| 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,[])). |