1		% (c) 2009-2019 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		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		get_por_preferences/1
11		]).
12
13		/* SICSTUS Libraries */
14		:- use_module(library(lists)).
15
16		/* ProB standard modules */
17		% B
18		:- use_module(probsrc(kernel_objects),[equal_object/2]).
19		:- use_module(probsrc(bsyntaxtree), [create_texpr/4, def_get_texpr_id/2]). % used for test cases
20		:- use_module(probsrc(bmachine),[b_get_machine_operation/4]).
21		:- use_module(probsrc(b_interpreter),[b_compute_expression_nowf/4,b_test_boolean_expression_wf/3]).
22		% state space modules
23		:- use_module(probsrc(state_space),[impl_trans_term/3,
24		visited_expression/2,
25		%transition/3,
26		state_space_add/2,retract_visited_expression/2 % used for test cases
27		]).
28		:- use_module(probsrc(store),[empty_state/1,lookup_value/3,add_var_to_localstate/4]).
29		:- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/2]).
30		% utility modules
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
38		/* ProB LTL modules */
39		:- use_module(probltlsrc(ltl_tools)).
40		:- use_module(probltlsrc(ltl_translate),[pp_ltl_formula/2]).
41
42		:- use_module(probsrc(module_information),[module_info/2]).
43		:- module_info(group,ltl).
44		:- module_info(description,'This module provides predicates for evaluating atomic and transition prepositions.').
45
46		:- use_module(probsrc(specfile),[property/2]).
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		check_ap(xtl_predicate_check(Prop),Node) :-
69		visited_expression(Node,State),!,
70		property(State,Prop).
71		check_ap(X,Node) :- visited_expression(Node,_),!,
72		add_internal_error('Unknown atomic proposition:',check_ap(X,Node)),fail.
73		check_ap(X,Node) :- add_internal_error('Unknown state:',check_ap(X,Node)),fail.
74
75		check_if_maximum_one_enabled(OpList,Node) :-
76		check_if_maximum_one_enabled(OpList,0,Node).
77
78		check_if_maximum_one_enabled([],_NrEnabled,_Node).
79		check_if_maximum_one_enabled([Op|Ops],NrEnabled,Node) :-
80		(check_enabled(Op,Node) ->
81		NrEnabled == 0, NrEnabled1 = 1
82		; NrEnabled1 = 0
83		), check_if_maximum_one_enabled(Ops,NrEnabled1,Node).
84
85		is_exactly_one_operation_enabled(OpList,Node) :-
86		is_exactly_one_operation_enabled(OpList,0,Node).
87
88		is_exactly_one_operation_enabled([],NrEnabled,_Node) :-
89		NrEnabled=1.
90		is_exactly_one_operation_enabled([Op|Ops],NrEnabled,Node) :-
91		(check_enabled(Op,Node) ->
92		NrEnabled == 0, NrEnabled1 = 1
93		; NrEnabled1 = NrEnabled
94		), is_exactly_one_operation_enabled(Ops,NrEnabled1,Node).
95
96		check_if_all_disabled([],_Node).
97		check_if_all_disabled([Op|Ops],Node) :-
98		\+check_enabled(Op,Node),
99		check_if_all_disabled(Ops,Node).
100
101		check_enabled(Spec,SrcNode) :-
102		check_transition(Spec,Transition,SrcNode,DestNode),
103		trans(SrcNode,DestNode,Transition),!.
104
105
106		trans(A,B,Op) :- impl_trans_term(A,Op,B).
107		% THE FOLLOWING CODE IS BROKEN: TO DO FIX or REMOVE and probably remove use_por_for_ltl preference
108		%:- use_module(probltlsrc(ample_sets),[compute_ample_set2/2]).
109		%trans(A,B,Op) :-
110		% ( (preference(use_por_for_ltl,true), animation_mode(b))
111		% -> get_por_preferences(POROptions), % poor implementation (ltl predicates should not be called from here)
112		% ample_sets: compute_ample_set2(A,POROptions), % TO DO : THIS HAS 3 ARGUMENTS !!!
113		% transition(A,Op,B) % from state_space.pl
114		% ; impl_trans_term(A,Op,B) /* will automatically compute as required */
115		% ).
116
117		:- use_module(probsrc(preferences),[get_preference/2]).
118		get_por_preferences(por(TYPE,UseEnableGraph,Depth,UsePGE)) :-
119		get_preference(por,TYPE),
120		get_preference(enable_graph,UseEnableGraph),
121		get_preference(enable_graph_depth,Depth),
122		get_preference(pge,UsePGE).
123
124		% a utility to check restricted atomic LTL properties on single nodes
125		check_atomic_property_formula(ap(ParsedFormula),NodeId) :- !,
126		check_ap(ParsedFormula,NodeId).
127		%check_atomic_property_formula(ap(ParsedFormula),NodeId) :- !,
128		check_atomic_property_formula(and(P1,P2),NodeId) :- !,
129		check_atomic_property_formula(P1,NodeId),
130		check_atomic_property_formula(P2,NodeId).
131		check_atomic_property_formula(or(P1,P2),NodeId) :- !,
132		(check_atomic_property_formula(P1,NodeId) ;
133		check_atomic_property_formula(P2,NodeId)).
134		check_atomic_property_formula(implies(P1,P2),NodeId) :- !,
135		(check_atomic_property_formula(P1,NodeId)
136		-> check_atomic_property_formula(P2,NodeId) ; true).
137		check_atomic_property_formula(not(P1),NodeId) :- !,
138		(check_atomic_property_formula(P1,NodeId) -> fail ; true).
139		check_atomic_property_formula(Formula,_) :- %print(Formula),nl,
140		pp_ltl_formula(Formula,Text),!,
141		add_error(check_atomic_property_formula,'LTL formula is not an atomic property: ',Text).
142		check_atomic_property_formula(Formula,N) :-
143		add_internal_error('LTL formula invalid: ',check_atomic_property_formula(Formula,N)),fail.
144
145		% check_transition(Spec,Transition,SrcNode,DstNode)
146		% Checks if a transition fulfils the specification, it fails if not.
147		% Please note, that this predicate is called _before_ the actual transition
148		% is known.
149		% Spec: specification that encodes how the transition should look like
150		% See below for the supported transitions
151		% Transition: The transition itself as it is stored in the second arg of state_space:transition/3
152		% SrcNode: The Id of the source state (first arg of transition/3)
153		% DstNode: The Id of the destination state (third arg of transition/3)
154
155		:- assert_must_succeed( check_transition(bop(dummyop,2,0,[],[]),dummyop(int(1),int(2)),tsrc,tdst) ).
156		:- assert_must_fail( check_transition(bop(dummyop,2,0,[],[]),otherop(int(1),int(2)),tsrc,tdst) ).
157		:- assert_must_fail( check_transition(bop(dummyop,2,0,[],[]),dummyop(int(1)),tsrc,tdst) ).
158		:- assert_must_succeed(call_cleanup(( empty_state(E),
159		state_space_add(tsrc,E),
160		create_texpr(integer(2),integer,[],I2),
161		check_transition(bop(dummyop,2,0,[2/I2],[]),
162		dummyop(int(1),int(2)),tsrc,tdst)),
163		retract_visited_expression(tsrc,_))).
164		:- assert_must_fail(call_cleanup(( empty_state(E),
165		state_space_add(tsrc,E),
166		create_texpr(integer(2),integer,[],I2),
167		check_transition(bop(dummyop,2,0,[1/I2],[]),
168		dummyop(int(1),int(2)),tsrc,tdst)),
169		retract_visited_expression(tsrc,_))).
170		:- assert_must_succeed( check_transition(bop(dummyop,1,1,[],[]),'-->'(dummyop(int(1)),[int(2)]),tsrc,tdst) ).
171		:- assert_must_fail( check_transition(bop(dummyop,1,1,[],[]),dummyop(int(1)),tsrc,tdst) ).
172		:- assert_must_succeed(call_cleanup(( empty_state(E),
173		state_space_add(tsrc,E),
174		create_texpr(integer(2),integer,[],I2),
175		check_transition(bop(dummyop,1,1,[],[1/I2]),
176		'-->'(dummyop(int(1)),[int(2)]),tsrc,tdst)),
177		retract_visited_expression(tsrc,_))).
178		:- assert_must_fail(call_cleanup(( empty_state(E),
179		state_space_add(tsrc,E),
180		create_texpr(integer(2),integer,[],I2),
181		check_transition(bop(dummyop,1,1,[],[1/I2]),
182		'-->'(dummyop(int(1)),[int(1)]),tsrc,tdst)),
183		retract_visited_expression(tsrc,_))).
184
185		% bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns):
186		% The transition is a B operation with name Name, NumberArgs parameters and NumberResults
187		% result values.
188		% ArgPatterns is a list of Terms of the form Index/Expr where Index is the
189		% number of the parameter that should have the value of the expression Expr.
190		% ResPatterns is a list analogous to ArgPatterns on the result
191		check_transition(bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),
192		Transition,SrcNode,_DstNode) :-
193		!, functor(Op,Name,NumberArgs),
194		( NumberResults == 0 -> Transition = Op
195		; otherwise ->
196		Transition = '-->'(Op,ReturnValues),
197		length(ReturnValues,NumberResults),
198		check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues)),
199		check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op).
200		check_transition(btrans(TransPred),Transition,SrcNode,DstNode) :-
201		!, check_eventb_transition(TransPred,Transition,SrcNode,DstNode).
202		check_transition(csp(Channel,Arity,Args),Transition,_SrcNode,_DstNode) :-
203		!, check_csp_event(Channel,Arity,Args,Transition).
204		check_transition(xtl(Op,Arity,PatternArgs),Transition,_SrcNode,_DstNode) :-
205		!, check_xtl_transition(Op,Arity,PatternArgs,Transition).
206		check_transition(Spec,_Trans,_SrcNode,_DstNode) :-
207		functor(Spec,Name,Arity), add_error(ltl, 'Unknown transition specification: ', Name/Arity), fail.
208
209		:- block check_xtl_transition(?,?,?,-).
210		check_xtl_transition(Op,Arity,PatternArgs,Transition) :-
211		( Arity=0 ->
212		functor(Transition,Op,_) /* in this case: pattern match any operation with right number of args */
213		; %functor(Transition,Op,Arity),
214		Transition =.. [Op|Args],
215		check_xtl_arguments(Args,PatternArgs)
216		).
217
218		check_bop_arg_patterns([],_,_,_).
219		check_bop_arg_patterns([P|Prest],Node,State,Op) :-
220		check_bop_arg_patterns2([P|Prest],Node,State,Op).
221		:- block check_bop_arg_patterns2(?,?,?,-).
222		check_bop_arg_patterns2([],_,_,_).
223		check_bop_arg_patterns2([Index/Expr|Prest],Node,State,Op) :-
224		check_bop_arg_pattern(Index,Expr,Node,State,Op),
225		check_bop_arg_patterns2(Prest,Node,State,Op).
226		check_bop_arg_pattern(Index,Expr,Node,State,Op) :-
227		arg(Index,Op,OpValue), % exception if Index is expression like 1+1 <----
228		check_b_operation_value(OpValue,Expr,Node,State).
229
230		check_bop_res_patterns([],_,_,_).
231		check_bop_res_patterns([P|Prest],Node,State,OpResult) :-
232		check_bop_res_patterns2([P|Prest],Node,State,OpResult).
233		:- block check_bop_res_patterns2(?,?,?,-).
234		check_bop_res_patterns2([],_,_,_).
235		check_bop_res_patterns2([Index/Expr|Prest],Node,State,OpResult) :-
236		check_bop_res_pattern(Index,Expr,Node,State,OpResult),
237		check_bop_res_patterns2(Prest,Node,State,OpResult).
238		check_bop_res_pattern(Index,Expr,Node,State,OpResult) :-
239		nth1(Index,OpResult,OpValue),
240		check_b_operation_value(OpValue,Expr,Node,State).
241
242		check_b_operation_value(OpValue,Expr,Node,State) :-
243		( var(State) ->
244		visited_expression(Node,RawState),
245		state_corresponds_to_initialised_b_machine(RawState,State)
246		; otherwise -> true),
247		empty_state(LS),
248		b_compute_expression_nowf(Expr,LS,State,PatternValue),
249		equal_object(PatternValue,OpValue),!.
250
251
252		:- block check_eventb_transition(?,-,?,?).
253		check_eventb_transition(event(Name),Transition,_SrcNode,_DstNode) :- !,
254		functor(Transition,Name,_).
255		check_eventb_transition(event(Name,Predicate,PoststateAccess),Transition,SrcNode,DstNode) :- !,
256		functor(Transition,Name,_),
257		visited_expression(SrcNode,CurState),
258		state_corresponds_to_initialised_b_machine(CurState,CurBState),
259		parameter_values(Transition,LocalState1),
260		add_post_state_values(PoststateAccess,DstNode,LocalState1,LocalState),
261		b_test_boolean_expression_wf(Predicate,LocalState,CurBState).
262
263		add_post_state_values([],_DstNode,State,State) :- !.
264		add_post_state_values(Access,Node,InState,OutState) :-
265		visited_expression(Node,DstState1),
266		state_corresponds_to_initialised_b_machine(DstState1,DstState),
267		add_post_state_values2(Access,DstState,InState,OutState).
268		add_post_state_values2([],_DstState,State,State).
269		add_post_state_values2([poststate(Orig,Primed)|Prest],DstState,InState,OutState) :-
270		lookup_value(Orig,DstState,Value),
271		add_var_to_localstate(Primed,Value,InState,InterState),
272		add_post_state_values2(Prest,DstState,InterState,OutState).
273
274		parameter_values(Transition,LocalState) :-
275		Transition =.. [Name|Arguments],
276		b_get_machine_operation(Name,_,Parameters,_),
277		empty_state(Empty),
278		add_parameter_values2(Parameters,Arguments,Empty,LocalState).
279		add_parameter_values2([],[],State,State).
280		add_parameter_values2([TParameter|Prest],[Argument|Arest],InState,OutState) :-
281		def_get_texpr_id(TParameter,Parameter),
282		add_var_to_localstate(Parameter,Argument,InState,InterState),
283		add_parameter_values2(Prest,Arest,InterState,OutState).
284
285
286		check_xtl_arguments([],[]).
287		check_xtl_arguments([],[H|T]) :-
288		print('### Extra arguments in LTL/CTL pattern: '),print([H|T]),nl,fail.
289		check_xtl_arguments([_H|_T],[]).
290		% format('Ignoring extra argument(s) ~w in action, add .? to LTL/CTL pattern to get rid of this message.~n',[[H|T]]).
291		check_xtl_arguments([H|T],[PatH|PatT]) :-
292		check_xtl_arg(PatH,H,T,RemArgs),
293		check_xtl_arguments(RemArgs,PatT).
294
295		check_xtl_arg('_',_,TArgs,RemArgs) :- !,RemArgs=TArgs.
296		check_xtl_arg('?',_,TArgs,RemArgs) :- !,RemArgs=TArgs.
297		check_xtl_arg(X,Y,TArgs,RemArgs) :- atomic(Y),!,X=Y,RemArgs=TArgs.
298		check_xtl_arg(X,Y,TArgs,RemArgs) :- nonvar(Y),!,Y=..[Functor|YArgs], Functor=X,
299		append(YArgs,TArgs,RemArgs).
300		check_xtl_arg(X,Y,TArgs,RemArgs) :- var(Y),
301		print(variable_for_ltl_pattern(X)),nl,
302		X=Y,RemArgs=TArgs.