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