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