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