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