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. |