1 % (c) 2009-2024 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 :- use_module(probpgesrc(pge_algo), [is_pge_opt_on/0]).
61 % static analyses
62 :- use_module(probsrc(b_read_write_info),[b_get_read_write/3,b_get_operation_read_guard_vars/4]).
63
64
65 /* ProB LTL modules */
66 :- use_module(probltlsrc(ltl_fairness)).
67 :- use_module(probltlsrc(ltl_verification)).
68 :- use_module(probltlsrc(ltl_safety)).
69 :- use_module(probltlsrc(ltl_tools)).
70 :- use_module(probltlsrc(ltl_translate)).
71 :- use_module(probltlsrc(ltl_propositions)).
72 :- use_module(probltlsrc(state_space_explorer)).
73
74 :- use_module(probsrc(module_information),[module_info/2]).
75 :- module_info(group,ltl).
76 :- module_info(description,'This module provides LTL model checking on models.').
77
78 /* LTL relevant PL modules */
79 % import the low-level C-library wrapper
80 :- use_module(extension('ltlc/ltlc')).
81
82 :- set_prolog_flag(double_quotes, codes).
83
84 parse_and_preprocess_formula(FormulaAsAtom,Type,Result) :-
85 temporal_parser(FormulaAsAtom,Type,ParseResult),
86 preprocess_formula(ParseResult,Result).
87
88 % a utility to find a node satisfying a restricted atomic LTL property
89 find_atomic_property_formula(AtomFormula,NodeID) :-
90 parse_and_preprocess_formula(AtomFormula,ltl,PF),
91 visited_expression_id(NodeID),
92 check_atomic_property_formula(PF,NodeID).
93
94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
95 % get LTL formulas from 'DEFINITIONS' for B machines and
96 % from pragmas ({-# ... #-}) for CSP-M specifications
97 :- dynamic ltl_formula_cache/2.
98
99 get_ltl_formula_strings(Names,Strings) :-
100 (animation_mode(b)
101 -> get_ltl_def_formula_strings(Names,Strings) % ASSERT_LTL... DEFINITIONS
102 ; animation_mode(cspm)
103 -> filter_formulas_from_pragmas(ltl,Names,Strings) % assert P |= LTL: "ltl-formula"
104 ; animation_mode(csp_and_b)
105 -> get_ltl_def_formula_strings(BNames,BStrings),
106 filter_formulas_from_pragmas(ltl,CSPNames,CSPStrings),
107 append(BNames,CSPNames,Names),
108 append(BStrings,CSPStrings,Strings)
109 ).
110
111 get_ltl_formulas(Names,Strings,Formulas) :-
112 get_ltl_formula_strings(Names,Strings),
113 (ltl_formula_cache(Strings,Formulas)
114 -> true
115 ; retractall(ltl_formula_cache(_,_)),
116 temporal_parser_l(Strings,ltl,Formulas),
117 assertz(ltl_formula_cache(Strings,Formulas))
118 ).
119
120 get_ltl_def_formula_strings(Names,Formulas) :-
121 findall(ltl_assertion(Name,F),get_ltl_formula_string(Name,F),Assertions),
122 findall(N,member(ltl_assertion(N,_),Assertions),Names),
123 findall(F,member(ltl_assertion(_,F),Assertions),Formulas).
124 get_ltl_formula_string(Tail,S) :-
125 b_definition_prefixed(_,'ASSERT_LTL',Tail,DefName,_),
126 b_get_typed_definition(DefName,[],F),
127 ( get_texpr_expr(F,string(S)) -> true
128 ; get_texpr_pos(F,Pos) ->
129 add_all_perrors([error('Expected String for LTL formula',Pos)]),
130 fail).
131
132 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
133 % check all LTL assertions in a machine
134
135 ltl_check_assertions(Limit,Outcome) :-
136 get_ltl_formulas(Names,Strings,Formulas),
137 extract_expectations(Names,Exp),
138 ltl_check_assertions2(Names,Strings,Formulas,Exp,Limit,Outcomes),
139 merge_outcomes(Outcomes,Outcome).
140
141 ltl_check_assertions2([],[],[],[],_,[]).
142 ltl_check_assertions2([Name|Nrest],[String|Srest],[Formula|Frest],[Exp|Erest],Limit,[Outcome|Orest]) :-
143 print('Checking LTL formula '),print(Name),print(': '),print(String),nl,
144 flush_output(user_output),
145 catch( ltl_model_check2(Formula,Limit,init,Status),
146 E,
147 Status = exception(E)),
148 ( Exp=pass, Status=ok -> Outcome=pass, print('no counter-example found, test passed\n')
149 ; Exp=fail, Status=no -> Outcome=pass, print('counter-example found, test passed\n')
150 ; Status=exception(E) ->
151 add_error(ltl,'Caught exception: ',E),Outcome=error
152 ; Exp=pass, Status=no ->
153 Outcome=fail, add_error(ltl, 'Expected correct formula, but found counter-example')
154 ; Exp=fail, Status=ok ->
155 Outcome=fail, add_error(ltl, 'Expected counter-example, but model checker found none')
156 ;
157 add_error(ltl,'Unexpected result: ',(Exp,Status)),Outcome=fail),
158 ltl_check_assertions2(Nrest,Srest,Frest,Erest,Limit,Orest).
159
160 extract_expectations([],[]).
161 extract_expectations([N|Nrest],[E|Erest]) :-
162 ( atom(N),atom_codes(N,Codes),append(_,"FAIL",Codes)
163 -> E=fail ; E=pass),
164 extract_expectations(Nrest,Erest).
165
166 merge_outcomes(List,Result) :-
167 merge_outcomes2(List,no_tests,Result).
168 merge_outcomes2([],R,R).
169 merge_outcomes2([O|Rest],P,R) :-
170 merge_outcomes3(P,O,I),
171 merge_outcomes2(Rest,I,R).
172 merge_outcomes3(no_tests,X,X) :- !.
173 merge_outcomes3(_,error,error) :- !.
174 merge_outcomes3(P,fail,fail) :- P\=error,!.
175 merge_outcomes3(P,pass,P).
176
177 %*******************************************************************************
178
179 % ltl_model_check(FormulaAsAtom,Max,Mode,Status):
180 % FormulaAsAtom: The LTL formula as an atom
181 % Max: The maximum number of states that should be newly calculated, use -1 for no limit
182 % Mode: Where to start the search in state space
183 % starthere: start the evaluation of the formula in the current state
184 % init: start in the (possible several) initialisation states of the model
185 % checkhere: start the search as in init, but check the formula F in the
186 % current state by constructing a new formula (current -> F) "makes sense only for Past-LTL"
187 % Status:
188 % no: the model does not fulfil the formula, a counter-example is shown by
189 % modifying the history
190 % ok: the model does fulfil the formula
191 % incomplete: the search was stopped (usually because the limit Max was reached)
192 % before finding a counter-example or guarantee the absent of a counter-example
193 ltl_model_check(FormulaAsAtom,Max,Mode,Status) :-
194 debug_println(19,parsing_ltl_formula(FormulaAsAtom)),
195 reset_counterexample,
196 ( temporal_parser(FormulaAsAtom,ltl,Ltl) ->
197 debug_println(19,ltl_model_check(Ltl)),
198 (ltl_model_check2(Ltl,Max,Mode,Status) -> true
199 ; add_error(ltl,'LTL checking internal failure:',Ltl),
200 fail)
201 ;
202 add_error(ltl,'LTL Parser failed: ',FormulaAsAtom),fail
203 ).
204
205 ltl_model_check2(Ltl,Max,Mode,Status) :-
206 debug_println(19,initialising_ltlc(Ltl,Max,Mode)),
207 ( Ltl=syntax_error ->
208 Status=syntax_error
209 ;
210 ltl_model_check_ast(Ltl,Max,Mode,_,Result),
211 convert_result(Result,Mode,Status)).
212
213 % TypeOfMC is output and either regular_ltl_mc or safety_ltl_mc
214 ltl_model_check_ast(Ltl,Max,Mode,TypeOfMC,MinimizedResult) :-
215 perform_static_analyses_if_necessary(Ltl),
216 set_max_nr_of_new_impl_trans_nodes(Max),
217 % initialising all given fairness constraints
218 initialise_fairness_assumptions(Ltl,WeakFairnessAssumption,StrongFairnessAssumption,LtlFormula),
219 debug_println(9,fairness_constraints(weak(WeakFairnessAssumption),strong(StrongFairnessAssumption))),
220 select_ltl_mode(Mode,LtlFormula,Startnodes,Ltl2),
221 preprocess_formula(Ltl2,Ltl3),
222 debug_println(9,preprocess_formula(LtlFormula,Ltl3)),
223 ltl_model_check4(Ltl3,Max,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,TypeOfMC,Result),
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 safety_mc_not_possible(Ltl,_) :-
247 \+ safety_property_can_be_encoded_directly(Ltl),
248 \+ is_ltl2ba_tool_installed,!, % will also generate a message
249 pp_ltl_formula(Ltl,LS),
250 add_message(ltl,'LTL formula is a (complex) safety property; install ltl2ba (see above)): ',LS).
251 safety_mc_not_possible(Ltl,_) :- get_preference(use_safety_ltl_model_checker,false),!,
252 pp_ltl_formula(Ltl,LS),
253 add_message(ltl,'LTL formula is a safety property; set use_safety_ltl_model_checker to true to check it more efficiently: ',LS).
254 safety_mc_not_possible(_,Max) :- % ProB2 calls with Max=500
255 Max>=0,
256 add_message(ltl,'Ignoring ltllimit for safety model checking: ',Max),fail.
257
258 ltl_model_check5([],_Ltl,_WeakFairnessAssumption,_StrongFairnessAssumption,nostart) :- !.
259 ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result) :-
260 (get_preference(por,ample_sets);get_preference(por,ample_sets2)),!,
261 % explore state space without performing any checks
262 depth_breadth_first_mode(DFMODE),
263 set_depth_breadth_first_mode(depth_first), % set to depth-first mode
264 print_message('******** starting a static LTL model check with partial order reduction ********'),
265 statistics(runtime,[T1,_]),
266 explore_state_space(0,-1,NodesAnalysed,_LimitTime,Res),
267 statistics(runtime,[T2,_]),
268 D is T2-T1,
269 debug_println(9,statspace_stats(NodesAnalysed,Res)),
270 format('state space exploration needed ~w ms to explore ~w states\n',[D,NodesAnalysed]),
271 print_message('******** state space explored using partial order reduction ********'),
272 set_depth_breadth_first_mode(DFMODE), % reset to previous mode
273 print_message('******** start LTL model checking on the explored state space ********'),
274 ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result).
275 ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result) :-
276 ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result).
277
278 ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result) :-
279 % checking first whether some fairness constraints have been set up
280 (fairness_check_on(WeakFairnessAssumption,StrongFairnessAssumption) ->
281 c_ltl_modelcheck(Ltl, Startnodes, Result, ltl:cltl_callback, none,
282 ltl_fairness:cltl_get_transition_ids_callback, ltl_fairness:cltl_get_enabled_actions_callback, WeakFairnessAssumption,StrongFairnessAssumption)
283 ; c_ltl_modelcheck(Ltl, Startnodes, Result, ltl:cltl_callback) % no fairness assumptions have been imposed
284 ).
285
286 call_c_initialisation :- ltlc_init,!.
287 call_c_initialisation :-
288 add_error(ltl,'Initialisation of LTL-C module failed'),
289 fail.
290
291 select_ltl_mode(starthere,Ltl,[Startnode],not(Ltl)) :-
292 !,current_state_id(Startnode).
293 select_ltl_mode(init,Ltl,Startnodes,not(Ltl)) :-
294 !,find_initialised_states(Startnodes).
295 select_ltl_mode(checkhere,Ltl,Startnodes,not(globally(implies(ap(current),Ltl)))) :-
296 !,find_initialised_states(Startnodes).
297 select_ltl_mode(specific_node(Startnode),Ltl,[Startnode],not(Ltl)) :- !.
298 % TODO: support providing explicit trace to check or check history up to current state only
299 select_ltl_mode(Mode,Ltl,[],Ltl) :-
300 add_error(ltl,'Internal error: Unexpected mode: ', Mode),
301 fail.
302
303 %:- use_module(probsrc(model_checker),[model_checking_is_incomplete/6]).
304 % 'nostart' means no initialisation state found (safety properties are true, but plain liveness properties are not true)
305 convert_result(nostart,_,Result) :- !,Result=nostart.
306 convert_result(none,_,Result) :- !, Result=ok.
307 % TO DO: maybe return different result when model_checking_is_incomplete(0,1,0,0,_Msg,_Term) is true
308 % limit 'Max' reached (possibly there are unexplored states that have not been checked yet)
309 convert_result(incomplete,_,Result) :- !,Result=incomplete.
310 % model/2 means counter-example has been found, if Entry=no_loop then we have a finite path (safety property or deadlock)
311 % 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)
312 convert_result(model(CE,_Entry),Mode,Result) :- !, Result=no,
313 translate_ctrace(CE,Ops,N,Dest),
314 ( (Mode=init; Mode=checkhere) ->
315 ce_get_first_state(CE,UsedInitState),
316 set_trace_to_init(UsedInitState)
317 ; Mode=specific_node(InitState) ->
318 set_trace_to_init(InitState)
319 ; true),
320 execute_id_trace_from_current(Dest,Ops,N).
321 convert_result(Result,_,_) :-
322 add_internal_error('Unexpected LTL result: ', convert_result(Result,_,_)),
323 fail.
324
325 ce_get_first_state([atom(State,_,_)|_],State).
326
327 :- use_module(probsrc(tools),[minimize_lasso/4]).
328 % try to reduce/minimise counter-example lasso prefix as much as possible
329 minmize_model_lasso(model(AtomList,loop(Idx)),model(NewAtomList,loop(NewIdx))) :-
330 append_length(Prefix,Loop,AtomList,Idx),
331 minimize_lasso(Prefix,Loop,NewPrefix,NewLoop),
332 append_length(NewPrefix,NewLoop,NewAtomList,NewIdx),
333 NewIdx < Idx,!, % triggers e.g. for test 929 and GF [a.red.red.red], 930, 1221
334 debug_println(9,reducing_ltl_lasso(NewIdx,Idx,NewPrefix,NewLoop)).
335 minmize_model_lasso(M,M).
336
337
338 % ---------------
339
340 reset_ltl :-
341 retractall(ltl_formula_cache(_,_)),
342 retractall(ltl_counter_examples_cache(_,_,_,_)).
343
344 :- use_module(probsrc(eventhandling),[register_event_listener/3]).
345 :- register_event_listener(reset_specification,reset_ltl,
346 'Reset LTL Model Checker.').
347 :- register_event_listener(reset_prob,reset_ltl,
348 'Reset LTL Model Checker.').
349
350 translate_ctrace(Atoms,OpIds,StateIds,Dest) :-
351 translate_ctrace2(Atoms,beginning,OpIds,StateIds,Dest).
352 translate_ctrace2([atom(StartNode,_,OpId)|RestAtoms],_PreviousState,Ops,Nodes,Dest) :-
353 add_counterexample_node(StartNode),
354 add_counterexample_op(OpId),
355 ( OpId = none -> Ops=[],Nodes=[],Dest=StartNode
356 ;
357 transition(StartNode,_Op,OpId,NextNode),
358 Ops=[OpId|OpRest], Nodes=[NextNode|NextRest],
359 translate_ctrace2(RestAtoms,NextNode,OpRest,NextRest,Dest)).
360 translate_ctrace2([],Dest,[],[],Dest).
361
362 % replacing unparsed/1 by atomic propositions
363 % DEAD CODE
364 %% unparsed_ap(ap(P),ap(P)) --> !.
365 %% unparsed_ap(action(unparsed_b(OpName/Arity/Types,Exprs)),action(b(OpName/Arity,Es))) --> !,
366 %% add_unparsed_exprs(Exprs,Types,Es).
367 %% unparsed_ap(action(b(OpName/Arity/_Types)),action(b(OpName/Arity))) --> !.
368 %% unparsed_ap(action(Op),action(Op)) --> !.
369 %% unparsed_ap(unparsed(Unparsed),ap(P)) --> !,[pred(Unparsed,P)].
370 %% unparsed_ap(F,N) --> {F =..[Functor|Args]},unparsed_ap_l(Args,NArgs),{N=..[Functor|NArgs]}.
371 %% unparsed_ap_l([],[]) --> [].
372 %% unparsed_ap_l([F|Rest],[N|NRest]) --> unparsed_ap(F,N), unparsed_ap_l(Rest,NRest).
373
374 %% add_unparsed_exprs([],[],[]) --> [].
375 %% add_unparsed_exprs([expr(P,U)|UR],[T|TR],[expr(P,E)|ER]) -->
376 %% [expr(U,T,E)], add_unparsed_exprs(UR,TR,ER).
377
378 %*******************************************************************************
379 % set current trace
380
381 executetrace(Trace) :-
382 translate_trace(Trace,OpIds,Ids,Dest),
383 debug_println(9,exec(Dest,OpIds,Ids)),
384 execute_id_trace_from_current(Dest,OpIds,Ids),!.
385 executetrace(Trace) :- add_internal_error('Could not execute counter-example: ',executetrace(Trace)).
386
387 translate_trace([Dest],[],[],Dest) :-
388 add_counterexample_node(Dest).
389 translate_trace([Start,Id|RestNodes],[OpId|OpRest],[Id|IdRest],Dest) :-
390 !,transition(Start,_Op,OpId,Id),
391 add_counterexample_node(Start),
392 add_counterexample_op(OpId),
393 translate_trace([Id|RestNodes],OpRest,IdRest,Dest).
394
395 %*******************************************************************************
396 % find initialised states
397
398
399 set_trace_to_init(Initstate) :-
400 find_trace_to_initial_state(Initstate,Trace),!,
401 state_space_reset,
402 executetrace(Trace).
403 set_trace_to_init(Initstate) :- add_internal_error('Could not replay counter-example: ',set_trace_to_init(Initstate)).
404
405
406
407 perform_static_analyses_if_necessary(Ltl) :-
408 % currently only for B and Event-B
409 (animation_mode(b) -> perform_static_analyses_if_necessary2(Ltl); true).
410
411 perform_static_analyses_if_necessary2(Ltl) :-
412 get_preference(por,PORMethod),
413 (PORMethod==ample_sets; PORMethod==ample_sets2),
414 prepare_ltl_model_checker_for_por(Ltl),
415 fail.
416 perform_static_analyses_if_necessary2(_Ltl) :-
417 is_pge_opt_on,
418 pge_algo: compute_operation_relations_for_pge(0), % 0 for not including the invariant into the analysis
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_all1(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 impl_trans_term_all1(Node,Trans) :-
541 % In case that sink/deadlock is checked or the e(-) predicate is used in the LTL formula,
542 % the state will be completely explored by execution of the check_aps/3 predicate (see implementation of trans/3).
543 ( animation_mode(b), is_pge_opt_on, not_all_transitions_added(Node)
544 -> set_context_state(Node),
545 visited_expression(Node,CurState),
546 pge_algo: compute_transitions_pge(Node,CurState),
547 clear_context_state,
548 findall(op(Id,ActionAsTerm,To),
549 transition(Node,ActionAsTerm,Id,To),
550 Trans)
551 ; impl_trans_term_all(Node,Trans)
552 ).
553
554 :- public cltl_callback_reexplore/5.
555 % predicate used only in case POR is enabled
556 % to satisfy the cycle condition
557 % at this moment of the call the node has already been explored
558 % and we need to apply the rest of the enabled events at node
559 % to force the full exploration of it
560 cltl_callback_reexplore(Node,Aps,Out,Queries,Specs) :-
561 check_aps(Queries,Node,Aps),
562 impl_trans_term_rest(Node,Trans),
563 check_tps(Trans,Specs,Node,Out),
564 debug_println(8,cltl_callback_reexplore(Node,Aps,Out,Queries,Specs)).
565
566 impl_trans_term_rest(Node,Trans) :-
567 get_all_already_explored_transitions(Node,Ops_so_far),
568 state_space: compute_transitions_if_necessary_saved(From),
569 findall(op(Id,ActionAsTerm,To),
570 (transition(From,ActionAsTerm,Id,To),nonmember(op(Id,ActionAsTerm,To),Ops_so_far)),
571 Trans).
572
573 get_all_already_explored_transitions(Node,Ops) :-
574 findall(op(Id,ActionAsTerm,To),
575 transition(Node,ActionAsTerm,Id,To),Ops).
576
577 % check list of atomic propositions (ap)
578 check_aps([],_,[]).
579 check_aps([Query|QRest],Node,[Result|RRest]) :-
580 (check_ap(Query,Node) -> !,Result=1; Result=0),
581 check_aps(QRest,Node,RRest).
582
583 % check list of transition properties:
584 % check_tps(+Transitions, +Specifications, +State, -Result):
585 % "Transitions" is a list of terms of the form op(Id,Operation,NextState)
586 % each term represents a transition from "State" to "NextState",
587 % with the id "Id" and operation "Operation"
588 % "Specifications" is a list of propositions on transistions (tp)
589 % "Result" is a list where each element corresponds to a transition in "Transitions"
590 % each entry has the form "trans(Next,Id,ResVector)" where "Next" and "Id"
591 % are the destination state and the id of the transition, respectively, and
592 % "ResVector" a list where each element corresponds to a proposition (tp)
593 % in "Specifications". It is 0 resp. 1 if the proposition is false resp. true.
594 check_tps([],_,_,[]).
595 check_tps([op(Id,Op,Next)|OpRest],Specs,Node,[trans(Next,Id,Tp)|TpRest]) :-
596 check_tps2(Specs,Node,Next,Op,Tp),
597 check_tps(OpRest,Specs,Node,TpRest).
598 check_tps2([],_,_,_,[]).
599 check_tps2([Spec|SRest],SrcNode,DstNode,Op,[Result|RRest]) :-
600 (check_transition(Spec,Op,SrcNode,DstNode) -> !,Result=1; Result=0),
601 check_tps2(SRest,SrcNode,DstNode,Op,RRest).
602
603 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
604 %
605
606 ltl_formula_structure(Formula,Atomics,Structure) :-
607 c_ltl_aptp(Formula,ApTp),
608 pp_formulas(ApTp,Atomics),
609 ltl_structure(Formula,ApTp,Structure).
610
611 ltl_structure(fairnessimplication(_FAssumptions,F),Subformulas,Structure) :- !,
612 ltl_structure(F,Subformulas,Structure).
613 ltl_structure(ap(AP),Subformulas,ap(N)) :-
614 !,nth0(N,Subformulas,ap(AP)),!.
615 ltl_structure(action(TP),Subformulas,tp(N)) :-
616 !,nth0(N,Subformulas,action(TP)),!.
617 ltl_structure(F,ApTp,N) :-
618 F =.. [Functor|Args],
619 same_length(Args,NewArgs),
620 N =.. [Functor|NewArgs],
621 ltl_structure_l(Args,ApTp,NewArgs).
622 ltl_structure_l([],_,[]).
623 ltl_structure_l([F|Frest],ApTp,[N|Nrest]) :-
624 ltl_structure(F,ApTp,N),
625 ltl_structure_l(Frest,ApTp,Nrest).
626
627 % used by prob2_do_ltl_modelcheck (cf. groovyTests/ltlTest.groovy):
628 % Max is the maximum number of new nodes that will be explored; -1 means no limit
629 ltl_model_check_with_ce(Formula,Max,Mode,Result) :-
630 ltl_model_check_ast(Formula,Max,Mode,TypeOfMC,R1),
631 ce_result(R1,Mode,Formula,TypeOfMC,Result).
632
633 ce_result(nostart,_,_,_,nostart) :- !.
634 ce_result(none,_,_,_,ok) :- !.
635 ce_result(incomplete,_,_,_,incomplete) :- !.
636 ce_result(model(CE,LoopEntry),Mode,Formula,TypeOfMC,counterexample(Counterexample,LoopEntry,PathToCE)) :- !,
637 (ce_result_initpath(CE,Mode,PathToCE) -> true
638 ; add_error(ltl,'Could not find path to counter example: ', CE),fail),
639 (TypeOfMC=safety_ltl_mc -> N=0
640 ; c_ltl_aptp(Formula,ApTp), % list of atomic and transition propositions of Formula
641 length(ApTp,N)
642 ),
643 (convert_counterexample(CE,N,Counterexample)
644 -> true
645 ; add_error(ltl,'CE conversion failed: ', CE),fail).
646 ce_result(Result,_,_,_,_) :-
647 add_error(ltl,'Internal error: Unexpected result: ', Result),
648 fail.
649
650 :- use_module(probsrc(tcltk_interface),[find_shortest_trace_to_node/4]).
651 ce_result_initpath(CE,Mode,Path) :-
652 ce_get_first_state(CE,InitState),
653 (find_trace_to_initial_state(InitState,[root|StatePath]) -> true
654 ; Mode=specific_node(_), % we have started LTL model checking in another node
655 find_shortest_trace_to_node(root,InitState,_,StatePath)
656 ),
657 find_operation_ids(StatePath,root,Path).
658 find_operation_ids([],_,[]).
659 find_operation_ids([Dst|Srest],Src,[(Id,Op,Dst)|Irest]) :-
660 transition(Src,Op,Id,Dst),
661 find_operation_ids(Srest,Dst,Irest).
662
663 /* just restrict the evaluation bits to the atomic formulas */
664 convert_counterexample([],_N,[]).
665 convert_counterexample([atom(State,Evals,NextOp) |Arest],N,
666 [atom(State,NEvals,OpTuple)|Erest]) :-
667 (prefix_length(Evals,NEvals,N) -> true
668 ; add_warning(ltl,'Atom eval list is wrong: ',Evals), % the NEvals list does not seem to be used anywhere??
669 NEvals=Evals),
670 (NextOp = none -> OpTuple = none ; transition(State,Action,NextOp,Dst),OpTuple=(NextOp,Action,Dst)),
671 convert_counterexample(Arest,N,Erest).
672
673 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
674
675 % dynamic predicate for saving the LTL counterexamples for the Tcl/Tk interface
676 :- dynamic ltl_counter_examples_cache/4.
677
678 ltl_model_check_with_ce1(Proc,FormulaAsAtom,Max,Mode,Result) :-
679 debug_println(19,parsing_ltl_formula(FormulaAsAtom)),
680 (temporal_parser(FormulaAsAtom,ltl,Ltl) -> true ; add_error_fail(ltl,'LTL Parser failed: ',FormulaAsAtom)),
681 debug_println(19,checking_ltl_formula(Ltl)),
682 ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,Result).
683
684 ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,ActionTrace) :-
685 debug_println(19,initialising_ltlc2(Max,Mode)),
686 ( Ltl=syntax_error ->
687 ActionTrace=syntax_error
688 ;
689 interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result),
690 convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace)
691 ).
692
693 :- use_module(probsrc(user_interrupts),[catch_interrupt_assertion_call/1]).
694 :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
695 interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result) :-
696 user_interruptable_call_det(
697 catch_interrupt_assertion_call(ltl:ltl_model_check_ast(Ltl,Max,Mode,_,Result)),InterruptResult),
698 (InterruptResult=interrupted ->
699 Result=interrupted
700 ; (real_error_occurred ->
701 print_error('% *** Errors occurred while LTL model checking ! ***'),nl,nl,fail
702 ; print('LTL assertion check completed.'),nl)).
703
704 convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace) :-
705 ( Result = model(CE,LoopEntry) ->
706 pp_ltl_counterexample(LoopEntry,CE,ActionTrace),
707 (ltl_counter_examples_cache(Proc,Ltl,Mode,_) -> true; assertz(ltl_counter_examples_cache(Proc,Ltl,Mode,Result)))
708 ; Result = interrupted ->
709 ActionTrace = interrupted
710 ;
711 convert_result(Result,Mode,ActionTrace)).
712
713 pp_ltl_counterexample(deadlock,Counterexample,ce(Trace)) :- !,
714 length(Counterexample,N),
715 (N >= 2 ->
716 maplist(get_operation_name,Counterexample,Trace1),
717 ajoin_with_sep(Trace1,' -> ',Trace)
718 ;
719 Trace = deadlock).
720 pp_ltl_counterexample(no_loop,Counterexample,ce(Trace)) :- !,
721 maplist(get_operation_name,Counterexample,Trace1),
722 ajoin_with_sep(Trace1,' -> ',Trace).
723 pp_ltl_counterexample(loop(N),Counterexample,ce(Trace)) :- !,
724 prefix_length(Counterexample,PathToCE,N),
725 maplist(get_operation_name,PathToCE,PrefixTrace),
726 ajoin_with_sep(PrefixTrace,' -> ',PrefixTrace1),
727 append(PathToCE,CEPath,Counterexample),
728 maplist(get_operation_name,CEPath,SuffixTrace),
729 ajoin_with_sep(SuffixTrace,' -> ',SuffixTrace1),
730 ajoin([PrefixTrace1,' -> (',SuffixTrace1,')+'],Trace).
731 pp_ltl_counterexample(LoopEntry,_Counterexample,_CE) :-
732 add_error_fail(ltl, 'Internal error: unknown loop entry type: ', LoopEntry).
733
734 get_operation_name(atom(State,NEvasl,OpId),Res) :-
735 (OpId = none
736 -> Res = '|'
737 ; transition(State,Op,OpId,_NextState) ->
738 translate_event(Op,Res)
739 ;
740 add_error_fail(ltl_assertions_result, 'Internal Error: unknown operation in CE trace ', atom(State,NEvasl,OpId))).
741
742
743 tcltk_play_ltl_counterexample(Proc,Ltl) :-
744 ltl_counter_examples_cache(Proc,Ltl,Mode,model(CE,_Entry)),
745 translate_ctrace(CE,Op,N,Dest),
746 ( (Mode = init; Mode = checkhere) ->
747 ce_get_first_state(CE,UsedInitState),
748 set_trace_to_init(UsedInitState)
749 ; Mode = specific_node(NodeID) ->
750 set_trace_to_init(NodeID)
751 ;
752 true
753 ),execute_id_trace_from_current(Dest,Op,N).
754 tcltk_play_ltl_counterexample(Proc,Ltl) :-
755 add_error_fail(ltl_counter_example, 'Internal error: No counterexample has been asserted for the following configuration: ',(Proc,Ltl)).
756
757 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
758 % verify a counter-example
759
760 callback_tp(TP,StateId,TransId) :-
761 ( transition(StateId,Op,TransId,DestId) ->
762 check_transition(TP,Op,StateId,DestId)
763 ;
764 add_error(ltl,'Internal error: callback_tp called for unknown transition: ',
765 state_trans(StateId,TransId)),
766 fail
767 ).
768
769 call_ltl_verification(model(Atoms,Status),Formula) :-
770 !,call_ltl_verification2(Status,Atoms,Formula).
771 call_ltl_verification(_,_Formula).
772
773 call_ltl_verification2(Status,Atoms,Formula) :-
774 maplist(convert_atom_to_statetransition,Atoms,StateTransitions),!,
775 ( evaluate_ltl_formula(Formula,StateTransitions,Status,
776 check_ap,callback_tp,Result) ->
777 (Result = true -> true ; add_error(ltl,'Evaluation of LTL yielded unexpected result: ',Result))
778 ;
779 add_error(ltl,'Evaluation of LTL formula failed: ',Formula)).
780 call_ltl_verification2(_,Atoms,_) :-
781 add_error(ltl,'Evaluation of LTL yielded unexpected atoms: ',Atoms).
782
783 convert_atom_to_statetransition(atom(NodeId,_,TransId),strans(NodeId,TransId)).
784
785
786 % fairness
787 is_fairness_implication(fairnessimplication(_FAssumptions,_F)).
788
789 call_ltl_fairness_verification(model(Atoms,Status),WeakDNF,StrongDNF) :-
790 !,maplist(convert_atom_to_statetransition,Atoms,ST),
791 call_ltl_fairness_verification1(WeakDNF,weak,ST,Status),
792 call_ltl_fairness_verification1(StrongDNF,strong,ST,Status).
793 call_ltl_fairness_verification(_,_WeakDNF,_StrongDNF).
794
795 call_ltl_fairness_verification1([],_Type,_ST,_Status) :- !.
796 call_ltl_fairness_verification1(all,Type,ST,Status) :- !,
797 get_fairness_specification(Status,ST,Assumption),
798 call_ltl_fairness_verification1(Assumption,Type,ST,Status).
799 call_ltl_fairness_verification1(DNF,Type,ST,Status) :-
800 ( call_ltl_fairness_verification2(DNF,Type,ST,Status,Result) ->
801 true
802 ;
803 add_error(ltl,'Evalutation of LTL fairness failed: ',Type/DNF)),
804 ( Result = fair -> true
805 ;
806 print(Type/DNF),nl,
807 add_error(ltl,'Evaluation of LTL yields that the result violates fairness: ',Type/Result)).
808
809 call_ltl_fairness_verification2([],_Type,_ST,_Status,unfair([])).
810 call_ltl_fairness_verification2([Clause|CRest],Type,ST,Status,Result) :-
811 call_ltl_fairness_verification3(Clause,Type,ST,Status,CResult),
812 ( CResult = fair -> Result=fair
813 ; CResult = unfair(Cause) ->
814 call_ltl_fairness_verification2(CRest,Type,ST,Status,RResult),
815 ( RResult = fair -> Result=fair
816 ; RResult = unfair(Causes) -> Result=unfair([Cause|Causes]))).
817 call_ltl_fairness_verification3([],_Type,_ST,_Status,fair).
818 call_ltl_fairness_verification3([Spec|SRest],Type,ST,Status,Result) :-
819 evaluate_ltl_fairness(Type,ST,Status,ev_fairness_id(Spec),ev_fairness_id(Spec),LResult),
820 ( LResult = fair ->
821 call_ltl_fairness_verification3(SRest,Type,ST,Status,Result)
822 ; LResult = unfair(Id) ->
823 Result = unfair(Id)
824 ;
825 add_error_fail(ltl,'Unknown result after fairness verification check: ', evaluate_ltl_fairness(Type,ST,Status,ev_fairness_id(Spec),LResult))).