1 % (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 % LTL model checking
6
7 :- module(ltl,[ltl_model_check/4,ltl_model_check2/4,
8 ltl_model_check_ast/5,
9 ltl_check_assertions/2, parse_ltlfile/2,
10 ltl_model_check_with_ce/4, ltl_model_check_with_ce1/5,
11 parse_and_pp_ltl_formula/2, % imported from ltl_tools.pl
12 ltl_formula_structure/3,
13 pp_ltl_formula/2,
14 preprocess_formula/2,
15 %% reset_ltl/0,
16 find_atomic_property_formula/2,
17 executetrace/1,set_trace_to_init/1,
18 parse_and_preprocess_formula/3,
19 is_fairness_implication/1,
20 tcltk_play_ltl_counterexample/2,
21 get_ltl_formula_strings/2, get_ltl_formulas/3
22 ]).
23
24 /* SICSTUS libraries */
25 :- use_module(library(lists)).
26 :- use_module(library(ordsets)).
27
28 /* ProB standard libraries */
29 % B
30 :- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2,get_texpr_pos/2,predicate_identifiers/2]).
31 :- use_module(probsrc(bmachine),[
32 b_definition_prefixed/5, b_get_typed_definition/3, b_top_level_operation/1]).
33 % CSP
34 :- use_module(probcspsrc(haskell_csp),[filter_formulas_from_pragmas/3]).
35 % utility modules
36 :- use_module(probsrc(tools)).
37 :- use_module(probsrc(translate)).
38 :- use_module(probsrc(debug)).
39 :- use_module(probsrc(error_manager)).
40 :- use_module(probsrc(tools_printing), [print_error/1]).
41 :- use_module(probsrc(preferences),[get_preference/2]).
42 % state space relevant modules
43 :- use_module(probsrc(specfile),[animation_mode/1]).
44 :- use_module(probsrc(state_space),[set_max_nr_of_new_impl_trans_nodes/1,
45 current_state_id/1,visited_expression/2, visited_expression_id/1,
46 transition/4,
47 %retract_visited_expression/2, % used for test cases
48 impl_trans_term_all/2,state_space_reset/0,
49 execute_id_trace_from_current/3, set_context_state/1, clear_context_state/0,
50 state_space_initialise/0,
51 find_trace_to_initial_state/2, find_initialised_states/1,
52 %compute_transitions_if_necessary_saved/1, % NOT EXPORTED
53 not_all_transitions_added/1,
54 reset_counterexample/0,
55 add_counterexample_node/1, add_counterexample_op/1]).
56 :- use_module(probsrc(state_space_exploration_modes),[depth_breadth_first_mode/1,set_depth_breadth_first_mode/1]).
57 % Optimisations (POR and PGE)
58 :- use_module(probporsrc(ample_sets),[stutter_action/1, visible_action/1,check_cycle_proviso/0,reset_runtime_dynamic_predicates_POR/0]).
59 :- use_module(probporsrc(static_analysis),[compute_dependendency_relation_of_all_events_in_the_model/3]).
60 % static analyses
61 :- use_module(probsrc(b_read_write_info),[b_get_read_write/3,b_get_operation_read_guard_vars/4]).
62
63
64 /* ProB LTL modules */
65 :- use_module(probltlsrc(ltl_fairness)).
66 :- use_module(probltlsrc(ltl_verification)).
67 :- use_module(probltlsrc(ltl_safety)).
68 :- use_module(probltlsrc(ltl_tools)).
69 :- use_module(probltlsrc(ltl_translate)).
70 :- use_module(probltlsrc(ltl_propositions)).
71 :- use_module(probltlsrc(state_space_explorer)).
72
73 :- use_module(probsrc(module_information),[module_info/2]).
74 :- module_info(group,ltl).
75 :- module_info(description,'This module provides LTL model checking on models.').
76
77 /* LTL relevant PL modules */
78 % import the low-level C-library wrapper
79 :- use_module(extension('ltlc/ltlc')).
80
81 :- set_prolog_flag(double_quotes, codes).
82
83 parse_and_preprocess_formula(FormulaAsAtom,Type,Result) :-
84 (temporal_parser(FormulaAsAtom,Type,LtlCtl) -> true
85 ; add_error(Type,'LTL Parser failed:',FormulaAsAtom),fail
86 ),
87 ( LtlCtl=syntax_error ->
88 add_error(Type,'Syntax error while parsing:',FormulaAsAtom),fail
89 ;
90 preprocess_formula(LtlCtl,Result)
91 ).
92
93 % a utility to find a node satisfying a restricted atomic LTL property
94 find_atomic_property_formula(AtomFormula,NodeID) :-
95 parse_and_preprocess_formula(AtomFormula,ltl,PF),
96 visited_expression_id(NodeID),
97 check_atomic_property_formula(PF,NodeID).
98
99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
100 % get LTL formulas from 'DEFINITIONS' for B machines and
101 % from pragmas ({-# ... #-}) for CSP-M specifications
102 :- dynamic ltl_formula_cache/2.
103
104 get_ltl_formula_strings(Names,Strings) :-
105 (animation_mode(b)
106 -> get_ltl_def_formula_strings(Names,Strings) % ASSERT_LTL... DEFINITIONS
107 ; animation_mode(cspm)
108 -> filter_formulas_from_pragmas(ltl,Names,Strings) % assert P |= LTL: "ltl-formula"
109 ; animation_mode(csp_and_b)
110 -> get_ltl_def_formula_strings(BNames,BStrings),
111 filter_formulas_from_pragmas(ltl,CSPNames,CSPStrings),
112 append(BNames,CSPNames,Names),
113 append(BStrings,CSPStrings,Strings)
114 ).
115
116 get_ltl_formulas(Names,Strings,Formulas) :-
117 get_ltl_formula_strings(Names,Strings),
118 (ltl_formula_cache(Strings,Formulas)
119 -> true
120 ; retractall(ltl_formula_cache(_,_)),
121 temporal_parser_l(Strings,ltl,Formulas),
122 assertz(ltl_formula_cache(Strings,Formulas))
123 ).
124
125 get_ltl_def_formula_strings(Names,Formulas) :-
126 findall(ltl_assertion(Name,F),get_ltl_formula_string(Name,F),Assertions),
127 findall(N,member(ltl_assertion(N,_),Assertions),Names),
128 findall(F,member(ltl_assertion(_,F),Assertions),Formulas).
129 get_ltl_formula_string(Tail,S) :-
130 b_definition_prefixed(_,'ASSERT_LTL',Tail,DefName,_),
131 b_get_typed_definition(DefName,[],F),
132 ( get_texpr_expr(F,string(S)) -> true
133 ; get_texpr_pos(F,Pos) ->
134 add_all_perrors([error('Expected String for LTL formula',Pos)]),
135 fail).
136
137 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
138 % check all LTL assertions in a machine
139
140 ltl_check_assertions(Limit,Outcome) :-
141 get_ltl_formulas(Names,Strings,Formulas),
142 extract_expectations(Names,Exp),
143 ltl_check_assertions2(Names,Strings,Formulas,Exp,Limit,Outcomes),
144 merge_outcomes(Outcomes,Outcome).
145
146 ltl_check_assertions2([],[],[],[],_,[]).
147 ltl_check_assertions2([Name|Nrest],[String|Srest],[Formula|Frest],[Exp|Erest],Limit,[Outcome|Orest]) :-
148 print('Checking LTL formula '),print(Name),print(': '),print(String),nl,
149 flush_output(user_output),
150 catch( ltl_model_check2(Formula,Limit,init,Status),
151 E,
152 Status = exception(E)),
153 ( Exp=pass, Status=ok -> Outcome=pass, print('no counter-example found, test passed\n')
154 ; Exp=fail, Status=no -> Outcome=pass, print('counter-example found, test passed\n')
155 ; Status=exception(E) ->
156 add_error(ltl,'Caught exception: ',E),Outcome=error
157 ; Exp=pass, Status=no ->
158 Outcome=fail, add_error(ltl, 'Expected correct formula, but found counter-example')
159 ; Exp=fail, Status=ok ->
160 Outcome=fail, add_error(ltl, 'Expected counter-example, but model checker found none')
161 ;
162 add_error(ltl,'Unexpected result: ',(Exp,Status)),Outcome=fail),
163 ltl_check_assertions2(Nrest,Srest,Frest,Erest,Limit,Orest).
164
165 extract_expectations([],[]).
166 extract_expectations([N|Nrest],[E|Erest]) :-
167 ( atom(N),atom_codes(N,Codes),append(_,"FAIL",Codes)
168 -> E=fail ; E=pass),
169 extract_expectations(Nrest,Erest).
170
171 merge_outcomes(List,Result) :-
172 merge_outcomes2(List,no_tests,Result).
173 merge_outcomes2([],R,R).
174 merge_outcomes2([O|Rest],P,R) :-
175 merge_outcomes3(P,O,I),
176 merge_outcomes2(Rest,I,R).
177 merge_outcomes3(no_tests,X,X) :- !.
178 merge_outcomes3(_,error,error) :- !.
179 merge_outcomes3(P,fail,fail) :- P\=error,!.
180 merge_outcomes3(P,pass,P).
181
182 %*******************************************************************************
183
184 % ltl_model_check(FormulaAsAtom,Max,Mode,Status):
185 % FormulaAsAtom: The LTL formula as an atom
186 % Max: The maximum number of states that should be newly calculated, use -1 for no limit
187 % Mode: Where to start the search in state space
188 % starthere: start the evaluation of the formula in the current state
189 % init: start in the (possible several) initialisation states of the model
190 % checkhere: start the search as in init, but check the formula F in the
191 % current state by constructing a new formula (current -> F) "makes sense only for Past-LTL"
192 % Status:
193 % no: the model does not fulfil the formula, a counter-example is shown by
194 % modifying the history
195 % ok: the model does fulfil the formula
196 % incomplete: the search was stopped (usually because the limit Max was reached)
197 % before finding a counter-example or guarantee the absent of a counter-example
198 ltl_model_check(FormulaAsAtom,Max,Mode,Status) :-
199 debug_println(19,parsing_ltl_formula(FormulaAsAtom)),
200 reset_counterexample,
201 ( temporal_parser(FormulaAsAtom,ltl,Ltl) ->
202 debug_println(19,ltl_model_check(Ltl)),
203 (ltl_model_check2(Ltl,Max,Mode,Status) -> true
204 ; add_error(ltl,'LTL checking internal failure:',Ltl),
205 fail)
206 ;
207 add_error(ltl,'LTL Parser failed:',FormulaAsAtom),fail
208 ).
209
210 ltl_model_check2(Ltl,Max,Mode,Status) :-
211 debug_println(19,initialising_ltlc(Ltl,Max,Mode)),
212 ( Ltl=syntax_error ->
213 Status=syntax_error
214 ;
215 ltl_model_check_ast(Ltl,Max,Mode,_,Result),
216 convert_result(Result,Mode,Status)).
217
218 % TypeOfMC is output and either regular_ltl_mc or safety_ltl_mc
219 ltl_model_check_ast(Ltl,Max,Mode,TypeOfMC,MinimizedResult) :-
220 perform_static_analyses_if_necessary(Ltl),
221 set_max_nr_of_new_impl_trans_nodes(Max),
222 % initialising all given fairness constraints
223 initialise_fairness_assumptions(Ltl,WeakFairnessAssumption,StrongFairnessAssumption,LtlFormula),
224 debug_println(9,fairness_constraints(weak(WeakFairnessAssumption),strong(StrongFairnessAssumption))),
225 select_ltl_mode(Mode,LtlFormula,Startnodes,Ltl2),
226 preprocess_formula(Ltl2,Ltl3),
227 debug_println(9,preprocess_formula(LtlFormula,Ltl3)),
228 ltl_model_check4(Ltl3,Max,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,TypeOfMC,Result),
229 !,
230 % validating the counter-example returned by the model-checker
231 % if it fails, then this is a bug in the model-checker
232 call_ltl_verification(Result,Ltl3),
233 % the same to check if the counter-example is a fair counter-example (if fairness set)
234 call_ltl_fairness_verification(Result,WeakFairnessAssumption,StrongFairnessAssumption),
235 minmize_model_lasso(Result,MinimizedResult),
236 debug_println(9,ltl_result(TypeOfMC,MinimizedResult)).
237
238 :- use_module(probsrc(preferences),[get_preference/2]).
239 % deciding whether to run the safety model checker or the ordinary LTL model checker
240 ltl_model_check4(Ltl,Max,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,TypeOfMC,Result) :-
241 % checkig whether the property is a safety LTL formula
242 (safety_mc_not_possible(Ltl,Max)
243 -> TypeOfMC=regular_ltl_mc,
244 call_c_initialisation,
245 ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result)
246 ; debug_println(19,'Formula is a safety property'),
247 TypeOfMC=safety_ltl_mc,
248 ltl_mc_safety_property(Ltl,Startnodes,Result)
249 ).
250
251 safety_mc_not_possible(Ltl,_) :- \+ is_safety_property(Ltl,_),!,
252 (debug_mode(off) -> true
253 ; pp_ltl_formula(Ltl,LS),
254 add_message(ltl,'LTL formula could not be determined to be a safety property: ',LS)
255 ).
256 safety_mc_not_possible(Ltl,_) :-
257 \+ safety_property_can_be_encoded_directly(Ltl),
258 \+ is_ltl2ba_tool_installed,!, % will also generate a message
259 pp_ltl_formula(Ltl,LS),
260 add_message(ltl,'LTL formula is a (complex) safety property; install ltl2ba (see above)): ',LS).
261 safety_mc_not_possible(Ltl,_) :- get_preference(use_safety_ltl_model_checker,false),!,
262 pp_ltl_formula(Ltl,LS),
263 add_message(ltl,'LTL formula is a safety property; set use_safety_ltl_model_checker to true to check it more efficiently: ',LS).
264 safety_mc_not_possible(_,Max) :- % ProB2 calls with Max=500
265 Max>=0,
266 add_message(ltl,'Ignoring ltllimit for safety model checking: ',Max),fail.
267
268 ltl_model_check5([],_Ltl,_WeakFairnessAssumption,_StrongFairnessAssumption,nostart) :- !.
269 ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result) :-
270 (get_preference(por,ample_sets);get_preference(por,ample_sets2)),!,
271 % explore state space without performing any checks
272 depth_breadth_first_mode(DFMODE),
273 set_depth_breadth_first_mode(depth_first), % set to depth-first mode
274 print_message('******** starting a static LTL model check with partial order reduction ********'),
275 statistics(runtime,[T1,_]),
276 explore_state_space(0,-1,NodesAnalysed,_LimitTime,Res),
277 statistics(runtime,[T2,_]),
278 D is T2-T1,
279 debug_println(9,statspace_stats(NodesAnalysed,Res)),
280 format('state space exploration needed ~w ms to explore ~w states\n',[D,NodesAnalysed]),
281 print_message('******** state space explored using partial order reduction ********'),
282 set_depth_breadth_first_mode(DFMODE), % reset to previous mode
283 print_message('******** start LTL model checking on the explored state space ********'),
284 ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result).
285 ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result) :-
286 ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result).
287
288 ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result) :-
289 % checking first whether some fairness constraints have been set up
290 (fairness_check_on(WeakFairnessAssumption,StrongFairnessAssumption) ->
291 c_ltl_modelcheck(Ltl, Startnodes, Result, ltl:cltl_callback, none,
292 ltl_fairness:cltl_get_transition_ids_callback, ltl_fairness:cltl_get_enabled_actions_callback, WeakFairnessAssumption,StrongFairnessAssumption)
293 ; c_ltl_modelcheck(Ltl, Startnodes, Result, ltl:cltl_callback) % no fairness assumptions have been imposed
294 ).
295
296 call_c_initialisation :- ltlc_init,!.
297 call_c_initialisation :-
298 add_error(ltl,'Initialisation of LTL-C module failed'),
299 fail.
300
301 select_ltl_mode(starthere,Ltl,[Startnode],not(Ltl)) :-
302 !,current_state_id(Startnode).
303 select_ltl_mode(init,Ltl,Startnodes,not(Ltl)) :-
304 !,find_initialised_states(Startnodes).
305 select_ltl_mode(checkhere,Ltl,Startnodes,not(globally(implies(ap(current),Ltl)))) :-
306 !,find_initialised_states(Startnodes).
307 select_ltl_mode(specific_node(Startnode),Ltl,[Startnode],not(Ltl)) :- !.
308 % TODO: support providing explicit trace to check or check history up to current state only
309 select_ltl_mode(Mode,Ltl,[],Ltl) :-
310 add_error(ltl,'Internal error: Unexpected mode: ', Mode),
311 fail.
312
313 %:- use_module(probsrc(model_checker),[model_checking_is_incomplete/6]).
314 % 'nostart' means no initialisation state found (safety properties are true, but plain liveness properties are not true)
315 convert_result(nostart,_,Result) :- !,Result=nostart.
316 convert_result(none,_,Result) :- !, Result=ok.
317 % TO DO: maybe return different result when model_checking_is_incomplete(0,1,0,0,_Msg,_Term) is true
318 % limit 'Max' reached (possibly there are unexplored states that have not been checked yet)
319 convert_result(incomplete,_,Result) :- !,Result=incomplete.
320 % model/2 means counter-example has been found, if Entry=no_loop then we have a finite path (safety property or deadlock)
321 % if Entry=loop(Idx) then we have a counter-example in lasso form with entry node of the loop on the Idx-position (starting from 0)
322 convert_result(model(CE,_Entry),Mode,Result) :- !, Result=no,
323 translate_ctrace(CE,Ops,N,Dest),
324 ( (Mode=init; Mode=checkhere) ->
325 ce_get_first_state(CE,UsedInitState),
326 set_trace_to_init(UsedInitState)
327 ; Mode=specific_node(InitState) ->
328 set_trace_to_init(InitState)
329 ; true),
330 execute_id_trace_from_current(Dest,Ops,N).
331 convert_result(Result,_,_) :-
332 add_internal_error('Unexpected LTL result: ', convert_result(Result,_,_)),
333 fail.
334
335 ce_get_first_state([atom(State,_,_)|_],State).
336
337 :- use_module(probsrc(tools),[minimize_lasso/4]).
338 % try to reduce/minimise counter-example lasso prefix as much as possible
339 minmize_model_lasso(model(AtomList,loop(Idx)),model(NewAtomList,loop(NewIdx))) :-
340 append_length(Prefix,Loop,AtomList,Idx),
341 minimize_lasso(Prefix,Loop,NewPrefix,NewLoop),
342 append_length(NewPrefix,NewLoop,NewAtomList,NewIdx),
343 NewIdx < Idx,!, % triggers e.g. for test 929 and GF [a.red.red.red], 930, 1221
344 debug_println(9,reducing_ltl_lasso(NewIdx,Idx,NewPrefix,NewLoop)).
345 minmize_model_lasso(M,M).
346
347
348 % ---------------
349
350 reset_ltl :-
351 retractall(ltl_formula_cache(_,_)),
352 retractall(ltl_counter_examples_cache(_,_,_,_)).
353
354 :- use_module(probsrc(eventhandling),[register_event_listener/3]).
355 :- register_event_listener(reset_specification,reset_ltl,
356 'Reset LTL Model Checker.').
357 :- register_event_listener(reset_prob,reset_ltl,
358 'Reset LTL Model Checker.').
359
360 translate_ctrace(Atoms,OpIds,StateIds,Dest) :-
361 translate_ctrace2(Atoms,beginning,OpIds,StateIds,Dest).
362 translate_ctrace2([atom(StartNode,_,OpId)|RestAtoms],_PreviousState,Ops,Nodes,Dest) :-
363 add_counterexample_node(StartNode),
364 add_counterexample_op(OpId),
365 ( OpId = none -> Ops=[],Nodes=[],Dest=StartNode
366 ;
367 transition(StartNode,_Op,OpId,NextNode),
368 Ops=[OpId|OpRest], Nodes=[NextNode|NextRest],
369 translate_ctrace2(RestAtoms,NextNode,OpRest,NextRest,Dest)).
370 translate_ctrace2([],Dest,[],[],Dest).
371
372 % replacing unparsed/1 by atomic propositions
373 % DEAD CODE
374 %% unparsed_ap(ap(P),ap(P)) --> !.
375 %% unparsed_ap(action(unparsed_b(OpName/Arity/Types,Exprs)),action(b(OpName/Arity,Es))) --> !,
376 %% add_unparsed_exprs(Exprs,Types,Es).
377 %% unparsed_ap(action(b(OpName/Arity/_Types)),action(b(OpName/Arity))) --> !.
378 %% unparsed_ap(action(Op),action(Op)) --> !.
379 %% unparsed_ap(unparsed(Unparsed),ap(P)) --> !,[pred(Unparsed,P)].
380 %% unparsed_ap(F,N) --> {F =..[Functor|Args]},unparsed_ap_l(Args,NArgs),{N=..[Functor|NArgs]}.
381 %% unparsed_ap_l([],[]) --> [].
382 %% unparsed_ap_l([F|Rest],[N|NRest]) --> unparsed_ap(F,N), unparsed_ap_l(Rest,NRest).
383
384 %% add_unparsed_exprs([],[],[]) --> [].
385 %% add_unparsed_exprs([expr(P,U)|UR],[T|TR],[expr(P,E)|ER]) -->
386 %% [expr(U,T,E)], add_unparsed_exprs(UR,TR,ER).
387
388 %*******************************************************************************
389 % set current trace
390
391 executetrace(Trace) :-
392 translate_trace(Trace,OpIds,Ids,Dest),
393 debug_println(9,exec(Dest,OpIds,Ids)),
394 execute_id_trace_from_current(Dest,OpIds,Ids),!.
395 executetrace(Trace) :- add_internal_error('Could not replay counterexample (trace to init): ',executetrace(Trace)).
396
397 translate_trace([Dest],[],[],Dest) :-
398 add_counterexample_node(Dest).
399 translate_trace([Start,Id|RestNodes],[OpId|OpRest],[Id|IdRest],Dest) :-
400 !,transition(Start,_Op,OpId,Id),
401 add_counterexample_node(Start),
402 add_counterexample_op(OpId),
403 translate_trace([Id|RestNodes],OpRest,IdRest,Dest).
404
405 %*******************************************************************************
406 % find initialised states
407
408
409 set_trace_to_init(Initstate) :-
410 find_trace_to_initial_state(Initstate,Trace),!,
411 state_space_reset,
412 executetrace(Trace).
413 set_trace_to_init(Initstate) :- add_internal_error('Could not replay counterexample: ',set_trace_to_init(Initstate)).
414
415
416
417 perform_static_analyses_if_necessary(Ltl) :-
418 % currently only for B and Event-B
419 (animation_mode(b) -> perform_static_analyses_if_necessary2(Ltl); true).
420
421 perform_static_analyses_if_necessary2(Ltl) :-
422 get_preference(por,PORMethod),
423 (PORMethod==ample_sets; PORMethod==ample_sets2),
424 prepare_ltl_model_checker_for_por(Ltl),
425 fail.
426 perform_static_analyses_if_necessary2(_Ltl).
427
428 %%% Predicates for determining which actions are visible and which are stutter in regard to the given LTL formula.
429 %%% An operation Op in a B machine should be identified as visible for a given LTL formula f, if Op writes variables used
430 %%% in the predicates in f or writes variables read in guard of operations inside the e(-) atoms in f.
431 %%% In case the respective LTL formula f contains a X (next) operator then M_{POR} |= f and M |= f are not equivalent.
432 %%% It is not clear how to handle LTL formulae containing transition propositions ([-]). (investigate e.g. LTL formulae of the form: ([Op] => g))
433 prepare_ltl_model_checker_for_por(Ltl) :-
434 debug_println(9,prepare_ltl_model_checker_for_por(Ltl)),
435 % state space should be reseted every time when a new LTL_X formula is checked,
436 % because of the stutter condition
437 state_space_initialise,
438 reset_runtime_dynamic_predicates_POR,
439 get_stutter_visible_actions(Ltl,StutterActions,VisibleActions,NextOrTP),
440 (NextOrTP -> pp_ltl_formula(Ltl,LTLString),add_warning(ltl_mc_por, 'LTL formula contains X or Y operator, or [-] connstruct: ', LTLString); true),
441 debug_println(9,get_stutter_visible_actions(Ltl,stutter(StutterActions),visible(VisibleActions),next_tps(NextOrTP))),
442 assert_all_visible_stutter_actions(StutterActions,VisibleActions),
443 % if the model is not reloaded _EnableGraph will not be computed every time a new LTL formula is checked
444 get_por_preferences(POROptions),
445 assertz(ample_sets:check_cycle_proviso),
446 compute_dependendency_relation_of_all_events_in_the_model(0,POROptions,_EnableGraph).
447
448 % get_stutter_visible_actions(+Ltl,-StutterActions,-VisibleActions)
449 % Ltl: the parsed Ltl formula presented as Prolog term.
450 % StutterActions: the set of stutter actions in regard to Ltl
451 % VisibleActions: the set of visible actions in regard to Ltl
452 get_stutter_visible_actions(Ltl,StutterActions,VisibleActions,NextOrTP) :-
453 findall(Op,b_top_level_operation(Op),Ops),
454 list_to_ord_set(Ops,Operations),
455 look_up_for_visible_actions(Ltl,Operations,VisActions,NextOrTP),
456 list_to_ord_set(VisActions,VisibleActions),
457 ord_subtract(Operations,VisibleActions,StutterActions).
458
459 look_up_for_visible_actions(Ltl,Operations,VisActions,NextOrTP) :-
460 look_up_for_visible_actions1(Ltl,Operations,VisActions,NextOrTPs),
461 (NextOrTPs = [] -> NextOrTP=fail;NextOrTP=true).
462
463 look_up_for_visible_actions1(ap(bpred(Pred)),Ops,Acts,[]) :- !,
464 predicate_identifiers(Pred,Ids),
465 list_to_ord_set(Ids,Vars),
466 get_actions_modifying_variables(Vars,Ops,Acts).
467 look_up_for_visible_actions1(action(bop(Name,_NArgs,_NRes,_Args,_Outputs)),_Ops,[Name],[true]) :- !.
468 %% in case of [evt], 'evt' will be recognised as visible
469 % All actions that can enable or disable an action checked for enabledness should be
470 % asserted as visible. This means that every action that writes the variables of action
471 % "a" which is checked for enabledness (e(a)) in the LTL-formula.
472 look_up_for_visible_actions1(enabled(bop(Name,_NArgs,_NRes,_Args,_Outputs)),Ops,Acts,[]) :- !,
473 b_get_operation_read_guard_vars(Name,true,GuardReads,_Precise),
474 list_to_ord_set(GuardReads,Vars),
475 get_actions_modifying_variables(Vars,Ops,Acts).
476 look_up_for_visible_actions1(next(F),Ops,Acts,[true|NextOrTPs]) :- !,
477 look_up_for_visible_actions1(F,Ops,Acts,NextOrTPs).
478 look_up_for_visible_actions1(yesterday(F),Ops,Acts,[true|NextOrTPs]) :- !,
479 look_up_for_visible_actions1(F,Ops,Acts,NextOrTPs).
480 look_up_for_visible_actions1(Term,_Ops,[],[]) :- % atomic can be deadlock or sink
481 atomic(Term),!. % can Term be a variable???
482 % the recursive clause
483 look_up_for_visible_actions1(Term,Ops,Actions,NextOrTPs) :-
484 compound(Term),!,
485 functor(Term,_Functor,N),
486 look_up_for_visible_actions_args(N,Term,Ops,Acts,NOrTPs),
487 append(Acts,Actions),append(NOrTPs,NextOrTPs).
488
489 look_up_for_visible_actions_args(0,_,_,[],[]) :- !.
490 look_up_for_visible_actions_args(N,Term,Ops,Actions,NextOrTPs) :-
491 N>0,!,
492 arg(N,Term,Arg),
493 look_up_for_visible_actions1(Arg,Ops,Acts,NTPs),
494 Actions = [Acts|ActsRest], NextOrTPs = [NTPs|NTPsRest],
495 N1 is N-1,
496 look_up_for_visible_actions_args(N1,Term,Ops,ActsRest,NTPsRest).
497
498 get_actions_modifying_variables(Vars,Ops,Actions) :-
499 maplist(variable_modified_by_action(Vars),Ops,Acts),
500 append(Acts,Actions).
501
502 variable_modified_by_action(Vars,Op,Res) :-
503 b_get_read_write(Op,_Read,Write),
504 (ord_intersect(Vars,Write)
505 -> Res=[Op]
506 ; Res=[]
507 ).
508
509 % asserting all stutter and visible actions before starting the LTL model checker
510 assert_all_visible_stutter_actions(StutterActions,VisibleActions) :-
511 maplist(assert_stutter_action,StutterActions),
512 maplist(assert_visible_action,VisibleActions).
513
514 assert_stutter_action(Act) :-
515 assertz(ample_sets:stutter_action(Act)).
516
517 assert_visible_action(Act) :-
518 assertz(ample_sets:visible_action(Act)).
519
520 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
521 % callback from LTLc:
522
523 % cltl_callback(+Node, -Aps, -Out, +Queries, +Specs):
524 % Callback predicate that evaluates for a state "Node" all atomic
525 % propositions and returns a list of outgoing transitions.
526 % It evaluates if each of the transitions met the propositions on transistions.
527 % "Queries" is a list of atomic propositions (ap), "Aps" is a lists where
528 % each entry is 0 resp 1 if the corresponding atomic proposition is true resp. false.
529 % "Specs" is a list of propositions on transitions (tp).
530 % "Out" is a list of outgoing transitions, trans(NextId,TransId,ResVector), for details, see below check_tps/4.
531 :- public cltl_callback/5.
532 cltl_callback(Node, Aps, Out, Queries, Specs) :-
533 %format('LTL-Callback from C for node ~w~n Atomic Prop. Queries = ~w~n Transition Prop. Queries = ~w~n',[Node,Queries,Specs]),
534 check_aps(Queries,Node,Aps), % generate a list of 0s and 1s, depending on whether the AP is met or not
535 impl_trans_term_all(Node,Trans), % find all outgoing transitions
536 check_tps(Trans,Specs,Node,Out). % evaluate the TP on each transition and generate a list of transitions, each
537 % annotated with 0s and 1s, depending on whether the TP is met or not
538 %print_trans_result(Node,Aps,Out).
539
540 %print_trans_result(Node,Aps,OutList) :-
541 % format(' APs truth vector for ~w: ~w~n Transitions: ',[Node,Aps]),
542 % maplist(print_trans_entry,OutList),nl.
543 %print_trans_entry(trans(NextId,TransId,ResVector)) :-
544 % format('(state id ~w, trans. id ~w, TP truth ~w) ',[NextId,TransId,ResVector]).
545
546
547 :- public cltl_callback_reexplore/5.
548 % predicate used only in case POR is enabled
549 % to satisfy the cycle condition
550 % at this moment of the call the node has already been explored
551 % and we need to apply the rest of the enabled events at node
552 % to force the full exploration of it
553 cltl_callback_reexplore(Node,Aps,Out,Queries,Specs) :-
554 check_aps(Queries,Node,Aps),
555 impl_trans_term_rest(Node,Trans),
556 check_tps(Trans,Specs,Node,Out),
557 debug_println(8,cltl_callback_reexplore(Node,Aps,Out,Queries,Specs)).
558
559 impl_trans_term_rest(Node,Trans) :-
560 get_all_already_explored_transitions(Node,Ops_so_far),
561 state_space: compute_transitions_if_necessary_saved(From),
562 findall(op(Id,ActionAsTerm,To),
563 (transition(From,ActionAsTerm,Id,To),nonmember(op(Id,ActionAsTerm,To),Ops_so_far)),
564 Trans).
565
566 get_all_already_explored_transitions(Node,Ops) :-
567 findall(op(TransId,ActionAsTerm,To),
568 transition(Node,ActionAsTerm,TransId,To),Ops).
569
570 % check list of atomic propositions (ap)
571 check_aps([],_,[]).
572 check_aps([Query|QRest],Node,[Result|RRest]) :-
573 (check_ap(Query,Node) -> !,Result=1; Result=0),
574 check_aps(QRest,Node,RRest).
575
576 % check list of transition properties:
577 % check_tps(+Transitions, +Specifications, +State, -Result):
578 % "Transitions" is a list of terms of the form op(Id,Operation,NextState)
579 % each term represents a transition from "State" to "NextState",
580 % with the id "Id" and operation "Operation"
581 % "Specifications" is a list of propositions on transistions (tp)
582 % "Result" is a list where each element corresponds to a transition in "Transitions"
583 % each entry has the form "trans(Next,Id,ResVector)" where "Next" and "Id"
584 % are the destination state and the id of the transition, respectively, and
585 % "ResVector" a list where each element corresponds to a proposition (tp)
586 % in "Specifications". It is 0 resp. 1 if the proposition is false resp. true.
587 check_tps([],_,_,[]).
588 check_tps([op(TransId,Op,Next)|OpRest],Specs,Node,[trans(Next,TransId,Tp)|TpRest]) :-
589 check_tps2(Specs,Node,TransId,Next,Op,Tp),
590 check_tps(OpRest,Specs,Node,TpRest).
591 check_tps2([],_,_,_,_,[]).
592 check_tps2([Spec|SRest],SrcNode,TransId,DstNode,Op,[Result|RRest]) :-
593 (check_transition_pred(Spec,Op,SrcNode,TransId,DstNode) -> !,Result=1; Result=0),
594 check_tps2(SRest,SrcNode,TransId,DstNode,Op,RRest).
595
596 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
597 %
598
599 ltl_formula_structure(Formula,Atomics,Structure) :-
600 c_ltl_aptp(Formula,ApTp),
601 pp_formulas(ApTp,Atomics),
602 ltl_structure(Formula,ApTp,Structure).
603
604 ltl_structure(fairnessimplication(_FAssumptions,F),Subformulas,Structure) :- !,
605 ltl_structure(F,Subformulas,Structure).
606 ltl_structure(ap(AP),Subformulas,ap(N)) :-
607 !,nth0(N,Subformulas,ap(AP)),!.
608 ltl_structure(action(TP),Subformulas,tp(N)) :-
609 !,nth0(N,Subformulas,action(TP)),!.
610 ltl_structure(F,ApTp,N) :-
611 F =.. [Functor|Args],
612 same_length(Args,NewArgs),
613 N =.. [Functor|NewArgs],
614 ltl_structure_l(Args,ApTp,NewArgs).
615 ltl_structure_l([],_,[]).
616 ltl_structure_l([F|Frest],ApTp,[N|Nrest]) :-
617 ltl_structure(F,ApTp,N),
618 ltl_structure_l(Frest,ApTp,Nrest).
619
620 % used by prob2_do_ltl_modelcheck (cf. groovyTests/ltlTest.groovy):
621 % Max is the maximum number of new nodes that will be explored; -1 means no limit
622 ltl_model_check_with_ce(Formula,Max,Mode,Result) :-
623 ltl_model_check_ast(Formula,Max,Mode,TypeOfMC,R1),
624 ce_result(R1,Mode,Formula,TypeOfMC,Result).
625
626 ce_result(nostart,_,_,_,nostart) :- !.
627 ce_result(none,_,_,_,ok) :- !.
628 ce_result(incomplete,_,_,_,incomplete) :- !.
629 ce_result(model(CE,LoopEntry),Mode,Formula,TypeOfMC,counterexample(Counterexample,LoopEntry,PathToCE)) :- !,
630 (ce_result_initpath(CE,Mode,PathToCE) -> true
631 ; add_error(ltl,'Could not find path to counter example: ', CE),fail),
632 (TypeOfMC=safety_ltl_mc -> N=0
633 ; c_ltl_aptp(Formula,ApTp), % list of atomic and transition propositions of Formula
634 length(ApTp,N)
635 ),
636 (convert_counterexample(CE,N,Counterexample)
637 -> true
638 ; add_error(ltl,'CE conversion failed: ', CE),fail).
639 ce_result(Result,_,_,_,_) :-
640 add_error(ltl,'Internal error: Unexpected result: ', Result),
641 fail.
642
643 :- use_module(probsrc(tcltk_interface),[find_shortest_trace_to_node/4]).
644 ce_result_initpath(CE,Mode,Path) :-
645 ce_get_first_state(CE,InitState),
646 (find_trace_to_initial_state(InitState,[root|StatePath]) -> true
647 ; Mode=specific_node(_), % we have started LTL model checking in another node
648 find_shortest_trace_to_node(root,InitState,_,StatePath)
649 ),
650 find_operation_ids(StatePath,root,Path).
651 find_operation_ids([],_,[]).
652 find_operation_ids([Dst|Srest],Src,[(Id,Op,Dst)|Irest]) :-
653 transition(Src,Op,Id,Dst),
654 find_operation_ids(Srest,Dst,Irest).
655
656 /* just restrict the evaluation bits to the atomic formulas */
657 convert_counterexample([],_N,[]).
658 convert_counterexample([atom(State,Evals,NextOp) |Arest],N,
659 [atom(State,NEvals,OpTuple)|Erest]) :-
660 (prefix_length(Evals,NEvals,N) -> true
661 ; add_warning(ltl,'Atom eval list is wrong: ',Evals), % the NEvals list does not seem to be used anywhere??
662 NEvals=Evals),
663 (NextOp = none -> OpTuple = none ; transition(State,Action,NextOp,Dst),OpTuple=(NextOp,Action,Dst)),
664 convert_counterexample(Arest,N,Erest).
665
666 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
667
668 % dynamic predicate for saving the LTL counterexamples for the Tcl/Tk interface
669 :- dynamic ltl_counter_examples_cache/4.
670
671 ltl_model_check_with_ce1(Proc,FormulaAsAtom,Max,Mode,Result) :-
672 debug_println(19,parsing_ltl_formula(FormulaAsAtom)),
673 (temporal_parser(FormulaAsAtom,ltl,Ltl) -> true ; add_error_fail(ltl,'LTL Parser failed: ',FormulaAsAtom)),
674 debug_println(19,checking_ltl_formula(Ltl)),
675 ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,Result).
676
677 ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,ActionTrace) :-
678 debug_println(19,initialising_ltlc2(Max,Mode)),
679 ( Ltl=syntax_error ->
680 ActionTrace=syntax_error
681 ;
682 interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result),
683 convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace)
684 ).
685
686 :- use_module(probsrc(user_interrupts),[catch_interrupt_assertion_call/1]).
687 :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
688 interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result) :-
689 user_interruptable_call_det(
690 catch_interrupt_assertion_call(ltl:ltl_model_check_ast(Ltl,Max,Mode,_,Result)),InterruptResult),
691 (InterruptResult=interrupted ->
692 Result=interrupted
693 ; (real_error_occurred ->
694 print_error('% *** Errors occurred while LTL model checking ! ***'),nl,nl,fail
695 ; print('LTL assertion check completed.'),nl)).
696
697 convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace) :-
698 ( Result = model(CE,LoopEntry) ->
699 pp_ltl_counterexample(LoopEntry,CE,ActionTrace),
700 (ltl_counter_examples_cache(Proc,Ltl,Mode,_) -> true; assertz(ltl_counter_examples_cache(Proc,Ltl,Mode,Result)))
701 ; Result = interrupted ->
702 ActionTrace = interrupted
703 ;
704 convert_result(Result,Mode,ActionTrace)).
705
706 pp_ltl_counterexample(deadlock,Counterexample,ce(Trace)) :- !,
707 length(Counterexample,N),
708 (N >= 2 ->
709 maplist(get_operation_name,Counterexample,Trace1),
710 ajoin_with_sep(Trace1,' -> ',Trace)
711 ;
712 Trace = deadlock).
713 pp_ltl_counterexample(no_loop,Counterexample,ce(Trace)) :- !,
714 maplist(get_operation_name,Counterexample,Trace1),
715 ajoin_with_sep(Trace1,' -> ',Trace).
716 pp_ltl_counterexample(loop(N),Counterexample,ce(Trace)) :- !,
717 prefix_length(Counterexample,PathToCE,N),
718 maplist(get_operation_name,PathToCE,PrefixTrace),
719 ajoin_with_sep(PrefixTrace,' -> ',PrefixTrace1),
720 append(PathToCE,CEPath,Counterexample),
721 maplist(get_operation_name,CEPath,SuffixTrace),
722 ajoin_with_sep(SuffixTrace,' -> ',SuffixTrace1),
723 ajoin([PrefixTrace1,' -> (',SuffixTrace1,')+'],Trace).
724 pp_ltl_counterexample(LoopEntry,_Counterexample,_CE) :-
725 add_error_fail(ltl, 'Internal error: unknown loop entry type: ', LoopEntry).
726
727 get_operation_name(atom(State,NEvasl,OpId),Res) :-
728 (OpId = none
729 -> Res = '|'
730 ; transition(State,Op,OpId,_NextState) ->
731 translate_event(Op,Res)
732 ;
733 add_error_fail(ltl_assertions_result, 'Internal Error: unknown operation in CE trace ', atom(State,NEvasl,OpId))).
734
735
736 tcltk_play_ltl_counterexample(Proc,Ltl) :-
737 ltl_counter_examples_cache(Proc,Ltl,Mode,model(CE,_Entry)),
738 translate_ctrace(CE,Op,N,Dest),
739 ( (Mode = init; Mode = checkhere) ->
740 ce_get_first_state(CE,UsedInitState),
741 set_trace_to_init(UsedInitState)
742 ; Mode = specific_node(NodeID) ->
743 set_trace_to_init(NodeID)
744 ;
745 true
746 ),execute_id_trace_from_current(Dest,Op,N).
747 tcltk_play_ltl_counterexample(Proc,Ltl) :-
748 add_error_fail(ltl_counter_example, 'Internal error: No counterexample has been asserted for the following configuration: ',(Proc,Ltl)).
749
750 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
751 % verify a counter-example
752
753 callback_tp(TP,StateId,TransId) :-
754 ( transition(StateId,Op,TransId,DestId) ->
755 check_transition_pred(TP,Op,StateId,TransId,DestId)
756 ;
757 add_error(ltl,'Internal error: callback_tp called for unknown transition: ',
758 state_trans(StateId,TransId)),
759 fail
760 ).
761
762 call_ltl_verification(model(Atoms,Status),Formula) :-
763 !,call_ltl_verification2(Status,Atoms,Formula).
764 call_ltl_verification(_,_Formula).
765
766 call_ltl_verification2(Status,Atoms,Formula) :-
767 maplist(convert_atom_to_statetransition,Atoms,StateTransitions),!,
768 ( evaluate_ltl_formula(Formula,StateTransitions,Status,
769 check_ap,callback_tp,Result) ->
770 (Result = true -> true
771 ; add_error(ltl,'Verification of LTL formula counter example yielded unexpected result: ',Result))
772 ;
773 add_error(ltl,'Verification of LTL formula counter example failed: ',Formula)).
774 call_ltl_verification2(_,Atoms,_) :-
775 add_error(ltl,'Evaluation of LTL yielded unexpected atoms: ',Atoms).
776
777 convert_atom_to_statetransition(atom(NodeId,_,TransId),strans(NodeId,TransId)).
778
779
780 % fairness
781 is_fairness_implication(fairnessimplication(_FAssumptions,_F)).
782
783 call_ltl_fairness_verification(model(Atoms,Status),WeakDNF,StrongDNF) :-
784 !,maplist(convert_atom_to_statetransition,Atoms,ST),
785 call_ltl_fairness_verification1(WeakDNF,weak,ST,Status),
786 call_ltl_fairness_verification1(StrongDNF,strong,ST,Status).
787 call_ltl_fairness_verification(_,_WeakDNF,_StrongDNF).
788
789 call_ltl_fairness_verification1([],_Type,_ST,_Status) :- !.
790 call_ltl_fairness_verification1(all,Type,ST,Status) :- !,
791 get_fairness_specification(Status,ST,Assumption),
792 call_ltl_fairness_verification1(Assumption,Type,ST,Status).
793 call_ltl_fairness_verification1(DNF,Type,ST,Status) :-
794 ( call_ltl_fairness_verification2(DNF,Type,ST,Status,Result) ->
795 true
796 ;
797 add_error(ltl,'Evalutation of LTL fairness failed: ',Type/DNF)),
798 ( Result = fair -> true
799 ;
800 print(Type/DNF),nl,
801 add_error(ltl,'Evaluation of LTL yields that the result violates fairness: ',Type/Result)).
802
803 call_ltl_fairness_verification2([],_Type,_ST,_Status,unfair([])).
804 call_ltl_fairness_verification2([Clause|CRest],Type,ST,Status,Result) :-
805 call_ltl_fairness_verification3(Clause,Type,ST,Status,CResult),
806 ( CResult = fair -> Result=fair
807 ; CResult = unfair(Cause) ->
808 call_ltl_fairness_verification2(CRest,Type,ST,Status,RResult),
809 ( RResult = fair -> Result=fair
810 ; RResult = unfair(Causes) -> Result=unfair([Cause|Causes]))).
811 call_ltl_fairness_verification3([],_Type,_ST,_Status,fair).
812 call_ltl_fairness_verification3([Spec|SRest],Type,ST,Status,Result) :-
813 evaluate_ltl_fairness(Type,ST,Status,ev_fairness_id(Spec),ev_fairness_id(Spec),LResult),
814 ( LResult = fair ->
815 call_ltl_fairness_verification3(SRest,Type,ST,Status,Result)
816 ; LResult = unfair(Id) ->
817 Result = unfair(Id)
818 ;
819 add_error_fail(ltl,'Unknown result after fairness verification check: ', evaluate_ltl_fairness(Type,ST,Status,ev_fairness_id(Spec),LResult))).