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