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