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 | | |
6 | | :- module(cbc_path_solver,[ |
7 | | create_testcase_path/5, |
8 | | create_testcase_path_nondet/4, |
9 | | |
10 | | testcase_path_timeout/9, |
11 | | testcase_path_timeout_catch/9, |
12 | | testcase_predicate_timeout/3, |
13 | | |
14 | | testcase_initialise/5, % not a very nice API call; used in sap, refactor |
15 | | testcase_set_up_events/9, % ditto |
16 | | add_constants_to_state_space/5, add_operations_to_state_space/5, % ditto |
17 | | remove_constants_from_state/4, |
18 | | verify_alloy_command/5 |
19 | | ]). |
20 | | |
21 | | :- use_module(probsrc(module_information),[module_info/2]). |
22 | | :- module_info(group,cbc). |
23 | | :- module_info(description,'Create paths for Event-B or Classical B via constraint solving'). |
24 | | |
25 | | |
26 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
27 | | % test case generation for a given list of event by |
28 | | % constraint solving |
29 | | |
30 | | :- use_module(probsrc(b_interpreter)). |
31 | | %:- use_module(b_interpreter_eventb). |
32 | | :- use_module(probsrc(kernel_waitflags)). |
33 | | :- use_module(probsrc(store)). |
34 | | :- use_module(probsrc(debug)). |
35 | | :- use_module(probsrc(bmachine)). |
36 | | :- use_module(probsrc(state_space)). |
37 | | :- use_module(probsrc(solver_interface)). |
38 | | :- use_module(probsrc(debug),[debug_format/3]). |
39 | | :- use_module(probsrc('cdclt_solver/cdclt_solver')). |
40 | | :- use_module(probsrc(bsyntaxtree),[conjunct_predicates/2]). |
41 | | :- use_module(probsrc('smt_solvers_interface/smt_solvers_interface')). |
42 | | :- use_module(probsrc(tools), [start_ms_timer/1,stop_ms_walltimer_with_msg/2]). |
43 | | :- use_module(probsrc(error_manager),[add_internal_error/2, enter_new_error_scope/2, exit_error_scope/3, |
44 | | add_error/3, add_message/3, |
45 | | critical_enumeration_warning_occured_in_error_scope/0]). |
46 | | :- use_module(probsrc(tools), [ajoin/2]). |
47 | | |
48 | | %create_testcase_path(Events,Timeout,Result) :- |
49 | | % create_testcase_path(init,Events,b(truth,pred,[]),Timeout,Result). |
50 | | %create_testcase_path(INIT,Events,Timeout,Result) :- % version with arity 4; not used |
51 | | % create_testcase_path(INIT,Events,b(truth,pred,[]),Timeout,Result). |
52 | | |
53 | | |
54 | | % use the constraint solver to create a path from an initial state (and valuation of the constants) |
55 | | % with the given list of events/operations and the provided target predicate |
56 | | % INIT is either |
57 | | % init: start from an initial state |
58 | | % invariant start from a state satisfying the invariant |
59 | | % typing start from a state without any constraint, apart from typing |
60 | | % typing(Pred) start from a state where Pred holds (and typing) |
61 | | % pred(P) start from invariant and predicate P |
62 | | |
63 | | create_testcase_path(INIT,Events,EndPredicate,Timeout,Result) :- |
64 | | % allow user interrupts during the search, just fail if that happens |
65 | | testcase_path_timeout(INIT,Timeout,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R), |
66 | | ( R==ok -> |
67 | | add_constants_to_state_space(ConstantsState,TestStates,ConstTestStates,SetupSequence,StartStateId), |
68 | | add_operations_to_state_space(Operations,StartStateId,ConstTestStates,TransInfos,OpSequence), |
69 | | append(SetupSequence,OpSequence,Result) |
70 | | ; Result = R). |
71 | | |
72 | | % same as create_testcase_path: does not react to interrupts, no time-out, but can be backtracked ! |
73 | | create_testcase_path_nondet(INIT,Events,EndPredicate,Result) :- |
74 | | % allow user interrupts during the search, just fail if that happens |
75 | | testcase_path(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos), |
76 | | add_constants_to_state_space(ConstantsState,TestStates,ConstTestStates,SetupSequence,StartStateId), |
77 | | add_operations_to_state_space(Operations,StartStateId,ConstTestStates,TransInfos,OpSequence), |
78 | | append(SetupSequence,OpSequence,Result). |
79 | | |
80 | | % ------------------------------- |
81 | | :- use_module(probsrc(clpfd_interface),[catch_clpfd_overflow_call3/3]). |
82 | | % copy of predicate in static_analysis to avoid meta_predicate error in Spider: |
83 | | :- meta_predicate catch_enumeration_warning_and_overflow(0,0). |
84 | | catch_enumeration_warning_and_overflow(Call,Handler) :- |
85 | | % throw/1 predicate raises instantiation_error |
86 | | catch_clpfd_overflow_call3( |
87 | | catch(Call, enumeration_warning(enumerating(_),_Type,_,_,critical), call(Handler)), |
88 | | message, % could also be silent |
89 | | call(Handler)). |
90 | | |
91 | | testcase_path_timeout_catch(Pred,TIMEOUT,Seq,P2,Csts,Ops,TestS,TI,Res) :- |
92 | | enter_new_error_scope(ScopeID,testcase_path_timeout_catch), |
93 | | (catch_enumeration_warning_and_overflow( |
94 | | cbc_path_solver:testcase_path_timeout(Pred,TIMEOUT,Seq,P2,Csts,Ops,TestS,TI,Res), |
95 | | Res=virtual_time_out) |
96 | | -> exit_error_scope(ScopeID,_ErrOcc,testcase_path_timeout_catch) |
97 | | ; (critical_enumeration_warning_occured_in_error_scope -> |
98 | | debug_format(19,'Enumeration warning occurred and is treated as timeout due to failure to find solution.~n',[]), |
99 | | exit_error_scope(ScopeID,_ErrOcc,testcase_path_timeout_catch), |
100 | | Res=virtual_time_out |
101 | | ; exit_error_scope(ScopeID,_ErrOcc,testcase_path_timeout_catch), |
102 | | fail |
103 | | ) |
104 | | ). |
105 | | |
106 | | |
107 | | :- use_module(probsrc(tools_meta),[safe_time_out/3]). |
108 | | :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]). |
109 | | |
110 | | testcase_path_timeout(INIT,0,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R) :- |
111 | | !,testcase_path_interrupt(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R). |
112 | | testcase_path_timeout(INIT,TimeoutMs,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result) :- |
113 | | safe_time_out(testcase_path_interrupt(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,R), |
114 | | TimeoutMs, |
115 | | T), |
116 | | (T==success -> Result=R ; Result=timeout). |
117 | | |
118 | | :- use_module(probsrc(clpfd_interface),[catch_clpfd_overflow_call3/3]). |
119 | | testcase_path_interrupt(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result) :- |
120 | | catch_clpfd_overflow_call3( |
121 | | testcase_path_interrupt2(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result), |
122 | | message, % no need to create warning or error; we return clpfd_overflow as result |
123 | | Result=clpfd_overflow). |
124 | | |
125 | | testcase_path_interrupt2(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos,Result) :- |
126 | | user_interruptable_call_det(testcase_path(INIT,Events,EndPredicate,ConstantsState,Operations,TestStates,TransInfos), |
127 | | Interrupt), |
128 | | (Interrupt==ok -> Result=ok ; Result=interrupt). |
129 | | |
130 | | add_constants_to_state_space(ConstantsState,TestStates,TestStates,[],root) :- |
131 | | empty_state(ConstantsState),!. |
132 | | add_constants_to_state_space(ConstantsState,TestStates,ConstTestStates,[Tuple],ConstantsID) :- |
133 | | Tuple = (SetupID,Setup,root,ConstantsID), |
134 | | specfile:create_setup_constants_operation(ConstantsState,complete_properties,Setup), |
135 | | tcltk_interface:tcltk_add_new_transition_transid(root,Setup,ConstantsID,concrete_constants(ConstantsState),[],SetupID), |
136 | | remove_constants_from_state(TestStates,ConstantsState,ConstantsID,ConstTestStates). |
137 | | |
138 | | remove_constants_from_state([],_,_,[]). |
139 | | remove_constants_from_state([InState|Irest],Constants,ConstId,[const_and_vars(ConstId,OutState)|Orest]) :- |
140 | | append(OutState,Constants,InState),!, % assume constants are at hend |
141 | | remove_constants_from_state(Irest,Constants,ConstId,Orest). |
142 | | |
143 | | |
144 | | add_operations_to_state_space([],_,[],[],[]). |
145 | | add_operations_to_state_space([Operation|Orest],PrevId,[State|Srest],[TransInfo|Trest],[Tuple|Irest]) :- |
146 | | Tuple = (OpId,Operation,PrevId,NextId), |
147 | | tcltk_interface:tcltk_add_new_transition_transid(PrevId,Operation,NextId,State,TransInfo,OpId), |
148 | | add_operations_to_state_space(Orest,NextId,Srest,Trest,Irest). |
149 | | |
150 | | :- use_module(probsrc(store),[normalise_state/2, normalise_states/2]). |
151 | | :- use_module(probsrc(kernel_waitflags),[push_wait_flag_call_stack_info/3, opt_push_wait_flag_call_stack_info/3]). |
152 | | |
153 | | testcase_path(INITIALISE,Events,EndPredicate,NormalisedConstantsState,OPS,StateSequence,TINFOS) :- |
154 | | init_wait_flags(WF0,[testcase_path]), |
155 | | opt_push_wait_flag_call_stack_info(WF0,using_state(cbc_path_solver,InitialState),WF), |
156 | | (INITIALISE=init |
157 | | -> OPS = [OpInit|Operations], TINFOS = [ITransInfo|OpTransInfos], |
158 | | testcase_initialise(ConstantsState,InitialState,OpInit,ITransInfo,WF) |
159 | | % TODO: push Init on WF call stack |
160 | | ; OPS = Operations, TINFOS = OpTransInfos, |
161 | | (just_typing_opt(INITIALISE) |
162 | | -> set_up_a_typed_state(ConstantsState,InitialState,WF) % only set up types |
163 | | ; set_up_a_valid_state(ConstantsState,InitialState,WF) % set up invariant |
164 | | ), |
165 | | % TO DO: project away constants and variables not needed for OPS and Predicates |
166 | | (init_opt_has_predicate(INITIALISE,InitialPredicate) |
167 | | -> eval_predicate(InitialPredicate,InitialState,WF) |
168 | | ; true) |
169 | | ), |
170 | | testcase_set_up_events(Events,InitialState,ConstantsState,Operations,States,FinalState,OpTransInfos,WF,WF2), |
171 | | eval_predicate(EndPredicate,FinalState,WF2), |
172 | ? | ground_wait_flags(WF2), |
173 | | normalise_states([InitialState|States],StateSequence), |
174 | | normalise_state(ConstantsState,NormalisedConstantsState). |
175 | | |
176 | ? | just_typing_opt(Option) :- get_init_option_paras(Option,Typing,_), !, Typing=typing. |
177 | ? | init_opt_has_predicate(Option,Pred) :- get_init_option_paras(Option,_,Pred),!, Pred \= none. |
178 | | |
179 | | get_init_option_paras(init,init,none). |
180 | | get_init_option_paras(typing,typing,none). |
181 | | get_init_option_paras(typing(Pred),typing,Pred). % just use typing from invariant and add P |
182 | | get_init_option_paras(invariant,invariant,none). |
183 | | get_init_option_paras(pred(Pred),invariant,Pred). % add P to invariant |
184 | | get_init_option_paras(INITIALISE,_,_) :- |
185 | | add_internal_error('Illegal init option:',get_init_option_paras(INITIALISE)),fail. |
186 | | |
187 | | |
188 | | testcase_predicate_timeout(Pred,Timeout,Result) :- |
189 | | catch(( |
190 | | safe_time_out(testcase_predicate(Pred), Timeout, T), |
191 | | (T==success -> Result=ok ; Result=timeout) |
192 | | ), enumeration_warning(_,_,_,_,_), Result=timeout). |
193 | | |
194 | | testcase_predicate(Predicate) :- |
195 | | init_wait_flags(WF,[testcase_predicate]), |
196 | | (just_typing_opt(Predicate) -> |
197 | | set_up_a_typed_state(_ConstantsState,InitialState,WF) % only set up types |
198 | | ; |
199 | | set_up_a_valid_state(_ConstantsState,InitialState,WF)), |
200 | | (init_opt_has_predicate(Predicate,Pred) -> |
201 | | eval_predicate(Pred,InitialState,WF) |
202 | | ; true), |
203 | | ground_wait_flags(WF). |
204 | | |
205 | | eval_predicate(Predicate,State,WF) :- |
206 | | empty_state(EmptyState), |
207 | | b_test_boolean_expression(Predicate,EmptyState,State,WF). |
208 | | |
209 | | :- use_module(probsrc(b_state_model_check),[set_up_transition/7, set_up_initialisation/5]). |
210 | | |
211 | | |
212 | | testcase_set_up_events([],State,_ConstState,[],[],State,[],WF,WF). |
213 | | testcase_set_up_events([Event|Erest],InState,ConstantState,[Operation|Orest], |
214 | | [InterState|Srest],OutState,[TransInfo|Trest],WF,WF3) :- |
215 | | set_up_transition(Event,Operation,ConstantState,InState,InterState,TransInfo,WF), |
216 | | push_wait_flag_call_stack_info(WF,after_event(Operation),WF2), |
217 | | testcase_set_up_events(Erest,InterState,ConstantState,Orest,Srest,OutState,Trest,WF2,WF3). |
218 | | |
219 | | |
220 | | |
221 | | testcase_initialise(ConstantState,InitialState,Initialisation,TransInfo,WF) :- |
222 | | set_up_constants_state(ConstantState,WF), |
223 | | set_up_initialisation(ConstantState,InitialState,Initialisation,TransInfo,WF). % TO DO: here I would like to be able to set up the invariant instead, if requested by another parameter |
224 | | |
225 | | :- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1, b_get_properties_from_machine/1, |
226 | | b_get_machine_constants/1, b_get_machine_variables/1]). |
227 | | :- use_module(probsrc(b_global_sets),[static_symmetry_reduction_for_global_sets/1]). |
228 | | :- use_module(probsrc(b_enumerate), [b_tighter_enumerate_all_values/2]). |
229 | | :- use_module(probsrc(b_interpreter), [b_test_boolean_expression/4]). |
230 | | |
231 | | set_up_constants_state(ConstantsState,_WF) :- |
232 | | \+ not_all_transitions_added(root), |
233 | | \+ state_space:max_reached_or_timeout_for_node(root), |
234 | | % We should also check enumeration warnings : [DONE with max_reached_or_timeout_for_node] |
235 | | (state_space:transition(root,_,N) -> true), |
236 | | \+ ( state_space:transition(root,_,N2), N2\=N ), |
237 | | state_space:visited_expression(N,concrete_constants(ConstantsState)), |
238 | | !, % there is only one possible valuation of the constants |
239 | | debug_format(19,'Reusing constant values from state id ~w (only solution for PROPERTIES/axioms)~n',[N]). |
240 | | set_up_constants_state(ConstantState,WF) :- |
241 | | b_get_properties_from_machine(Properties), |
242 | | b_get_machine_constants(Constants), |
243 | | empty_state(EmptyState), |
244 | | set_up_typed_localstate(Constants,_FreshVars,TypedVals,EmptyState,ConstantState,positive), |
245 | | static_symmetry_reduction_for_global_sets(ConstantState), % from b_global_sets |
246 | | b_tighter_enumerate_all_values(TypedVals,WF), |
247 | | b_test_boolean_expression(Properties,EmptyState,ConstantState,WF). |
248 | | |
249 | | % set up a valid state satisfying the invariant |
250 | | set_up_a_valid_state(ConstantState,ValidState,WF) :- |
251 | | set_up_constants_state(ConstantState,WF), |
252 | | b_get_machine_variables(Variables), |
253 | | % create_target_state(Variables,Values,ConstantsState,ValidState,WF), |
254 | | set_up_typed_localstate(Variables,_Values,TypedVals,ConstantState,ValidState,positive), |
255 | | b_tighter_enumerate_all_values(TypedVals,WF), |
256 | | b_get_invariant_from_machine(Invariant), |
257 | | empty_state(EmptyState), |
258 | | b_test_boolean_expression(Invariant,EmptyState,ValidState,WF). |
259 | | |
260 | | |
261 | | |
262 | | set_up_constants_typed_state(ConstantState,WF) :- |
263 | | b_get_machine_constants(Constants), |
264 | | empty_state(EmptyState), |
265 | | set_up_typed_localstate(Constants,_FreshVars,TypedVals,EmptyState,ConstantState,positive), |
266 | | b_tighter_enumerate_all_values(TypedVals,WF). |
267 | | |
268 | | % set up a valid state satisfying the typing conditions of the invariant; but not necessarily the invariant |
269 | | set_up_a_typed_state(ConstantState,ValidState,WF) :- |
270 | | set_up_constants_typed_state(ConstantState,WF), |
271 | | b_get_machine_variables(Variables), |
272 | | % create_target_state(Variables,Values,ConstantsState,ValidState,WF), |
273 | | set_up_typed_localstate(Variables,_Values,TypedVals,ConstantState,ValidState,positive), |
274 | | b_tighter_enumerate_all_values(TypedVals,WF). |
275 | | |
276 | | |
277 | | %% verify_alloy_command(+CmdName, +Solver, -CmdIsValid, -IsCheckCmd, -Res). |
278 | | % Verify a command by solving the translated operation's precondition conjoined with the machine properties. |
279 | | % This is a special case of cbc path checking of length 1 but using a monolithic predicate. |
280 | | % Assumes that a corresponding Alloy model is loaded. |
281 | | % Solver is one of prob, probkodkod, probsmt or z3. |
282 | | verify_alloy_command(ProvidedCmdName, Solver, CmdIsValid, IsCheckCmd, Res) :- |
283 | | (ProvidedCmdName = '_' , b_get_machine_operation(CmdName, _, _, _) -> true % _ as a wildcard for first command |
284 | | ; CmdName = ProvidedCmdName), |
285 | | if(b_get_machine_operation(CmdName, _, _, Body), |
286 | | true, |
287 | | (add_error(cbc_path_solver,'Unknown Alloy command name:',CmdName), |
288 | | findall(Other,b_get_machine_operation(Other, _, _, _),OL), |
289 | | add_message(cbc_path_solver,'Available B operations: ',OL),fail)), |
290 | | get_precondition_from_translated_alloy_operation(Body, Precondition), |
291 | | b_get_properties_from_machine(Properties), |
292 | | conjunct_predicates([Properties,Precondition], Conj), |
293 | | start_ms_timer(Timer), |
294 | | ( Solver == prob |
295 | | -> solve_predicate(Conj, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true], Res) |
296 | | ; Solver == probkodkod |
297 | | -> solve_predicate(Conj, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true,use_solver_on_load/kodkod], Res) |
298 | | ; Solver == probsmt |
299 | | -> cdclt_solve_predicate(Conj, _SolvedWDPred, Res) |
300 | | ; Solver == z3, |
301 | | smt_solve_predicate(z3, Conj, _, Res) |
302 | | ), |
303 | | ( atom_concat(check, _, CmdName) |
304 | | -> validate_solver_result_for_command(check, Res, CmdIsValid), |
305 | | IsCheckCmd = true |
306 | | ; validate_solver_result_for_command(run, Res, CmdIsValid), |
307 | | IsCheckCmd = false |
308 | | ), |
309 | | (silent_mode(on) -> true |
310 | | ; (Res=solution(_) -> RS=solution ; RS=Res), |
311 | | ajoin(['Checking Alloy command ',CmdName,' with ',Solver,'; result = ',RS],Msg), |
312 | | stop_ms_walltimer_with_msg(Timer,Msg)). |
313 | | % comment in to perform double-checking of result: |
314 | | %(Solver=prob -> true ; eval_strings:double_check_smt_result(nostate(Solver),[],Conj,[],Res)). |
315 | | verify_alloy_command(ProvidedCmdName, Solver, CmdIsValid, IsCheckCmd, Res) :- |
316 | | add_internal_error('Call failed:',verify_alloy_command(ProvidedCmdName, Solver, CmdIsValid, IsCheckCmd, Res)). |
317 | | |
318 | | %% validate_solver_result_for_command(+RunOrCheck, +Res). |
319 | | % Note that check commands are negated to search for a counterexample. |
320 | | validate_solver_result_for_command(RunOrCheck, Res, CmdIsValid) :- |
321 | | Res == contradiction_found, |
322 | | !, |
323 | | ( RunOrCheck == check |
324 | | -> CmdIsValid = true |
325 | | ; CmdIsValid = false |
326 | | ). |
327 | | validate_solver_result_for_command(RunOrCheck, Res, CmdIsValid) :- |
328 | | Res = solution(_), |
329 | | ground(Res), |
330 | | !, |
331 | | ( RunOrCheck == run |
332 | | -> CmdIsValid = true |
333 | | ; CmdIsValid = false |
334 | | ). |
335 | | validate_solver_result_for_command(_, _, unknown). |
336 | | |
337 | | % We generate precondition/2 in alloy2b. No other guards. |
338 | | get_precondition_from_translated_alloy_operation(b(precondition(TPrecondition,_),subst,_), Precondition) :- |
339 | | !, |
340 | | Precondition = TPrecondition. |
341 | | get_precondition_from_translated_alloy_operation(_, b(truth,pred,[])). |