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,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),Formula,TypeOfMC,counterexample(Counterexample,LoopEntry,PathToCE)) :- !,
637		ce_result_initpath(CE,PathToCE),
638		(TypeOfMC=safety_ltl_mc -> N=0
639		; c_ltl_aptp(Formula,ApTp), % list of atomic and transition propositions of Formula
640		length(ApTp,N)
641		),
642		(convert_counterexample(CE,N,Counterexample) -> true
643		; add_error(ltl,'CE conversion failed: ', CE),fail).
644		ce_result(Result,_,_,_) :-
645		add_error(ltl,'Internal error: Unexpected result: ', Result),
646		fail.
647
648		ce_result_initpath(CE,Path) :-
649		ce_get_first_state(CE,InitState),
650		find_trace_to_initial_state(InitState,[root|StatePath]),
651		find_operation_ids(StatePath,root,Path).
652		find_operation_ids([],_,[]).
653		find_operation_ids([Dst|Srest],Src,[(Id,Op,Dst)|Irest]) :-
654		transition(Src,Op,Id,Dst),
655		find_operation_ids(Srest,Dst,Irest).
656
657		/* just restrict the evaluation bits to the atomic formulas */
658		convert_counterexample([],_N,[]).
659		convert_counterexample([atom(State,Evals,NextOp) |Arest],N,
660		[atom(State,NEvals,OpTuple)|Erest]) :-
661		(prefix_length(Evals,NEvals,N) -> true
662		; add_warning(ltl,'Atom eval list is wrong: ',Evals), % the NEvals list does not seem to be used anywhere??
663		NEvals=Evals),
664		(NextOp = none -> OpTuple = none ; transition(State,Action,NextOp,Dst),OpTuple=(NextOp,Action,Dst)),
665		convert_counterexample(Arest,N,Erest).
666
667		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
668
669		% dynamic predicate for saving the LTL counterexamples for the Tcl/Tk interface
670		:- dynamic ltl_counter_examples_cache/4.
671
672		ltl_model_check_with_ce1(Proc,FormulaAsAtom,Max,Mode,Result) :-
673		debug_println(19,parsing_ltl_formula(FormulaAsAtom)),
674		(temporal_parser(FormulaAsAtom,ltl,Ltl) -> true ; add_error_fail(ltl,'LTL Parser failed: ',FormulaAsAtom)),
675		debug_println(19,checking_ltl_formula(Ltl)),
676		ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,Result).
677
678		ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,ActionTrace) :-
679		debug_println(19,initialising_ltlc2(Max,Mode)),
680		( Ltl=syntax_error ->
681		ActionTrace=syntax_error
682		;
683		interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result),
684		convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace)
685		).
686
687		:- use_module(probsrc(user_interrupts),[catch_interrupt_assertion_call/1]).
688		:- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
689		interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result) :-
690		user_interruptable_call_det(
691		catch_interrupt_assertion_call(ltl:ltl_model_check_ast(Ltl,Max,Mode,_,Result)),InterruptResult),
692		(InterruptResult=interrupted ->
693		Result=interrupted
694		; (real_error_occurred ->
695		print_error('% *** Errors occurred while LTL model checking ! ***'),nl,nl,fail
696		; print('LTL assertion check completed.'),nl)).
697
698		convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace) :-
699		( Result = model(CE,LoopEntry) ->
700		pp_ltl_counterexample(LoopEntry,CE,ActionTrace),
701		(ltl_counter_examples_cache(Proc,Ltl,Mode,_) -> true; assertz(ltl_counter_examples_cache(Proc,Ltl,Mode,Result)))
702		; Result = interrupted ->
703		ActionTrace = interrupted
704		;
705		convert_result(Result,Mode,ActionTrace)).
706
707		pp_ltl_counterexample(deadlock,Counterexample,ce(Trace)) :- !,
708		length(Counterexample,N),
709		(N >= 2 ->
710		maplist(get_operation_name,Counterexample,Trace1),
711		ajoin_with_sep(Trace1,' -> ',Trace)
712		;
713		Trace = deadlock).
714		pp_ltl_counterexample(no_loop,Counterexample,ce(Trace)) :- !,
715		maplist(get_operation_name,Counterexample,Trace1),
716		ajoin_with_sep(Trace1,' -> ',Trace).
717		pp_ltl_counterexample(loop(N),Counterexample,ce(Trace)) :- !,
718		prefix_length(Counterexample,PathToCE,N),
719		maplist(get_operation_name,PathToCE,PrefixTrace),
720		ajoin_with_sep(PrefixTrace,' -> ',PrefixTrace1),
721		append(PathToCE,CEPath,Counterexample),
722		maplist(get_operation_name,CEPath,SuffixTrace),
723		ajoin_with_sep(SuffixTrace,' -> ',SuffixTrace1),
724		ajoin([PrefixTrace1,' -> (',SuffixTrace1,')+'],Trace).
725		pp_ltl_counterexample(LoopEntry,_Counterexample,_CE) :-
726		add_error_fail(ltl, 'Internal error: unknown loop entry type: ', LoopEntry).
727
728		get_operation_name(atom(State,NEvasl,OpId),Res) :-
729		(OpId = none
730		-> Res = '|'
731		; transition(State,Op,OpId,_NextState) ->
732		translate_event(Op,Res)
733		;
734		add_error_fail(ltl_assertions_result, 'Internal Error: unknown operation in CE trace ', atom(State,NEvasl,OpId))).
735
736
737		tcltk_play_ltl_counterexample(Proc,Ltl) :-
738		ltl_counter_examples_cache(Proc,Ltl,Mode,model(CE,_Entry)),
739		translate_ctrace(CE,Op,N,Dest),
740		( (Mode = init; Mode = checkhere) ->
741		ce_get_first_state(CE,UsedInitState),
742		set_trace_to_init(UsedInitState)
743		; Mode = specific_node(NodeID) ->
744		set_trace_to_init(NodeID)
745		;
746		true
747		),execute_id_trace_from_current(Dest,Op,N).
748		tcltk_play_ltl_counterexample(Proc,Ltl) :-
749		add_error_fail(ltl_counter_example, 'Internal error: No counterexample has been asserted for the following configuration: ',(Proc,Ltl)).
750
751		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
752		% verify a counter-example
753
754		callback_tp(TP,StateId,TransId) :-
755		( transition(StateId,Op,TransId,DestId) ->
756		check_transition(TP,Op,StateId,DestId)
757		;
758		add_error(ltl,'Internal error: callback_tp called for unknown transition: ',
759		state_trans(StateId,TransId)),
760		fail
761		).
762
763		call_ltl_verification(model(Atoms,Status),Formula) :-
764		!,call_ltl_verification2(Status,Atoms,Formula).
765		call_ltl_verification(_,_Formula).
766
767		call_ltl_verification2(Status,Atoms,Formula) :-
768		maplist(convert_atom_to_statetransition,Atoms,StateTransitions),!,
769		( evaluate_ltl_formula(Formula,StateTransitions,Status,
770		check_ap,callback_tp,Result) ->
771		(Result = true -> true ; add_error(ltl,'Evaluation of LTL yielded unexpected result: ',Result))
772		;
773		add_error(ltl,'Evaluation of LTL formula 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))).