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		:- module(ltl_propositions,[check_ap/2, % testing atomic preposition in a state
6		is_atomic_ltl_property/1,
7		check_atomic_property_formula/2,
8		check_transition_pred/5, % testing whether a transition proposition can be executed from some state
9		check_enabled/2,
10		non_det_output_transition/4,
11		trans/4, % exported for use in ctl.pl
12		get_por_preferences/1
13		]).
14
15		/* SICSTUS Libraries */
16		:- use_module(library(lists)).
17
18		/* ProB standard modules */
19		% B
20		:- use_module(probsrc(kernel_objects),[equal_object/2, not_equal_object/2, less_than/2, greater_than/2,
21		strict_subset_of/2]).
22		:- use_module(probsrc(bsyntaxtree), [create_texpr/4, def_get_texpr_id/2]). % used for test cases
23		:- use_module(probsrc(bmachine),[b_get_machine_operation/4]).
24		:- use_module(probsrc(b_interpreter),[b_compute_expression_nowf/6, b_test_boolean_expression_cs/5]).
25		% state space modules
26		:- use_module(probsrc(state_space),[impl_trans_term/3, impl_trans_term/4,
27		visited_expression/2,
28		state_error/3, %transition/3,
29		is_concrete_constants_state_id/1,
30		impl_trans_id/4, transition_info/2,
31		state_space_add/2, retract_visited_expression/2 % used for test cases
32		]).
33		:- use_module(probsrc(store),[empty_state/1,lookup_value/3,add_var_to_localstate/4]).
34		:- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/2]).
35		% utility modules
36		:- use_module(probsrc(error_manager)).
37		:- use_module(probsrc(debug),[debug_format/3]).
38		:- use_module(probsrc(self_check)).
39		% Promela
40		%:- use_module(probpromela(promela_tools),[eval_promela/4]).
41		% other
42		:- use_module(probsrc(eclipse_interface),[test_boolean_expression_in_node/3]).
43
44		/* ProB LTL modules */
45		:- use_module(probltlsrc(ltl_tools)).
46		:- use_module(probltlsrc(ltl_translate),[pp_ltl_formula/2]).
47
48		:- use_module(probsrc(module_information),[module_info/2]).
49		:- module_info(group,ltl).
50		:- module_info(description,'This module provides predicates for evaluating atomic and transition prepositions.').
51
52		:- use_module(probsrc(model_checker),[node_satisfies_goal/1]).
53		:- use_module(probsrc(specfile),[property/2]).
54		% check an atomic proposition in a given node (i.e. state)
55		check_ap(bpred(Property),Node) :-
56		!, test_boolean_expression_in_node(Node,Property,'LTL atomic proposition').
57		%check_ap(promela_pred(Predicate),Node) :-
58		% visited_expression(Node,State),!,
59		% eval_promela(Predicate,global,State,Result),!,
60		% ( Result == 0 -> fail
61		% ; number(Result) -> true
62		% ; add_error(ltl,'Promela eval returned a non-boolean value: ',Result),fail).
63		check_ap(enabled(Op),Node) :- !,
64		check_enabled(Op,Node).
65		check_ap(det(OpList),Node) :- !,
66		check_if_maximum_one_enabled(OpList,Node).
67		check_ap(dlk(OpList),Node) :- !,
68		check_if_all_disabled(OpList,Node).
69		check_ap(ctrl(OpList),Node) :- !,
70		is_exactly_one_operation_enabled(OpList,Node).
71		check_ap(det_output,Node) :- !,
72		\+ non_det_output_transition(Node,_,_TID1,_TID2).
73	?	check_ap(deadlock,Node) :- !, \+ trans(Node,_,_,_).
74		check_ap(goal,Node) :- !, node_satisfies_goal(Node).
75		check_ap(state_error,Node) :- !, state_error(Node,_StateErrId,_Error).
76		check_ap(sink,Node) :- !,
77	?	\+ ( trans(Node,Next,_,_),Next \= Node ).
78		check_ap(stateid(SpecNode),Node) :- !, SpecNode = Node.
79		check_ap(xtl_predicate_check(Prop),Node) :-
80		visited_expression(Node,State),!,
81	?	property(State,Prop).
82		% available(.) is not covered here; it is covered in ltlc.pl; it is Gavin Lowe's available operator
83		check_ap(X,Node) :- visited_expression(Node,_),!,
84		add_internal_error('Unknown atomic proposition:',check_ap(X,Node)),fail.
85		check_ap(X,Node) :- add_internal_error('Unknown state:',check_ap(X,Node)),fail.
86
87
88		check_if_maximum_one_enabled(OpList,Node) :-
89		check_if_maximum_one_enabled(OpList,0,Node).
90
91		check_if_maximum_one_enabled([],_NrEnabled,_Node).
92		check_if_maximum_one_enabled([Op|Ops],NrEnabled,Node) :-
93		(check_enabled(Op,Node) ->
94		NrEnabled == 0, NrEnabled1 = 1
95		; NrEnabled1 = 0
96		), check_if_maximum_one_enabled(Ops,NrEnabled1,Node).
97
98		is_exactly_one_operation_enabled(OpList,Node) :-
99		is_exactly_one_operation_enabled(OpList,0,Node).
100
101		is_exactly_one_operation_enabled([],NrEnabled,_Node) :-
102		NrEnabled=1.
103		is_exactly_one_operation_enabled([Op|Ops],NrEnabled,Node) :-
104		(check_enabled(Op,Node) ->
105		NrEnabled == 0, NrEnabled1 = 1
106		; NrEnabled1 = NrEnabled
107		), is_exactly_one_operation_enabled(Ops,NrEnabled1,Node).
108
109		check_if_all_disabled([],_Node).
110		check_if_all_disabled([Op|Ops],Node) :-
111		\+check_enabled(Op,Node),
112		check_if_all_disabled(Ops,Node).
113
114		check_enabled(Spec,SrcNode) :-
115	?	trans(SrcNode,DestNode,Transition,TransId),
116	?	check_transition_pred(Spec,Transition,SrcNode,TransId,DestNode),!.
117
118		% ----------------
119
120		:- use_module(probsrc(specfile),[get_operation_name/2,
121		get_operation_arguments/2, get_operation_return_values_and_arguments/3]).
122
123		% check if there are two transition for OperationName with same args but different return result
124		% only works in b_mode
125		non_det_output_transition(ID,OperationName,TID1,TID2) :-
126	?	impl_trans_id(ID,Transition,TID1,_ID1),
127		get_operation_name(Transition,OperationName),
128		get_operation_return_values_and_arguments(Transition,Results1,OperationArgs),
129		Results1 \= [], % otherwise we have no return value
130	?	impl_trans_id(ID,Transition2,TID2,_ID2),
131		TID2 > TID1,
132		% note: here we do not care whether ID1 \= ID2,
133		get_operation_name(Transition2,OperationName), % same operation
134		get_operation_return_values_and_arguments(Transition2,Results2,OperationArgs), % same arguments
135		Results1 \= Results2. % Should we use equal_object ?
136
137		% ----------------
138
139	?	trans(A,B,Op,TransID) :- impl_trans_term(A,Op,TransID,B).
140		% THE FOLLOWING CODE IS BROKEN: TO DO FIX or REMOVE ; already removed use_por_for_ltl preference
141		%:- use_module(probltlsrc(ample_sets),[compute_ample_set2/2]).
142		%trans(A,B,Op,Tid) :-
143		% ( (preference(use_por_for_ltl,true), animation_mode(b))
144		% -> get_por_preferences(POROptions), % poor implementation (ltl predicates should not be called from here)
145		% ample_sets: compute_ample_set2(A,POROptions), % TO DO : THIS HAS 3 ARGUMENTS !!!
146		% transition(A,Op,Tid,B) % from state_space.pl
147		% ; impl_trans_term(A,Op,B,Tid) /* will automatically compute as required */
148		% ).
149
150		:- use_module(probsrc(preferences),[get_preference/2]).
151		get_por_preferences(por(TYPE,UseEnableGraph,Depth,UsePGE)) :-
152		get_preference(por,TYPE),
153		get_preference(enable_graph,UseEnableGraph),
154		get_preference(enable_graph_depth,Depth),
155		UsePGE = off.
156
157		is_atomic_ltl_property(ap(_)).
158		is_atomic_ltl_property(false).
159		is_atomic_ltl_property(true).
160		is_atomic_ltl_property(not(P1)) :- is_atomic_ltl_property(P1).
161		is_atomic_ltl_property(and(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).
162		is_atomic_ltl_property(or(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).
163		is_atomic_ltl_property(equivalent(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).
164		is_atomic_ltl_property(implies(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).
165
166		% a utility to check restricted atomic LTL properties on single nodes
167		check_atomic_property_formula(ap(ParsedFormula),NodeId) :- !,
168		check_ap(ParsedFormula,NodeId).
169		%check_atomic_property_formula(ap(ParsedFormula),NodeId) :- !,
170		check_atomic_property_formula(and(P1,P2),NodeId) :- !,
171		check_atomic_property_formula(P1,NodeId),
172		check_atomic_property_formula(P2,NodeId).
173		check_atomic_property_formula(or(P1,P2),NodeId) :- !,
174		(check_atomic_property_formula(P1,NodeId) -> true
175		; check_atomic_property_formula(P2,NodeId)).
176		check_atomic_property_formula(implies(P1,P2),NodeId) :- !,
177		(check_atomic_property_formula(P1,NodeId)
178		-> check_atomic_property_formula(P2,NodeId) ; true).
179		check_atomic_property_formula(equivalent(P1,P2),NodeId) :- !,
180		(check_atomic_property_formula(P1,NodeId)
181		-> check_atomic_property_formula(P2,NodeId)
182		; \+ check_atomic_property_formula(P2,NodeId)).
183		check_atomic_property_formula(not(P1),NodeId) :- !,
184		(check_atomic_property_formula(P1,NodeId) -> fail ; true).
185		check_atomic_property_formula(true,_) :- !.
186		check_atomic_property_formula(false,_) :- !,fail.
187		check_atomic_property_formula(Formula,_) :- %print(Formula),nl,
188		pp_ltl_formula(Formula,Text),!,
189		add_error(check_atomic_property_formula,'LTL formula is not an atomic property: ',Text).
190		check_atomic_property_formula(Formula,N) :-
191		add_internal_error('LTL formula invalid: ',check_atomic_property_formula(Formula,N)),fail.
192
193
194
195		% check_transition_pred(Spec,Transition,SrcNode,TransId,DstNode)
196		% Checks if a transition fulfils the specification, it fails if not.
197		% Please note, that this predicate is called _before_ the actual transition
198		% is known.
199		% Spec: specification that encodes how the transition should look like
200		% See below for the supported transitions
201		% Transition: The transition itself as it is stored in the second arg of state_space:transition/3
202		% SrcNode: The Id of the source state (first arg of transition/3)
203		% DstNode: The Id of the destination state (third arg of transition/3)
204
205
206		:- assert_must_succeed( check_transition(bop(dummyop,2,0,[],[]),dummyop(int(1),int(2)),tsrc,tdst) ).
207		:- assert_must_fail( check_transition(bop(dummyop,2,0,[],[]),otherop(int(1),int(2)),tsrc,tdst) ).
208		:- assert_must_fail( check_transition(bop(dummyop,2,0,[],[]),dummyop(int(1)),tsrc,tdst) ).
209		:- assert_must_succeed(call_cleanup(( empty_state(E),
210		state_space_add(tsrc,E),
211		create_texpr(integer(2),integer,[],I2),
212		check_transition(bop(dummyop,2,0,[2/I2],[]),
213		dummyop(int(1),int(2)),tsrc,tdst)),
214		retract_visited_expression(tsrc,_))).
215		:- assert_must_fail(call_cleanup(( empty_state(E),
216		state_space_add(tsrc,E),
217		create_texpr(integer(2),integer,[],I2),
218		check_transition(bop(dummyop,2,0,[1/I2],[]),
219		dummyop(int(1),int(2)),tsrc,tdst)),
220		retract_visited_expression(tsrc,_))).
221		:- assert_must_succeed( check_transition(bop(dummyop,1,1,[],[]),'-->'(dummyop(int(1)),[int(2)]),tsrc,tdst) ).
222		:- assert_must_fail( check_transition(bop(dummyop,1,1,[],[]),dummyop(int(1)),tsrc,tdst) ).
223		:- assert_must_succeed(call_cleanup(( empty_state(E),
224		state_space_add(tsrc,E),
225		create_texpr(integer(2),integer,[],I2),
226		check_transition(bop(dummyop,1,1,[],[1/I2]),
227		'-->'(dummyop(int(1)),[int(2)]),tsrc,tdst)),
228		retract_visited_expression(tsrc,_))).
229		:- assert_must_fail(call_cleanup(( empty_state(E),
230		state_space_add(tsrc,E),
231		create_texpr(integer(2),integer,[],I2),
232		check_transition(bop(dummyop,1,1,[],[1/I2]),
233		'-->'(dummyop(int(1)),[int(1)]),tsrc,tdst)),
234		retract_visited_expression(tsrc,_))).
235
236		% first transition predicates which require access to the transition id:
237		check_transition_pred(operation_call(OpCall),Transition,SrcNode,TransId,DstNode) :-
238		!, % check if subsidiary operation called
239		(transition_info(TransId,path(Path)) % path, eventtrace, event
240		-> debug_format(9,'Checking subsidiary opcall : ~w for transition id ~w : ~w~n',[OpCall,TransId, Path]),
241		(path_contains_operation_call(Path,matchop(SrcNode,OpCall)) -> true
242		; check_transition(OpCall, Transition,SrcNode,DstNode)
243		-> true % user has actually used it not for a subsidiary operation call but for the top-level call;
244		% should we warn the user?
245		)
246		; fail
247		).
248		check_transition_pred(Spec,Transition,SrcNode,_TransId,DstNode) :-
249	?	check_transition(Spec,Transition,SrcNode,DstNode).
250
251		:- use_module(library(terms),[sub_term/2]).
252		path_contains_operation_call(path(S),Pat) :- !, path_contains_operation_call(S,Pat).
253		path_contains_operation_call([H|T],Pat) :- !, member(S,[H|T]), path_contains_operation_call(S,Pat).
254		path_contains_operation_call(parallel(L),Pat) :- !, member(S,L), path_contains_operation_call(S,Pat).
255		path_contains_operation_call(sequence(A,B),Pat) :- !, member(S,[A,B]), path_contains_operation_call(S,Pat).
256		path_contains_operation_call(assertion(S),Pat) :- !, path_contains_operation_call(S,Pat).
257		path_contains_operation_call(pre(_,S),Pat) :- !, path_contains_operation_call(S,Pat).
258		path_contains_operation_call(choice(_,S),Pat) :- !, path_contains_operation_call(S,Pat).
259		path_contains_operation_call(if(_,S),Pat) :- !, path_contains_operation_call(S,Pat).
260		path_contains_operation_call(select(_,S),Pat) :- !, path_contains_operation_call(S,Pat).
261		path_contains_operation_call(let(S),Pat) :- !, path_contains_operation_call(S,Pat).
262		path_contains_operation_call(any(_,S),Pat) :- !, path_contains_operation_call(S,Pat).
263		path_contains_operation_call(var(_,S),Pat) :- !, path_contains_operation_call(S,Pat).
264		path_contains_operation_call(operation_call(Name,_ResultNames,Paras,ReturnValues, Path),Pat) :- !,
265		%write(opcall(Name)),nl,
266		(Pat = matchop(SrcNode,bop(Name,_NumberArgs,_NumberResults,ArgPatterns,ResPatterns)),
267		Op =.. [Name|Paras],
268		check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op), % State instantiated upon demand
269		check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues)
270		-> true
271		; path_contains_operation_call(Path,Pat)).
272		%path_contains_operation_call(Term,Pat) :- Term =.. [F|Args], write(unknown_functor(F)),nl,
273		% member(S,Args), path_contains_operation_call(S,Pat).
274
275		% bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns):
276		% The transition is a B operation with name Name, NumberArgs parameters and NumberResults
277		% result values.
278		% ArgPatterns is a list of Terms of the form Index/Expr where Index is the
279		% number of the parameter that should have the value of the expression Expr.
280		% ResPatterns is a list analogous to ArgPatterns on the result
281		check_transition(bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),
282		Transition,SrcNode,_DstNode) :-
283		!, functor(Op,Name,NumberArgs),
284		( NumberResults == 0 -> Transition = Op
285		;
286		Transition = '-->'(Op,ReturnValues),
287		length(ReturnValues,NumberResults),
288		check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues)),
289		check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op).
290		check_transition(btrans(TransPred),Transition,SrcNode,DstNode) :-
291		!, check_eventb_transition(TransPred,Transition,SrcNode,DstNode).
292		check_transition(change_expr(Comp,TExpr),Transition,SrcNode,DstNode) :-
293		!, check_change_expr_transition(Comp,TExpr,Transition,SrcNode,DstNode).
294		check_transition(before_after(TPred),Transition,SrcNode,DstNode) :-
295		!, check_before_after_transition(TPred,Transition,SrcNode,DstNode).
296		check_transition(csp(Channel,Arity,Args),Transition,_SrcNode,_DstNode) :-
297	?	!, check_csp_event(Channel,Arity,Args,Transition).
298		check_transition(xtl(Op,Arity,PatternArgs),Transition,_SrcNode,_DstNode) :-
299		!, check_xtl_transition(Op,Arity,PatternArgs,Transition).
300		check_transition(Spec,_Trans,_SrcNode,_DstNode) :-
301		functor(Spec,Name,Arity), add_error(ltl, 'Unknown transition specification: ', Name/Arity), fail.
302		% TODO: add non_det_output(OpName) for a transition
303
304		:- block check_xtl_transition(?,?,?,-).
305		check_xtl_transition(Op,Arity,PatternArgs,Transition) :-
306		( Arity=0 ->
307		functor(Transition,Op,_) /* in this case: pattern match any operation with right number of args */
308		; %functor(Transition,Op,Arity),
309		Transition =.. [Op|Args],
310		check_xtl_arguments(Args,PatternArgs)
311		).
312
313		check_bop_arg_patterns([],_,_,_).
314		check_bop_arg_patterns([P|Prest],Node,State,Op) :-
315		check_bop_arg_patterns2([P|Prest],Node,State,Op).
316		:- block check_bop_arg_patterns2(?,?,?,-).
317		check_bop_arg_patterns2([],_,_,_).
318		check_bop_arg_patterns2([Index/Expr|Prest],Node,State,Op) :-
319		check_bop_arg_pattern(Index,Expr,Node,State,Op),
320		check_bop_arg_patterns2(Prest,Node,State,Op).
321		check_bop_arg_pattern(Index,Expr,Node,State,Op) :-
322		arg(Index,Op,OpValue), % exception if Index is expression like 1+1 <----
323		check_b_operation_value(OpValue,Expr,Node,State).
324
325		check_bop_res_patterns([],_,_,_).
326		check_bop_res_patterns([P|Prest],Node,State,OpResult) :-
327		check_bop_res_patterns2([P|Prest],Node,State,OpResult).
328		:- block check_bop_res_patterns2(?,?,?,-).
329		check_bop_res_patterns2([],_,_,_).
330		check_bop_res_patterns2([Index/Expr|Prest],Node,State,OpResult) :-
331		check_bop_res_pattern(Index,Expr,Node,State,OpResult),
332		check_bop_res_patterns2(Prest,Node,State,OpResult).
333		check_bop_res_pattern(Index,Expr,Node,State,OpResult) :-
334		nth1(Index,OpResult,OpValue),
335		check_b_operation_value(OpValue,Expr,Node,State).
336
337		check_b_operation_value(OpValue,Expr,Node,State) :-
338		( var(State) ->
339	?	visited_expression(Node,RawState),
340		state_corresponds_to_initialised_b_machine(RawState,State)
341		; true),
342		empty_state(LS),
343		b_compute_expression_nowf(Expr,LS,State,PatternValue,'LTL check operation value',0),
344		equal_object(PatternValue,OpValue),!.
345
346		% check if an expression is unchanged/changed/increasing/decreasing by a transition
347		:- block check_change_expr_transition(?,?,?,-,?), check_change_expr_transition(?,?,?,?,-).
348		% block is needed for safety_mc which calls check_transition with DstNode free before calling transition
349		check_change_expr_transition(Comp,_,_Transition,root,_DstNode) :- !, Comp=eq. % we assume initialisation is not a change
350		check_change_expr_transition(Comp,_,_Transition,SrcNode,_DstNode) :-
351		is_concrete_constants_state_id(SrcNode),!, Comp=eq. % we assume initialisation is not a change
352		check_change_expr_transition(Comp,TExpr,_Transition,SrcNode,DstNode) :- !,
353		% TO DO: provide optimized version for variable ids: just obtain value from unpacked state
354		%print(check_unchanged(SrcNode,DstNode,_Transition)),nl,
355		eval_expr_in_state(TExpr,SrcNode,BeforeValue),
356		eval_expr_in_state(TExpr,DstNode,AfterValue),
357		%print(unchanged(SrcNode,DstNode,BeforeValue,AfterValue)),nl,
358		compare_values(Comp,BeforeValue,AfterValue).
359
360		compare_values(eq,V1,V2) :- equal_object(V1,V2).
361		compare_values(neq,V1,V2) :- not_equal_object(V1,V2).
362		compare_values(lt,V1,V2) :- less_than_value(V1,V2).
363		compare_values(gt,V1,V2) :- less_than_value(V2,V1).
364
365		:- use_module(probsrc(kernel_reals),[is_real/1, real_less_than_wf/3]).
366		% move to external functions? maybe use leq_sym_break
367		% we could use something like 'LESS' which works on strings, sets, booleans, ...
368		less_than_value(int(V1),int(V2)) :- !, V1 < V2.
369		less_than_value(pred_false,V2) :- !, V2=pred_true.
370		less_than_value(pred_true,_) :- !, fail.
371		less_than_value(string(V1),string(V2)) :- !, V1 @< V2.
372		less_than_value(fd(V1,G),fd(V2,G)) :- !, V1 < V2.
373		less_than_value((V1a,V1b),(V2a,V2b)) :- !,
374		(less_than_value(V1a,V2a) -> true
375		; equal_object(V1a,V2a) -> less_than_value(V1b,V2b)).
376		less_than_value(V1,V2) :- is_set(V1), !, strict_subset_of(V1,V2).
377		less_than_value(R1,R2) :- is_real(R1), !, real_less_than_wf(R1,R2,no_wf_available).
378		% TODO: records, freetypes
379		less_than_value(V1,_) :- add_error(ltl,'Operator increasing/decreasing not supported for:',V1).
380
381		is_set([]).
382		is_set([_|_]).
383		is_set(avl_set(_)).
384		is_set(closure(_,_,_)).
385
386
387		eval_expr_in_state(TExpr,ID,Val) :-
388		visited_expression(ID,CurState),
389		state_corresponds_to_initialised_b_machine(CurState,CurBState),
390		empty_state(LS),
391		(b_compute_expression_nowf(TExpr,LS,CurBState,Res,'LTL unchanged expression',0) -> Res=Val
392		; add_warning(ltl,'Evaluation of unchanged expression failed: ',TExpr),
393		fail).
394
395		:- use_module(probsrc(specfile),[extract_variables_from_state_as_primed/2]).
396
397		get_primed_variable_state(SrcNode,PrimedVarBindings) :-
398		visited_expression(SrcNode,SrcState),
399		extract_variables_from_state_as_primed(SrcState,PrimedVarBindings).
400
401		% $0 refers to variables in current state, unprimed variables to target state
402		:- block check_before_after_transition(?,?,?,-).
403		check_before_after_transition(Predicate,_Transition,SrcNode,DstNode) :-
404		get_primed_variable_state(SrcNode,LocalState),
405		visited_expression(DstNode,DstState),
406		state_corresponds_to_initialised_b_machine(DstState,DstBState),
407		b_test_boolean_expression_cs(Predicate,LocalState,DstBState,'LTL before-after',SrcNode).
408
409
410		:- block check_eventb_transition(?,-,?,?).
411		check_eventb_transition(event(Name),Transition,_SrcNode,_DstNode) :- !,
412		functor(Transition,Name,_).
413		check_eventb_transition(event(Name,Predicate,PoststateAccess),Transition,SrcNode,DstNode) :- !,
414		functor(Transition,Name,_),
415		visited_expression(SrcNode,CurState),
416		state_corresponds_to_initialised_b_machine(CurState,CurBState),
417		parameter_values(Transition,LocalState1),
418		add_post_state_values(PoststateAccess,DstNode,LocalState1,LocalState),
419		b_test_boolean_expression_cs(Predicate,LocalState,CurBState,'LTL event transition',SrcNode).
420		% TODO: we could add a transition to check if a variable or expression was modified
421
422		add_post_state_values([],_DstNode,State,State) :- !.
423		add_post_state_values(Access,Node,InState,OutState) :-
424		visited_expression(Node,DstState1),
425		state_corresponds_to_initialised_b_machine(DstState1,DstState),
426		add_post_state_values2(Access,DstState,InState,OutState).
427		add_post_state_values2([],_DstState,State,State).
428		add_post_state_values2([poststate(Orig,Primed)|Prest],DstState,InState,OutState) :-
429		lookup_value(Orig,DstState,Value),
430		add_var_to_localstate(Primed,Value,InState,InterState),
431		add_post_state_values2(Prest,DstState,InterState,OutState).
432
433		parameter_values(Transition,LocalState) :-
434		Transition =.. [Name|Arguments],
435		b_get_machine_operation(Name,_,Parameters,_),
436		empty_state(Empty),
437		add_parameter_values2(Parameters,Arguments,Empty,LocalState).
438		add_parameter_values2([],[],State,State).
439		add_parameter_values2([TParameter|Prest],[Argument|Arest],InState,OutState) :-
440		def_get_texpr_id(TParameter,Parameter),
441		add_var_to_localstate(Parameter,Argument,InState,InterState),
442		add_parameter_values2(Prest,Arest,InterState,OutState).
443
444
445		check_xtl_arguments([],[]).
446		check_xtl_arguments([],[H|T]) :-
447		print('### Extra arguments in LTL/CTL pattern: '),print([H|T]),nl,fail.
448		check_xtl_arguments([_H|_T],[]).
449		% format('Ignoring extra argument(s) ~w in action, add .? to LTL/CTL pattern to get rid of this message.~n',[[H|T]]).
450		check_xtl_arguments([H|T],[PatH|PatT]) :-
451		check_xtl_arg(PatH,H,T,RemArgs),
452		check_xtl_arguments(RemArgs,PatT).
453
454		check_xtl_arg('_',_,TArgs,RemArgs) :- !,RemArgs=TArgs.
455		check_xtl_arg('?',_,TArgs,RemArgs) :- !,RemArgs=TArgs.
456		check_xtl_arg(X,Y,TArgs,RemArgs) :- atomic(Y),!,X=Y,RemArgs=TArgs.
457		check_xtl_arg(X,Y,TArgs,RemArgs) :- nonvar(Y),!,Y=..[Functor|YArgs], Functor=X,
458		append(YArgs,TArgs,RemArgs).
459		check_xtl_arg(X,Y,TArgs,RemArgs) :- var(Y),
460		print(variable_for_ltl_pattern(X)),nl,
461		X=Y,RemArgs=TArgs.