1		% (c) 2009-2016 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_prepositions,[check_ap/2, % testing atomic preposition in a state
6		check_atomic_property_formula/2,
7		check_transition/4, % testing whether a transition proposition can be executed from some state
8		check_enabled/2,
9		trans/3 % exported for use in ctl.pl
10		]).
11
12		/* SICSTUS Libraries */
13		:- use_module(library(lists)).
14
15		/* ProB standard modules */
16		% B
17		:- use_module(probsrc(kernel_objects),[equal_object/2]).
18		:- use_module(probsrc(bsyntaxtree), [create_texpr/4, def_get_texpr_id/2]). % used for test cases
19		:- use_module(probsrc(bmachine),[b_get_machine_operation/4]).
20		:- use_module(probsrc(b_interpreter),[b_compute_expression/4,b_test_boolean_expression_wf/3]).
21		% state space modules
22		:- use_module(probsrc(state_space),[impl_trans_term/3,
23		visited_expression/2,
24		transition/3,
25		state_space_add/2,retract_visited_expression/2 % used for test cases
26		]).
27		:- use_module(probsrc(store),[empty_state/1,lookup_value/3,add_var_to_localstate/4]).
28		:- use_module(probsrc(specfile),[animation_mode/1,state_corresponds_to_initialised_b_machine/2]).
29		% utility modules
30		:- use_module(probsrc(preferences),[preference/2]).
31		:- use_module(probsrc(error_manager)).
32		:- use_module(probsrc(self_check)).
33		% Promela
34		:- use_module(probpromela(promela_tools),[eval_promela/4]).
35		% other
36		:- use_module(probsrc(eclipse_interface),[test_boolean_expression_in_node/2]).
37		:- use_module(probsrc(plugins),[plugin_evaluate_transition_predicate/3]).
38
39		/* ProB LTL modules */
40		:- use_module(probltlsrc(ltl_tools)).
41		:- use_module(probltlsrc(ltl_translate),[pp_ltl_formula/2]).
42
43		:- use_module(probsrc(module_information),[module_info/2]).
44		:- module_info(group,ltl).
45		:- module_info(description,'This module provides predicates for evaluating atomic and transition prepositions.').
46
47		% check an atomic proposition in a given node (i.e. state)
48		check_ap(bpred(Property),Node) :-
49		!, test_boolean_expression_in_node(Node,Property).
50		check_ap(promela_pred(Predicate),Node) :-
51		visited_expression(Node,State),!,
52		eval_promela(Predicate,global,State,Result),!,
53		( Result == 0 -> fail
54		; number(Result) -> true
55		; otherwise -> add_error(ltl,'Promela eval returned a non-boolean value: ',Result),fail).
56		check_ap(enabled(Op),Node) :- !,
57		check_enabled(Op,Node).
58		check_ap(det(OpList),Node) :- !,
59		check_if_maximum_one_enabled(OpList,Node).
60		check_ap(dlk(OpList),Node) :- !,
61		check_if_all_disabled(OpList,Node).
62		check_ap(ctrl(OpList),Node) :- !,
63		is_exactly_one_operation_enabled(OpList,Node).
64	?	check_ap(deadlock,Node) :- !, \+ trans(Node,_,_).
65		check_ap(sink,Node) :- !,
66		\+ ( trans(Node,Next,_),Next \= Node ).
67		check_ap(stateid(SpecNode),Node) :- !, SpecNode = Node.
68
69		check_if_maximum_one_enabled(OpList,Node) :-
70		check_if_maximum_one_enabled(OpList,0,Node).
71
72		check_if_maximum_one_enabled([],_NrEnabled,_Node).
73		check_if_maximum_one_enabled([Op|Ops],NrEnabled,Node) :-
74		(check_enabled(Op,Node) ->
75		NrEnabled == 0, NrEnabled1 = 1
76		; NrEnabled1 = 0
77		), check_if_maximum_one_enabled(Ops,NrEnabled1,Node).
78
79		is_exactly_one_operation_enabled(OpList,Node) :-
80		is_exactly_one_operation_enabled(OpList,0,Node).
81
82		is_exactly_one_operation_enabled([],NrEnabled,_Node) :-
83		NrEnabled=1.
84		is_exactly_one_operation_enabled([Op|Ops],NrEnabled,Node) :-
85		(check_enabled(Op,Node) ->
86		NrEnabled == 0, NrEnabled1 = 1
87		; NrEnabled1 = NrEnabled
88		), is_exactly_one_operation_enabled(Ops,NrEnabled1,Node).
89
90		check_if_all_disabled([],_Node).
91		check_if_all_disabled([Op|Ops],Node) :-
92		\+check_enabled(Op,Node),
93		check_if_all_disabled(Ops,Node).
94
95		check_enabled(Spec,SrcNode) :-
96		check_transition(Spec,Transition,SrcNode,DestNode),
97	?	trans(SrcNode,DestNode,Transition),!.
98
99		trans(A,B,Op) :-
100	?	( (preference(use_por_for_ltl,true), animation_mode(b))
101		-> ltl: get_por_preferences(POROptions), % poor implementation (ltl predicates should not be called from here)
102		user: compute_ample_set2(A,POROptions),
103		transition(A,Op,B) % from state_space.pl
104	?	; impl_trans_term(A,Op,B) /* will automatically compute as required */
105		).
106
107
108		% a utility to check restricted atomic LTL properties on single nodes
109		check_atomic_property_formula(ap(ParsedFormula),NodeId) :- !,
110		check_ap(ParsedFormula,NodeId).
111		%check_atomic_property_formula(ap(ParsedFormula),NodeId) :- !,
112		check_atomic_property_formula(and(P1,P2),NodeId) :- !,
113		check_atomic_property_formula(P1,NodeId),
114		check_atomic_property_formula(P2,NodeId).
115		check_atomic_property_formula(or(P1,P2),NodeId) :- !,
116		(check_atomic_property_formula(P1,NodeId) ;
117		check_atomic_property_formula(P2,NodeId)).
118		check_atomic_property_formula(implies(P1,P2),NodeId) :- !,
119		(check_atomic_property_formula(P1,NodeId)
120		-> check_atomic_property_formula(P2,NodeId) ; true).
121		check_atomic_property_formula(not(P1),NodeId) :- !,
122		(check_atomic_property_formula(P1,NodeId) -> fail ; true).
123		check_atomic_property_formula(Formula,_) :- %print(Formula),nl,
124		pp_ltl_formula(Formula,Text),!,
125		add_error(check_atomic_property_formula,'LTL formula is not an atomic property: ',Text).
126		check_atomic_property_formula(Formula,N) :-
127		add_internal_error('LTL formula invalid: ',check_atomic_property_formula(Formula,N)),fail.
128
129		% check_transition(Spec,Transition,SrcNode,DstNode)
130		% Checks if a transition fulfils the specification, it fails if not.
131		% Please note, that this predicate is called _before_ the actual transition
132		% is known.
133		% Spec: specification that encodes how the transition should look like
134		% See below for the supported transitions
135		% Transition: The transition itself as it is stored in the second arg of state_space:transition/3
136		% SrcNode: The Id of the source state (first arg of transition/3)
137		% DstNode: The Id of the destination state (third arg of transition/3)
138
139		:- assert_must_succeed( check_transition(bop(dummyop,2,0,[],[]),dummyop(int(1),int(2)),tsrc,tdst) ).
140		:- assert_must_fail( check_transition(bop(dummyop,2,0,[],[]),otherop(int(1),int(2)),tsrc,tdst) ).
141		:- assert_must_fail( check_transition(bop(dummyop,2,0,[],[]),dummyop(int(1)),tsrc,tdst) ).
142		:- assert_must_succeed(call_cleanup(( empty_state(E),
143		state_space_add(tsrc,E),
144		create_texpr(integer(2),integer,[],I2),
145		check_transition(bop(dummyop,2,0,[2/I2],[]),
146		dummyop(int(1),int(2)),tsrc,tdst)),
147		retract_visited_expression(tsrc,_))).
148		:- assert_must_fail(call_cleanup(( empty_state(E),
149		state_space_add(tsrc,E),
150		create_texpr(integer(2),integer,[],I2),
151		check_transition(bop(dummyop,2,0,[1/I2],[]),
152		dummyop(int(1),int(2)),tsrc,tdst)),
153		retract_visited_expression(tsrc,_))).
154		:- assert_must_succeed( check_transition(bop(dummyop,1,1,[],[]),'-->'(dummyop(int(1)),[int(2)]),tsrc,tdst) ).
155		:- assert_must_fail( check_transition(bop(dummyop,1,1,[],[]),dummyop(int(1)),tsrc,tdst) ).
156		:- assert_must_succeed(call_cleanup(( empty_state(E),
157		state_space_add(tsrc,E),
158		create_texpr(integer(2),integer,[],I2),
159		check_transition(bop(dummyop,1,1,[],[1/I2]),
160		'-->'(dummyop(int(1)),[int(2)]),tsrc,tdst)),
161		retract_visited_expression(tsrc,_))).
162		:- assert_must_fail(call_cleanup(( empty_state(E),
163		state_space_add(tsrc,E),
164		create_texpr(integer(2),integer,[],I2),
165		check_transition(bop(dummyop,1,1,[],[1/I2]),
166		'-->'(dummyop(int(1)),[int(1)]),tsrc,tdst)),
167		retract_visited_expression(tsrc,_))).
168
169		% bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns):
170		% The transition is a B operation with name Name, NumberArgs parameters and NumberResults
171		% result values.
172		% ArgPatterns is a list of Terms of the form Index/Expr where Index is the
173		% number of the parameter that should have the value of the expression Expr.
174		% ResPatterns is a list analogous to ArgPatterns on the result
175		check_transition(bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),
176		Transition,SrcNode,_DstNode) :-
177		!, functor(Op,Name,NumberArgs),
178		( NumberResults == 0 -> Transition = Op
179		; otherwise ->
180		Transition = '-->'(Op,ReturnValues),
181		length(ReturnValues,NumberResults),
182		check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues)),
183		check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op).
184		check_transition(btrans(TransPred),Transition,SrcNode,DstNode) :-
185		!, check_eventb_transition(TransPred,Transition,SrcNode,DstNode).
186		check_transition(csp(Channel,Arity,Args),Transition,_SrcNode,_DstNode) :-
187		!, check_csp_event(Channel,Arity,Args,Transition).
188		check_transition(xtl(Op,Arity,PatternArgs),Transition,_SrcNode,_DstNode) :-
189		!, check_xtl_transition(Op,Arity,PatternArgs,Transition).
190		check_transition(plugin_transition_check(Id,Predicate),Transition,_SrcNode,_DstNode) :-
191		!, plugin_evaluate_transition_predicate(Id,Predicate,Transition).
192		check_transition(Spec,_Trans,_SrcNode,_DstNode) :-
193		functor(Spec,Name,Arity), add_error(ltl, 'Unknown transition specification: ', Name/Arity), fail.
194
195		:- block check_xtl_transition(?,?,?,-).
196		check_xtl_transition(Op,Arity,PatternArgs,Transition) :-
197		( Arity=0 ->
198		functor(Transition,Op,_) /* in this case: pattern match any operation with right number of args */
199		; %functor(Transition,Op,Arity),
200		Transition =.. [Op|Args],
201		check_xtl_arguments(Args,PatternArgs)
202		).
203
204		check_bop_arg_patterns([],_,_,_).
205		check_bop_arg_patterns([P|Prest],Node,State,Op) :-
206		check_bop_arg_patterns2([P|Prest],Node,State,Op).
207		:- block check_bop_arg_patterns2(?,?,?,-).
208		check_bop_arg_patterns2([],_,_,_).
209		check_bop_arg_patterns2([Index/Expr|Prest],Node,State,Op) :-
210		check_bop_arg_pattern(Index,Expr,Node,State,Op),
211		check_bop_arg_patterns2(Prest,Node,State,Op).
212		check_bop_arg_pattern(Index,Expr,Node,State,Op) :-
213		arg(Index,Op,OpValue), % exception if Index is expression like 1+1 <----
214		check_b_operation_value(OpValue,Expr,Node,State).
215
216		check_bop_res_patterns([],_,_,_).
217		check_bop_res_patterns([P|Prest],Node,State,OpResult) :-
218		check_bop_res_patterns2([P|Prest],Node,State,OpResult).
219		:- block check_bop_res_patterns2(?,?,?,-).
220		check_bop_res_patterns2([],_,_,_).
221		check_bop_res_patterns2([Index/Expr|Prest],Node,State,OpResult) :-
222		check_bop_res_pattern(Index,Expr,Node,State,OpResult),
223		check_bop_res_patterns2(Prest,Node,State,OpResult).
224		check_bop_res_pattern(Index,Expr,Node,State,OpResult) :-
225		nth1(Index,OpResult,OpValue),
226		check_b_operation_value(OpValue,Expr,Node,State).
227
228		check_b_operation_value(OpValue,Expr,Node,State) :-
229	?	( var(State) ->
230	?	visited_expression(Node,RawState),
231		state_corresponds_to_initialised_b_machine(RawState,State)
232		; otherwise -> true),
233		empty_state(LS),
234		b_compute_expression(Expr,LS,State,PatternValue),
235		equal_object(PatternValue,OpValue),!.
236
237
238		:- block check_eventb_transition(?,-,?,?).
239		check_eventb_transition(event(Name),Transition,_SrcNode,_DstNode) :- !,
240		functor(Transition,Name,_).
241		check_eventb_transition(event(Name,Predicate,PoststateAccess),Transition,SrcNode,DstNode) :- !,
242		functor(Transition,Name,_),
243		visited_expression(SrcNode,CurState),
244		state_corresponds_to_initialised_b_machine(CurState,CurBState),
245		parameter_values(Transition,LocalState1),
246		add_post_state_values(PoststateAccess,DstNode,LocalState1,LocalState),
247		b_test_boolean_expression_wf(Predicate,LocalState,CurBState).
248
249		add_post_state_values([],_DstNode,State,State) :- !.
250		add_post_state_values(Access,Node,InState,OutState) :-
251		visited_expression(Node,DstState1),
252		state_corresponds_to_initialised_b_machine(DstState1,DstState),
253		add_post_state_values2(Access,DstState,InState,OutState).
254		add_post_state_values2([],_DstState,State,State).
255		add_post_state_values2([poststate(Orig,Primed)|Prest],DstState,InState,OutState) :-
256		lookup_value(Orig,DstState,Value),
257		add_var_to_localstate(Primed,Value,InState,InterState),
258		add_post_state_values2(Prest,DstState,InterState,OutState).
259
260		parameter_values(Transition,LocalState) :-
261		Transition =.. [Name|Arguments],
262		b_get_machine_operation(Name,_,Parameters,_),
263		empty_state(Empty),
264		add_parameter_values2(Parameters,Arguments,Empty,LocalState).
265		add_parameter_values2([],[],State,State).
266		add_parameter_values2([TParameter|Prest],[Argument|Arest],InState,OutState) :-
267		def_get_texpr_id(TParameter,Parameter),
268		add_var_to_localstate(Parameter,Argument,InState,InterState),
269		add_parameter_values2(Prest,Arest,InterState,OutState).
270
271		/*
272		:- assert_must_succeed(( ltl:split_operation('ch.2.3','.',ch,A), A=[2,3] )).
273		:- assert_must_succeed(( ltl:split_operation('ch.2.3','.',ch,[2,3]) )).
274		:- assert_must_succeed(( ltl:split_operation('ch','.',ch,[]) )).
275		:- assert_must_succeed(( ltl:split_operation('ch.','.',ch,[A]), A='' )).
276		split_operation(OpAtom, Sep, OpName, OpArgs) :-
277		atom_codes(OpAtom,ListAscii), atom_codes(Sep,[SepACode]),
278		split_op(ListAscii,SepACode,HeadA, ArgsA),
279		atom_codes(Head,HeadA), OpName=Head,
280		l_name(Args,ArgsA), Args=OpArgs.
281		l_name([],[]).
282		l_name([H|T],[AH|AT]) :- name(H,AH), % using name to generate numbers if possible
283		l_name(T,AT).
284
285		split_op([],_,[],[]). % no separator found
286		split_op([H|T],Sep,OpName,Args) :-
287		(H=Sep -> Args=[FirstArg|OtherArgs],OpName=[],split_args(T,Sep,FirstArg,OtherArgs)
288		; OpName = [H|CT], split_op(T,Sep,CT,Args)).
289
290		split_args([],_Sep,[],[]).
291		split_args([H|T],Sep,FirstArg,OtherArgs) :-
292		(H=Sep -> FirstArg=[], OtherArgs=[NextArg|TA],split_args(T,Sep,NextArg,TA)
293		; FirstArg = [H|CT], split_args(T,Sep,CT,OtherArgs)).
294		*/
295
296
297		check_xtl_arguments([],[]).
298		check_xtl_arguments([],[H|T]) :-
299		print('### Extra arguments in LTL/CTL pattern: '),print([H|T]),nl,fail.
300		check_xtl_arguments([H|T],[]) :- print(ltl_check_xtl_arguments_ignoring([H|T])),nl.
301		check_xtl_arguments([H|T],[PatH|PatT]) :-
302		check_xtl_arg(PatH,H,T,RemArgs),
303		check_xtl_arguments(RemArgs,PatT).
304
305		check_xtl_arg('_',_,TArgs,RemArgs) :- !,RemArgs=TArgs.
306		check_xtl_arg('?',_,TArgs,RemArgs) :- !,RemArgs=TArgs.
307		check_xtl_arg(X,Y,TArgs,RemArgs) :- atomic(Y),!,X=Y,RemArgs=TArgs.
308		check_xtl_arg(X,Y,TArgs,RemArgs) :- nonvar(Y),!,Y=..[Functor|YArgs], Functor=X,
309		append(YArgs,TArgs,RemArgs).
310		check_xtl_arg(X,Y,TArgs,RemArgs) :- var(Y),
311		print(variable_for_ltl_pattern(X)),nl,
312		X=Y,RemArgs=TArgs.