| 1 | | % (c) 2009-2025 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(b_state_model_check, |
| 7 | | [b_set_up_valid_state/1, |
| 8 | | b_set_up_valid_state_with_pred/2, b_set_up_valid_state_with_pred/4, |
| 9 | | b_find_dynamic_assertion_violation/1, |
| 10 | | cbc_dynamic_assertions_check/1, % a version of the above with time-out and result |
| 11 | | b_check_valid_state/1, |
| 12 | | |
| 13 | | state_model_check_invariant/4, |
| 14 | | state_model_check_assertions/4, |
| 15 | | state_model_check/5, |
| 16 | | |
| 17 | | cbc_deadlock_freedom_check/3, get_all_guards_false_pred/1, |
| 18 | | get_unsorted_all_guards_false_pred/1, get_negated_guard/3, get_negated_guard/4, |
| 19 | | get_guard/2, get_guard_and_precision/3, |
| 20 | | |
| 21 | | cbc_static_assertions_check/1, cbc_static_assertions_check/2, |
| 22 | | |
| 23 | | tcltk_perform_cbc_check/4, |
| 24 | | cbc_find_redundant_invariants/2, |
| 25 | | |
| 26 | | set_up_transition/7, |
| 27 | | set_up_initialisation/5, |
| 28 | | |
| 29 | | execute_operation_by_predicate_in_state/5, |
| 30 | | execute_operation_by_predicate_in_state_with_pos/6, |
| 31 | | |
| 32 | | cbc_constants_det_check/1, tcltk_cbc_constants_det_check/1 |
| 33 | | ]). |
| 34 | | |
| 35 | | |
| 36 | | |
| 37 | | :- use_module(tools). |
| 38 | | |
| 39 | | :- use_module(module_information,[module_info/2]). |
| 40 | | :- module_info(group,cbc). |
| 41 | | :- module_info(description,'This module provides various tools for constraint-based checking of B machines.'). |
| 42 | | |
| 43 | | :- use_module(self_check). |
| 44 | | :- use_module(library(lists)). |
| 45 | | :- use_module(library(ordsets)). |
| 46 | | :- use_module(store). |
| 47 | | :- use_module(translate). |
| 48 | | :- use_module(b_enumerate,[ b_tighter_enumerate_all_values/2]). |
| 49 | | :- use_module(b_interpreter, |
| 50 | | [b_test_boolean_expression/4, b_test_boolean_expression/6, |
| 51 | | %b_det_test_boolean_expression/6, |
| 52 | | %b_not_test_boolean_expression/6, |
| 53 | | b_execute_top_level_operation_wf/8, |
| 54 | | b_execute_top_level_statement/7, |
| 55 | | set_up_typed_localstate/6]). |
| 56 | | :- use_module(b_interpreter_eventb, [b_event_constraints/7]). |
| 57 | | :- use_module(b_global_sets). |
| 58 | | :- use_module(bmachine). |
| 59 | | :- use_module(bsyntaxtree). |
| 60 | | |
| 61 | | :- use_module(kernel_objects). |
| 62 | | :- use_module(bsets_clp). |
| 63 | | |
| 64 | | :- use_module(solver_interface, [set_up_typed_localstate_for_pred/4]). |
| 65 | | :- use_module(preferences, [get_preference/2]). |
| 66 | | |
| 67 | | :- use_module(debug). |
| 68 | | :- use_module(typechecker). |
| 69 | | :- use_module(bmachine). |
| 70 | | :- use_module(kernel_waitflags). |
| 71 | | :- use_module(error_manager). |
| 72 | | :- use_module(probsrc(solver_interface),[apply_kodkod_or_other_optimisations/3]). |
| 73 | | |
| 74 | | /* --------------------------------------------------------- */ |
| 75 | | |
| 76 | | :- use_module(tools_printing,[format_with_colour_nl/4]). |
| 77 | | :- use_module(tools,[start_ms_timer/1, stop_ms_timer/1]). |
| 78 | | stop_silent_ms_timer(T) :- (silent_mode(on) -> true ; stop_ms_timer(T)). |
| 79 | | |
| 80 | | % constraint-based checking of invariant; checking if invariant is inductive for a given operation |
| 81 | | state_model_check_invariant(OpName,State,Operation,NormalisedNewState) :- |
| 82 | | state_model_check(OpName,invariant,State,Operation,NormalisedNewState). |
| 83 | | |
| 84 | | state_model_check_assertions(OpName,State,Operation,NormalisedNewState) :- |
| 85 | | state_model_check(OpName,assertions,State,Operation,NormalisedNewState). |
| 86 | | |
| 87 | | state_model_check(OpName,InvOrAssertion,State,Operation,NormalisedNewState) :- |
| 88 | | debug_println(9,'===> Starting Constraint-Based Checking'), |
| 89 | | start_ms_timer(Timer), |
| 90 | ? | if(cbc_model_check(OpName,InvOrAssertion,State,Operation,NewState), |
| 91 | | stop_silent_ms_timer(Timer), |
| 92 | | (stop_silent_ms_timer(Timer), |
| 93 | | format_with_colour_nl(user_output,[green],'No cbc counter example for ~w',[OpName]), |
| 94 | | fail)), |
| 95 | | nl, |
| 96 | | format_with_colour_nl(user_error,[red,bold],'Found cbc counter example for ~w',[OpName]), |
| 97 | | printsilent('% ===> Operation: '), translate_event(Operation,OpStr),println_silent(OpStr), |
| 98 | | printsilent('% ===> State: '),translate_bstate(State,StateStr),println_silent(StateStr), |
| 99 | | normalise_store(NewState,NormalisedNewState), |
| 100 | | printsilent('% ===> NewState: '),translate_bstate(NormalisedNewState,NStateStr),println_silent(NStateStr). |
| 101 | | |
| 102 | | :- use_module(library(avl)). |
| 103 | | cbc_model_check(OpName,InvOrAssertion,BeforeState,Operation,NewState) :- |
| 104 | | (nonvar(OpName), |
| 105 | | \+ b_is_operation_name(OpName), \+ b_is_initialisation_name(OpName) |
| 106 | | -> add_error(constraint_based_check,'Operation does not exist: ',OpName), fail |
| 107 | | ; true |
| 108 | | ), |
| 109 | | debug_println(9,operation_name(OpName)), |
| 110 | | b_get_properties_from_machine(Properties), |
| 111 | | b_get_invariant_from_machine(Invariant), |
| 112 | | b_get_machine_variables(Variables), |
| 113 | | b_get_machine_constants(Constants), |
| 114 | | % print_message(extracted_invariant(Variables,Invariant)), |
| 115 | | |
| 116 | | empty_state(EmptyState), |
| 117 | | set_up_typed_localstate(Constants,_FreshVars1,TypedVals1,EmptyState,State1,positive), |
| 118 | | b_global_sets:static_symmetry_reduction_for_global_sets(State1), |
| 119 | | (b_is_initialisation_name(OpName) |
| 120 | | -> State=State1, |
| 121 | | BeforeState = concrete_constants(State), % Ideally we could use root if State==[]; but ProB2 after prob2_invariant_check then tries to evaluate the invariants on it; TO DO: fix ProB2/ProB2UI first |
| 122 | | TypedVals=TypedVals1 |
| 123 | | ; BeforeState=State, |
| 124 | | set_up_typed_localstate(Variables,_FreshVars2,TypedVals2,State1,State,positive), |
| 125 | | append(TypedVals1,TypedVals2,TypedVals) |
| 126 | | ), |
| 127 | | init_wait_flags_with_call_stack(WF,[prob_command_context(cbc_model_check(OpName),unknown)]), |
| 128 | | |
| 129 | | % print_message(' set up start state:'), print_message(State), |
| 130 | | % translate:print_bexpr(Properties), |
| 131 | | empty_avl(Ai), |
| 132 | ? | b_test_boolean_expression(Properties,[],State,WF,Ai,A2), % A2 is used below for after state |
| 133 | | % print_message(' set up properties for constants'), |
| 134 | | |
| 135 | | get_target_pred(InvOrAssertion,OpName, Invariant, PriorPred,TargetPred), |
| 136 | | |
| 137 | | %print('Prior: '),translate:print_bexpr(PriorPred),nl, |
| 138 | | b_test_boolean_expression(PriorPred,[],State,WF,A2,_A3), |
| 139 | | % print_message(' set up invariant for start state'), |
| 140 | | |
| 141 | | set_up_transition_or_init(OpName,Operation,State1,State,NewState,_TransInfo,WF), |
| 142 | | debug_print(9,' finished setting up target state for operation:'), debug_println(9,OpName), |
| 143 | | %print_message(' target state:'), print_message(NewState), |
| 144 | | % Note: we are not setting up an enumerator for NewState; here we would need to be careful as we cannot use tight enumeration for NewState |
| 145 | | |
| 146 | | predicate_level_optimizations(TargetPred,OptTargetPred), |
| 147 | | |
| 148 | | (debug_mode(on) -> translate:print_bexpr(OptTargetPred),nl ; true), |
| 149 | | b_test_boolean_expression(OptTargetPred,[],NewState,WF,A2,_Ao), % not A3 but A2; as different State |
| 150 | | debug_println(9,' finished setting up invariant of proven invariants and negation of invariant for target state'), |
| 151 | | |
| 152 | | % print(enum(TypedVals)),nl, |
| 153 | | b_tighter_enumerate_all_values(TypedVals,WF), |
| 154 | | |
| 155 | | %(debug_mode(on) -> ground_wait_flag0(WF),portray_waitflags(WF),print_bt_message(grounding_wait_flags) ; true), |
| 156 | ? | ground_wait_flags(WF). |
| 157 | | |
| 158 | | % find target predicate for invariant or assertion checking |
| 159 | | get_target_pred(invariant,OpName, Invariant, PriorPred, TargetPred) :- |
| 160 | | (b_is_initialisation_name(OpName) -> create_texpr(truth,pred,[],PriorPred) ; PriorPred=Invariant), |
| 161 | | % Retrieve Information on proof status of the invariant |
| 162 | | (get_preference(use_po,true),get_proven_invariant(OpName,ProvenInvariant) -> true |
| 163 | | ; create_texpr(truth,pred,[],ProvenInvariant), println_silent(no_proven_invariant_info) |
| 164 | | ), |
| 165 | | (get_preference(use_po,false) -> UncheckedInvariant=Invariant |
| 166 | | ; b_specialized_invariant_for_op(OpName,UncheckedInvariant) -> true |
| 167 | | ; UncheckedInvariant=Invariant, println_silent(no_specialized_invariant_info_for_op(OpName)) |
| 168 | | ), |
| 169 | | %print_message('proven invariant:'),print(proven(ProvenInvariant)), |
| 170 | | create_negation(UncheckedInvariant,NegUncheckedInvariant), |
| 171 | | % we conjoin the predicates so that predicate-level optimizations can be applied (TO DO: also allow Properties to be used) |
| 172 | | conjunct_predicates([ProvenInvariant,NegUncheckedInvariant],TargetPred). |
| 173 | | get_target_pred(assertions,OpName, Invariant, PriorPred, TargetPred) :- |
| 174 | | % TODO: deal with initialisation for PriorPred |
| 175 | | get_unproven_assertion(UPA), |
| 176 | | create_negation(UPA,NegUPA), |
| 177 | | format('Trying to find Assertion Violation after ~w~n Target:',[OpName]),translate:print_bexpr(NegUPA),nl,nl, |
| 178 | | conjunct_predicates([Invariant,UPA],PriorPred), |
| 179 | | conjunct_predicates([Invariant,NegUPA],TargetPred). |
| 180 | | % Note: in Rodin we should in principle only use assertions appearing before each theorem |
| 181 | | % Also: it would make sense to assert Assertion before the test |
| 182 | | |
| 183 | | get_unproven_assertion(UPA) :- |
| 184 | | b_get_assertions(main,dynamic,Assertions), |
| 185 | | (get_preference(use_po,true) |
| 186 | | -> exclude(bmachine:is_discharged_assertion,Assertions,UnProvenAssertions) |
| 187 | | ; UnProvenAssertions = Assertions |
| 188 | | ), |
| 189 | | conjunct_predicates(UnProvenAssertions,UPA). |
| 190 | | |
| 191 | | set_up_transition_or_init(OpName,Operation,ConstantsState,State,NewState,TransInfo,WF) :- |
| 192 | | b_is_initialisation_name(OpName),!, |
| 193 | | State = [], |
| 194 | | set_up_initialisation(ConstantsState,NewState,Operation,TransInfo,WF). |
| 195 | | set_up_transition_or_init(OpName,Operation,ConstantsState,State,NewState,TransInfo,WF) :- |
| 196 | | set_up_transition(OpName,Operation,ConstantsState,State,NewState,TransInfo,WF). |
| 197 | | |
| 198 | | % set up constraints for an operation/event |
| 199 | | set_up_transition(OpName,Operation,ConstantsState,State,NewState,TransInfo,WF) :- |
| 200 | | is_event_b_transition(OpName),!, |
| 201 | | b_get_machine_variables(Variables), |
| 202 | | create_target_state(Variables,_Values,ConstantsState,NewState,WF), |
| 203 | | copy_unmodified_variables(Variables,OpName,State,NewState), |
| 204 | | event_b_transition(OpName,Operation,State,NewState,TransInfo,WF). |
| 205 | | set_up_transition(OpName,Operation,ConstantsState,State,NewState,TransInfo,WF) :- |
| 206 | | b_is_operation_name(OpName),!, |
| 207 | | % classical B |
| 208 | | append(ConstantsState,State,InState), |
| 209 | | append(ConstantsState,NewState,OutState), |
| 210 | | b_get_machine_variables(Variables), |
| 211 | | if(set_up_target_store(InState,OutState),true, |
| 212 | | (add_internal_error('Call failed: ',set_up_target_store(InState,OutState)),fail)), |
| 213 | | copy_unmodified_variables(Variables,OpName,InState,OutState), |
| 214 | | b_execute_top_level_operation_wf(OpName,Operation,_Paras,_Results,InState,OutState,TransInfo,WF). |
| 215 | | set_up_transition(OpName,_,_,_,_,_,_) :- |
| 216 | | add_internal_error('Unknown operation: ',set_up_transition(OpName)),fail. |
| 217 | | |
| 218 | | |
| 219 | | is_event_b_transition(OpName) :- |
| 220 | | b_get_machine_operation(OpName,[],_Parameters,_TEvent,eventb_operation(_ChangeSet,_Values,_Operation),_),!. |
| 221 | | event_b_transition(OpName,Operation,State,NewState,TransInfo,WF) :- |
| 222 | | b_get_machine_operation(OpName,[],Parameters,TEvent,eventb_operation(ChangeSet,Values,Operation),_), |
| 223 | | copy_variable_store(State,ChangeSet,_,NewState), |
| 224 | | b_event_constraints(TEvent,Parameters,Values,State,NewState,TransInfo,WF). |
| 225 | | |
| 226 | | create_target_state(Variables,Values,ConstantsState,NewState,WF) :- |
| 227 | | set_up_typed_localstate(Variables,Values,TypedVals,ConstantsState,NewState,positive), |
| 228 | | b_tighter_enumerate_all_values(TypedVals,WF). |
| 229 | | |
| 230 | | % TODO[DP, 7.4.2011]: refactor, see b_interpreter:b_execute_operation3/13 |
| 231 | | set_up_initialisation(ConstantsState,NewState,Operation,TransInfo,WF) :- |
| 232 | | b_get_machine_variables(Variables), |
| 233 | | create_target_state(Variables,Values,ConstantsState,NewState,WF), |
| 234 | | store:l_expand_and_normalise_values(Values,NormalisedValues), |
| 235 | | safe_univ(Operation,['$initialise_machine'|NormalisedValues]), |
| 236 | | b_safe_get_initialisation_from_machine(Body,OType), |
| 237 | | set_up_initialisation2(OType,Body,Variables,ConstantsState,NewState,TransInfo,WF). |
| 238 | | set_up_initialisation2(classic,Body,Variables,ConstantsState,NewState,[path(Path)],WF) :- |
| 239 | | set_up_undefined_localstate(Variables,ConstantsState,PreInitState), |
| 240 | | empty_state(EmptyState), |
| 241 | | b_execute_top_level_statement(Body,EmptyState,PreInitState,Updates,WF,Path,output_required), |
| 242 | | save_updates_in_existing_store(Updates,NewState). |
| 243 | | set_up_initialisation2(eventb_operation(_,_,_),Body,_Variables,ConstantsState,NewState,TransInfo,WF) :- |
| 244 | | b_event_constraints(Body,[],_Values,ConstantsState,NewState,TransInfo,WF). |
| 245 | | |
| 246 | | set_up_target_store([],Out) :- |
| 247 | | (var(Out) -> Out=[] |
| 248 | | ; true % OutStore already set up by somebody else |
| 249 | | ). |
| 250 | | set_up_target_store([bind(V,_)|In],OutStore) :- |
| 251 | | nonvar(OutStore),!, % OutStore already set up by somebody else |
| 252 | | (OutStore=[bind(VV,_)|T], V==VV |
| 253 | | -> set_up_target_store(In,T) |
| 254 | | ; add_binding(OutStore,V), set_up_target_store(In,OutStore)). |
| 255 | | set_up_target_store([bind(V,_)|In],[bind(V,_)|Out]) :- |
| 256 | | set_up_target_store(In,Out). |
| 257 | | |
| 258 | | add_binding(List,V) :- var(List), !, List = [bind(V,_)|_]. |
| 259 | | add_binding([],V) :- add_internal_error(add_binding,'Variable does not appear in store: ',V,unknown). |
| 260 | | add_binding([bind(VV,_)|T],V) :- |
| 261 | | (V==VV -> true /* ok, found the variable */ |
| 262 | | ; add_binding(T,V)). |
| 263 | | |
| 264 | | % copy over the variables that are not changed by the operation from OldStore to NewStore |
| 265 | | copy_unmodified_variables(Variables,OpName,OldStore,NewStore) :- |
| 266 | | ( get_operation_info(OpName,SubstitutionInfo) -> |
| 267 | | ( memberchk(modifies(ModIDs),SubstitutionInfo) -> |
| 268 | | get_texpr_ids(Variables,Ids), |
| 269 | | exclude(is_modified_var(ModIDs),Ids,UnmodifiedIds), |
| 270 | | maplist(copy_var(OldStore,NewStore),UnmodifiedIds) |
| 271 | | ; |
| 272 | | add_internal_error('Operation/Event has no modifies info: ', |
| 273 | | copy_unmodified_variables(Variables,OpName,OldStore,NewStore)) |
| 274 | | % assume that all variables modified: no copy_var calls |
| 275 | | ) |
| 276 | | ; OpName = 'INITIALISATION' -> true % nothing to copy |
| 277 | | ; OpName = 'SETUP_CONSTANTS' -> true % nothing to copy |
| 278 | | ; |
| 279 | | add_internal_error('Unknown Operation/Event:', copy_unmodified_variables(Variables,OpName,OldStore,NewStore)), |
| 280 | | fail |
| 281 | | ). |
| 282 | | is_modified_var(ModIDs,Id) :- |
| 283 | | memberchk(Id,ModIDs). |
| 284 | | copy_var(OldStore,NewStore,Id) :- |
| 285 | | lookup_value(Id,OldStore,V),lookup_value(Id,NewStore,VNew), |
| 286 | | equal_object(V,VNew). |
| 287 | | |
| 288 | | |
| 289 | | /* --------------------------------------------------------- */ |
| 290 | | % a database of available CBC checks: |
| 291 | | cbc_check('INV_NO_RED', |
| 292 | | 'INV_NO_RED: Find invariants which are redundant', |
| 293 | | Call,Res,Ok) :- Call = (tcltk_find_redundant_invariants(Res,Ok)). |
| 294 | | cbc_check('INV_AXM_SAT', |
| 295 | | 'INV_AXM_SAT: Check if there exists a state that satisfies the INVARIANT and the PROPERTIES (AXIOMS)', |
| 296 | | Call,Res,Ok) :- |
| 297 | | Call = (b_set_up_valid_state(State) -> Ok=true,translate_bstate(State,Res) ; Ok=false, Res='NO_VALID_STATE_FOUND'). |
| 298 | | cbc_check('DLK', |
| 299 | | 'DLK: Check that INVARIANT does not allow a deadlocking state', |
| 300 | | Call,Res,Ok) :- |
| 301 | | Call = (cbc_deadlock_freedom_check(State) -> Ok=false,translate_bstate(State,Res) ; Ok=true, Res='NO_DEADLOCK_FOUND'). |
| 302 | | cbc_check('THM_STATIC', |
| 303 | | 'THM_STATIC: Check that static ASSERTIONS (THEOREMS) follow from PROPERTIES (AXIOMS)', |
| 304 | | Call,TclRes,Ok) :- |
| 305 | | Call = (cbc_static_assertions_check(Res),translate_result(Res,Ok),functor(Res,TclRes,_)). |
| 306 | | %cbc_check('INV/INITIALISATION', |
| 307 | | % 'INV/INITIALISATION: Check if INITIALISATION can violate INVARIANT', |
| 308 | | % Call,TclRes,Ok) :- |
| 309 | | % Call = (tcltk_constraint_based_check_op('$initialise_machine',invariant,Res) -> translate_result(Res,Ok),functor(Res,TclRes,_) ; Ok=true). |
| 310 | | cbc_check(INVO, |
| 311 | | Label, |
| 312 | | Call,Res,Ok) :- |
| 313 | | b_top_level_operation(OpName), |
| 314 | | ajoin(['INV/',OpName],INVO), |
| 315 | | ajoin(['INV/',OpName,': Check that ',OpName,' preserves INVARIANT'],Label), |
| 316 | | Call = (state_model_check(OpName,invariant,_State,_Operation,NewState) |
| 317 | | -> Ok=false,translate_bstate(NewState,Res) ; Ok=true, Res='NO_INVARIANT_violation_found'). |
| 318 | | % TO DO: maybe dynamically generate cbc_checks (inv preservation per event); disable certain checks |
| 319 | | |
| 320 | | :- public translate_result/2. % used above |
| 321 | | translate_result(no_counterexample_found,Ok) :- !, Ok=true. |
| 322 | | translate_result(no_counterexample_exists,Ok) :- !, Ok=true. |
| 323 | | translate_result(no_counterexample_exists(_,_,_),Ok) :- !, Ok=true. |
| 324 | | translate_result(time_out,Ok) :- !, Ok=time_out. |
| 325 | | translate_result(_,false). |
| 326 | | |
| 327 | | tcltk_perform_cbc_check(ID,Text,Result,Ok) :- |
| 328 | | %print(tcltk_perform_cbc_check(ID,Text,Result,Ok)),nl, |
| 329 | | if(cbc_check(ID,Text,Call,Res,Ok), |
| 330 | | (println_silent(Text), |
| 331 | | call(Call), |
| 332 | | Result=Res, |
| 333 | | println_silent(result(Ok,Result)) |
| 334 | | ), |
| 335 | | (add_internal_error('Illegal CBC check: ',tcltk_perform_cbc_check(ID,Text,Result,Ok)), |
| 336 | | fail) |
| 337 | | ). |
| 338 | | % enum_warning:enter_new_error_scope(ScopeID), event_occurred_in_error_scope(enumeration_warning(_,_,_,_)), exit_error_scope(ScopeID,ErrOcc),ErrOcc=true |
| 339 | | |
| 340 | | |
| 341 | | :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]). |
| 342 | | :- public tcltk_find_redundant_invariants/2. |
| 343 | | tcltk_find_redundant_invariants(list(Res),Ok) :- |
| 344 | | cbc_find_redundant_invariants(Invs,Timeout_occured), |
| 345 | | (Invs=[] -> Res = ['NO REDUNDANT INVARIANTS'], Ok=true |
| 346 | | ; Timeout_occured=true -> Res = ['REDUNDANT INVARIANTS (OR WITH TIME-OUT):'|Invs], Ok=false |
| 347 | | ; Res = ['REDUNDANT INVARIANTS:'|Invs], Ok=false). |
| 348 | | |
| 349 | | |
| 350 | | :- dynamic timeout_occured/0. |
| 351 | | cbc_find_redundant_invariants(RedundantInvs,Timeout_occured) :- |
| 352 | | retractall(timeout_occured), |
| 353 | | findall(RI, |
| 354 | | (b_find_redundant_invariant(RedInv,_,R,EnumWarning,ErrOcc), |
| 355 | | translate:translate_bexpression(RedInv,InvString), |
| 356 | | generate_explanation(R,EnumWarning,ErrOcc,InvString,RI), |
| 357 | | (R==time_out -> assertz(timeout_occured) ; true) |
| 358 | | ), |
| 359 | | RedundantInvs), |
| 360 | | (timeout_occured -> Timeout_occured = true ; Timeout_occured=false). |
| 361 | | |
| 362 | | generate_explanation(R,EnumWarning,ErrOcc,InvString,Res) :- |
| 363 | | (EnumWarning=true -> L1=[' /* ENUM WARNING */ '|L2] ; L1=L2), |
| 364 | | (ErrOcc=true -> L2=[' /* REQUIRED FOR WELL-DEFINEDNESS */ '] ; L2=[]), |
| 365 | | (R=redundant -> ajoin([InvString|L1],Res) |
| 366 | | ; R=useful -> EnumWarning=true, ajoin(['ENUMERATION WARNING (POSSIBLY USEFUL): ',InvString|L2],Res) |
| 367 | | ; R=time_out -> ajoin(['TIME OUT (POSSIBLY USEFUL): ',InvString|L1],Res) |
| 368 | | ). |
| 369 | | |
| 370 | | :- use_module(tools_timeout, [time_out_with_factor_call/3]). |
| 371 | | |
| 372 | | b_find_redundant_invariant(RedundantInv,State,Redundant,EnumWarning,ErrOcc) :- |
| 373 | | b_get_invariant_from_machine(Invariant), |
| 374 | | conjunction_to_list(Invariant,InvList), |
| 375 | ? | select(RedundantInv,InvList,RestInvariantList), |
| 376 | | (silent_mode(on) -> true ; |
| 377 | | print('CHECKING REDUNDANCY: '),translate:print_bexpr(RedundantInv),nl), |
| 378 | | create_negation(RedundantInv,NegRed), |
| 379 | | conjunct_predicates(RestInvariantList,AdaptedInvariant), |
| 380 | | %translate:print_bexpr(AdaptedInvariant),nl, |
| 381 | | enter_new_error_scope(ScopeID,b_find_redundant_invariant), |
| 382 | ? | ( time_out_with_factor_call(predicate_satisfiable_relevant_ids(NegRed,AdaptedInvariant,State),5, |
| 383 | | TO=time_out) |
| 384 | | -> (TO==time_out -> Redundant=time_out ; Redundant=useful) |
| 385 | | ; Redundant = redundant), |
| 386 | | (critical_enumeration_warning_occured_in_error_scope -> EnumWarning=true |
| 387 | | ; EnumWarning=false), |
| 388 | | exit_error_scope(ScopeID,ErrOcc,b_find_redundant_invariant), |
| 389 | | printsilent('RESULT: '),printsilent(Redundant),nls. |
| 390 | | |
| 391 | | |
| 392 | | |
| 393 | | /* --------------------------------------------------------- */ |
| 394 | | |
| 395 | | |
| 396 | | |
| 397 | | b_set_up_valid_state(State) :- b_set_up_valid_state_with_pred(State,b(truth,pred,[]),true,none). |
| 398 | | |
| 399 | | b_set_up_valid_state_with_pred(NormalisedState,Pred) :- |
| 400 | | b_set_up_valid_state_with_pred(NormalisedState,Pred,true,none). |
| 401 | | b_set_up_valid_state_with_pred(NormalisedState,Pred,UseInvariant,UseConstantsFromStateID) :- |
| 402 | | %enter_new_error_scope(ScopeID,cbc_find_state), |
| 403 | | predicate_satisfiable_all_ids(Pred,State,UseInvariant,UseConstantsFromStateID), |
| 404 | | normalise_store(State,NormalisedState). |
| 405 | | |
| 406 | | % find a state satisfying the invariant but violating the Assertions |
| 407 | | b_find_dynamic_assertion_violation(NormalisedState) :- |
| 408 | | get_unproven_assertion(UPA), |
| 409 | | create_negation(UPA,NegUPA), |
| 410 | | b_set_up_valid_state_with_pred(NormalisedState,NegUPA,true,none). |
| 411 | | |
| 412 | | % the same as above, but with time-out |
| 413 | | cbc_dynamic_assertions_check(Result) :- |
| 414 | | enter_new_error_scope(ScopeID,cbc_dynamic_assertions_check), |
| 415 | | start_ms_timer(Timer), |
| 416 | | ( time_out_with_factor_call(b_find_dynamic_assertion_violation(State),10,TO=time_out) -> |
| 417 | | (TO==time_out -> Result = time_out ; Result = counterexample_found(State)) |
| 418 | | ; critical_enumeration_warning_occured_in_error_scope -> Result = no_counterexample_found |
| 419 | | ; Result = no_counterexample_exists |
| 420 | | ), |
| 421 | | (debug_mode(on) -> print('cbc_dynamic_assertions_check: '),stop_ms_timer(Timer) ; true), |
| 422 | | exit_error_scope(ScopeID,_ErrOcc,cbc_dynamic_assertions_check). |
| 423 | | |
| 424 | | /* ---------------------- */ |
| 425 | | /* DEADLOCK FREEDOM CHECK */ |
| 426 | | /* ---------------------- */ |
| 427 | | |
| 428 | | :- use_module(bsyntaxtree,[predicate_identifiers/2]). |
| 429 | | :- use_module(b_ast_cleanup,[predicate_level_optimizations/2]). |
| 430 | | |
| 431 | | :- public cbc_deadlock_freedom_check/1. % used above |
| 432 | | cbc_deadlock_freedom_check(State) :- |
| 433 | | create_texpr(truth,pred,[],True), Filter=0, |
| 434 | | cbc_deadlock_freedom_check(State,True,Filter). |
| 435 | | |
| 436 | | % if Filter=1 we filter out guards which are inconsistent with the goal before solving the full predicate |
| 437 | | cbc_deadlock_freedom_check(State,Goal,Filter) :- |
| 438 | | debug_println(19,cbc_deadlock_freedom_check(State,Filter)),flush_output, |
| 439 | | ( is_truth(Goal) -> |
| 440 | | get_all_guards_false_pred(Target) |
| 441 | | ; |
| 442 | | print('Adding additional goal predicate: '),nl, |
| 443 | | print_bexpr(Goal),nl, |
| 444 | | ( Filter=1 -> |
| 445 | | get_all_guards_false_pred(AllGFalse,Goal) |
| 446 | | ; |
| 447 | | get_all_guards_false_pred(AllGFalse)), |
| 448 | | conjunct_predicates([AllGFalse,Goal],Target) |
| 449 | | ),!,flush_output, |
| 450 | | statistics(runtime,[Start,_]), |
| 451 | | statistics(walltime,[WStart,_]), |
| 452 | ? | cbc_deadlock_freedom_check2(Target,RState,Start,WStart,false,TO), % TO DO: control SkipIrrelevantComponents by preference or GUI |
| 453 | | (TO==time_out -> State=time_out ; State=RState). |
| 454 | | cbc_deadlock_freedom_check2(Target,NormalisedState,Start,WStart,SkipIrrelevantComponents,TO) :- |
| 455 | | get_texpr_expr(Target,T), T \= falsity, |
| 456 | | b_get_properties_from_machine(Properties), |
| 457 | | b_get_invariant_from_machine(Invariant), |
| 458 | | conjunct_predicates([Properties,Invariant,Target],Pred1), |
| 459 | | b_get_machine_variables(Variables), |
| 460 | | b_get_machine_constants(Constants), append(Constants,Variables,CV), |
| 461 | | |
| 462 | | apply_kodkod_or_other_optimisations(CV,Pred1,Pred), |
| 463 | | %predicate_level_optimizations(Pred2,Pred), % detect set partitions, etc..., now done inside b_interpreter_components |
| 464 | | |
| 465 | | set_up_typed_localstate_for_pred(CV,Pred,TypedVals,State), |
| 466 | | b_interpreter_components:reset_component_info(false), |
| 467 | | (debug_mode(on) -> translate:nested_print_bexpr_as_classicalb(Pred) ; true), |
| 468 | | %%visualize_graph:print_predicate_dependency_as_graph_for_dot(Pred,'~/Desktop/pdg.dot'), |
| 469 | | (SkipIrrelevantComponents==true |
| 470 | | -> predicate_identifiers(Target,TargetIds) % Warning: can skip over obvious inconsistencies TRUE:BOOL |
| 471 | | ; TargetIds=all), |
| 472 | | println_silent(target(TargetIds)), |
| 473 | | b_global_sets:static_symmetry_reduction_for_global_sets(State), |
| 474 | ? | time_out_with_factor_call( |
| 475 | | b_interpreter_components:b_trace_test_components(Pred,State,TypedVals,TargetIds), |
| 476 | | 10, (nl,TO=time_out)), |
| 477 | | statistics(runtime,[Stop,_]), Time is Stop - Start, |
| 478 | | statistics(walltime,[WStop,_]), WTime is WStop - WStart, |
| 479 | | (TO==time_out -> println_silent(time_out_during_deadlock_checking(Time)), NormalisedState=State |
| 480 | | ; TO=no_time_out, println_silent(deadlock_counter_example_found(Time,WTime)), |
| 481 | | normalise_store(State,NormalisedState) |
| 482 | | ). |
| 483 | | cbc_deadlock_freedom_check2(Target,_State,Start,WStart,_,no_time_out) :- |
| 484 | | (get_texpr_expr(Target,falsity) -> println_silent('Disjunction of guards obviously true') ; true), |
| 485 | | statistics(runtime,[Stop,_]), Time is Stop - Start, |
| 486 | | statistics(walltime,[WStop,_]), WTime is WStop - WStart, |
| 487 | | println_silent(no_deadlock_counter_example_found(Time,WTime)), %print_silent |
| 488 | | fail. |
| 489 | | |
| 490 | | % test if a predicate can be satisfied for some instantiation of constants and variables |
| 491 | | predicate_satisfiable(P) :- predicate_satisfiable(P,_),!, print('SATISFIABLE'),nl,nl. |
| 492 | | predicate_satisfiable(_) :- print('*UNSATISFIABLE*'),nl,nl,fail. |
| 493 | | predicate_satisfiable(Predicate,State) :- |
| 494 | | b_get_invariant_from_machine(Invariant), |
| 495 | | predicate_satisfiable_relevant_ids(Predicate,Invariant,State). |
| 496 | | |
| 497 | | predicate_satisfiable_all_ids(Predicate,State,UseInvariant,UseConstantsFromStateID) :- |
| 498 | | (UseInvariant=true -> b_get_invariant_from_machine(Invariant) ; create_texpr(truth,pred,[],Invariant)), |
| 499 | | predicate_satisfiable5(Predicate,Invariant,State,all,UseConstantsFromStateID). % all: look at all variables/constants: we want a complete solution |
| 500 | | |
| 501 | | predicate_satisfiable_relevant_ids(Predicate,Invariant,State) :- |
| 502 | | predicate_identifiers(Predicate,RelevantIds), % only look at relevant ids for Predicate; skip over components not involving them |
| 503 | ? | predicate_satisfiable5(Predicate,Invariant,State,RelevantIds,none). |
| 504 | | |
| 505 | | :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]). |
| 506 | | :- use_module(state_space,[get_constants_state_for_id/2]). |
| 507 | | predicate_satisfiable5(Predicate,Invariant,State,RelevantIds,UseConstantsFromStateID) :- |
| 508 | | (number(UseConstantsFromStateID), |
| 509 | | get_constants_state_for_id(UseConstantsFromStateID,UseCState) |
| 510 | | -> % instead of finding solutions to constants we re-use the constants found in an existing state |
| 511 | | Constants=[], ReuseConstants=true, |
| 512 | | debug_format(19,'Reusing constant values from state id ~w~n',[UseConstantsFromStateID]), |
| 513 | | Properties = b(truth,pred,[]) % no need to check properties |
| 514 | | ; b_get_properties_from_machine(Properties), |
| 515 | | b_get_machine_constants(Constants), |
| 516 | | UseCState=[], ReuseConstants=false |
| 517 | | ), |
| 518 | | conjunct_predicates([Properties,Invariant,Predicate],TotPred0), |
| 519 | | b_get_machine_variables(Variables), |
| 520 | | append(Constants,Variables,CV), |
| 521 | | set_up_typed_localstate_for_pred(CV,TotPred0,TypedVals,State0), |
| 522 | | append(UseCState,State0,State), |
| 523 | | apply_kodkod_or_other_optimisations(CV,TotPred0,TotPred), |
| 524 | | %predicate_level_optimizations(TotPred1,TotPred), %now done inside b_interpreter_components |
| 525 | | b_interpreter_components:reset_component_info(false), |
| 526 | | (debug_mode(off) -> true ; translate:nested_print_bexpr_as_classicalb(Predicate)), |
| 527 | | (ReuseConstants==false |
| 528 | | -> b_global_sets:static_symmetry_reduction_for_global_sets(State) |
| 529 | | % we could check if there is just a single solution for constants, |
| 530 | | ; true |
| 531 | | ), |
| 532 | | add_prob_deferred_set_elements_to_store(State,State1,visible), |
| 533 | | % TO DO: catch time-outs |
| 534 | ? | b_interpreter_components:b_trace_test_components(TotPred,State1,TypedVals,RelevantIds). |
| 535 | | |
| 536 | | % we could call solve_components in solver_interface or solve_predicate directly |
| 537 | | % we could provide options to call setlog, Z3, WD prover, ... |
| 538 | | % we could also integrate this into apply_kodkod_or_other_optimisations |
| 539 | | % should we merge with solve_cbc_predicate_over_constants |
| 540 | | |
| 541 | | % -------------- |
| 542 | | |
| 543 | | % set up a predicate which is true if all guards are false |
| 544 | | get_all_guards_false_pred(AllGuardsFalsePred) :- |
| 545 | | findall(NegGuard, |
| 546 | | (b_is_operation_name(OpName), |
| 547 | | get_negated_guard(OpName,_,NegGuard)), ListOfNegGuards), |
| 548 | | conjunct_and_sort_smt_predicates(ListOfNegGuards,AllGuardsFalsePred). |
| 549 | | get_all_guards_false_pred(AllGuardsFalsePred,FilterPred) :- |
| 550 | | findall(NegGuard, |
| 551 | | (b_is_operation_name(OpName), |
| 552 | | get_negated_guard(OpName,Guard,NegGuard), |
| 553 | | conjunct_predicates([Guard,FilterPred],FGuard), |
| 554 | | nls,printsilent('---> CHECKING IF GUARD SATISFIABLE: '), printsilent(OpName),nls, |
| 555 | | predicate_satisfiable(FGuard) % if Guard not satisfiable given FilterPred: remove it |
| 556 | | ), ListOfNegGuards), |
| 557 | | conjunct_and_sort_smt_predicates(ListOfNegGuards,AllGuardsFalsePred). |
| 558 | | |
| 559 | | % the following is useful, e.g., for graphical visualization |
| 560 | | get_unsorted_all_guards_false_pred(AllGuardsFalsePred) :- |
| 561 | | findall(NegGuard, |
| 562 | | (b_is_operation_name(OpName), |
| 563 | | get_negated_guard(OpName,_,NegGuard)), ListOfNegGuards), |
| 564 | | conjunct_predicates(ListOfNegGuards,AllGuardsFalsePred). |
| 565 | | |
| 566 | | conjunct_and_sort_smt_predicates(List,Result) :- |
| 567 | | debug_println(9,'Counting basic predicates'), |
| 568 | | empty_avl(Ai), count(List,2,Ai,Ao), |
| 569 | | % portray_avl(Ao),nl, |
| 570 | | sort_smt_predicates(List,Ao,SList), |
| 571 | | %nl,print(sorted(SList)),nl, |
| 572 | | conjunct_smt_predicates(SList,Result) , debug_println(9,finished). |
| 573 | | |
| 574 | | conjunct_smt_predicates([],b(truth,pred,[])). |
| 575 | | conjunct_smt_predicates([P|T],Res) :- conjunct_smt_predicates(T,TRes), |
| 576 | | extract_info(P,TRes,Info), % extract e.g., wd condition info |
| 577 | | conjoin(P,TRes,[try_smt|Info],Res). % try_smt currently no longer useful ? |
| 578 | | |
| 579 | | % Count the number of occurences of given basic predicates |
| 580 | | count(b(Pred,pred,_Info),Rel,Ai,Ao) :- !,count2(Pred,Rel,Ai,Ao). |
| 581 | | count([],_,Ai,Ao) :- !,Ao=Ai. |
| 582 | | count([H|T],Rel,Ai,Ao) :- !,count(H,Rel,Ai,Aii), count(T,Rel,Aii,Ao). |
| 583 | | count(R,_,_,_) :- add_error_fail(count,'Illegal argument to count: ',R). |
| 584 | | |
| 585 | | count2(negation(Pred),Rel,Ai,Ao) :- !, count(Pred,Rel,Ai,Ao). |
| 586 | | count2(conjunct(A,B),Rel,Ai,Ao) :- !, count(A,Rel,Ai,Aii), count(B,Rel,Aii,Ao). |
| 587 | | count2(Pred,Rel,Ai,Ao) :- disjunctive_pred(Pred,A,B),!, |
| 588 | | (Rel>1 |
| 589 | | -> R1 is Rel-1, count(A,R1,Ai,Aii), count(B,R1,Aii,Ao) |
| 590 | | ; Ai=Ao). |
| 591 | | count2(Pred,Rel,Ai,Ao) :- smt_predicate(Pred),!, norm_pred(Pred,NP), |
| 592 | | (avl_fetch(NP,Ai,C1) -> Count is C1+Rel ; Count = Rel), |
| 593 | | avl_store(NP,Ai,Count,Ao). |
| 594 | | count2(_Pred,_Rel,A,A). |
| 595 | | |
| 596 | | disjunctive_pred(disjunct(A,B),A,B). |
| 597 | | disjunctive_pred(implication(A,B),A,B). |
| 598 | | disjunctive_pred(equivalence(A,B),A,B). |
| 599 | | |
| 600 | | |
| 601 | | sort_smt_predicates(b(Pred,pred,Info),Ai,b(SP,pred,Info)) :- sort_smt_predicates2(Pred,Ai,SP). |
| 602 | | sort_smt_predicates([],_,[]). |
| 603 | | sort_smt_predicates([H|T],Ai,[SH|ST]) :- sort_smt_predicates(H,Ai,SH), sort_smt_predicates(T,Ai,ST). |
| 604 | | |
| 605 | | sort_smt_predicates2(negation(Pred),AVL,negation(SPred)) :- !,sort_smt_predicates(Pred,AVL,SPred). |
| 606 | | sort_smt_predicates2(implication(A,B),AVL,implication(SA,SB)) :- !, |
| 607 | | sort_smt_predicates(A,AVL,SA), sort_smt_predicates(B,AVL,SB). |
| 608 | | sort_smt_predicates2(equivalence(A,B),AVL,equivalence(SA,SB)) :- !, |
| 609 | | sort_smt_predicates(A,AVL,SA), sort_smt_predicates(B,AVL,SB). |
| 610 | | sort_smt_predicates2(disjunct(A,B),AVL,disjunct(SA,SB)) :- !, % To do: also sort disjuncts |
| 611 | | sort_smt_predicates(A,AVL,SA), sort_smt_predicates(B,AVL,SB). |
| 612 | | sort_smt_predicates2(conjunct(A,B),AVL,Res) :- !, |
| 613 | | conjunction_to_count_list(b(conjunct(A,B),pred,[]),AVL,CountList), |
| 614 | | sort(CountList,SC), |
| 615 | | reverse(SC,SortedCList), % to do : use samsort with custom order |
| 616 | | project_count_list(SortedCList,PR), |
| 617 | | conjunct_smt_predicates(PR,BRes), |
| 618 | | (debug_mode(on) -> translate:print_bexpr(BRes),nl ; true), |
| 619 | | BRes = b(Res,pred,_). |
| 620 | | sort_smt_predicates2(X,_,X). |
| 621 | | |
| 622 | | project_count_list([],[]). |
| 623 | | project_count_list([count(_,P)|T],[P|PT]) :- project_count_list(T,PT). |
| 624 | | |
| 625 | | conjunction_to_count_list(C,AVL,List) :- is_a_conjunct(C,LHS,RHS),!, |
| 626 | | conjunction_to_count_list(LHS,AVL,L1), |
| 627 | | conjunction_to_count_list(RHS,AVL,R1), |
| 628 | | append(L1,R1,List). % TO DO: improve, use Difference Lists |
| 629 | | conjunction_to_count_list(b(Pred,pred,Info),AVL,[count(Count,b(Pred,pred,Info))]) :- smt_predicate(Pred),!, |
| 630 | | norm_pred(Pred,NX), |
| 631 | | (avl_fetch(NX,AVL,Count) -> true ; Count=0). |
| 632 | | conjunction_to_count_list(P,_AVL,[count(0,P)]). |
| 633 | | |
| 634 | | smt_predicate(equal(_,_)). |
| 635 | | smt_predicate(not_equal(_,_)). |
| 636 | | smt_predicate(member(_,_)). |
| 637 | | smt_predicate(not_member(_,_)). |
| 638 | | smt_predicate(less(_,_)). |
| 639 | | smt_predicate(less_equal(_,_)). |
| 640 | | smt_predicate(greater(_,_)). |
| 641 | | smt_predicate(greater_equal(_,_)). |
| 642 | | |
| 643 | | norm_pred(equal(A,B),Res) :- !,norm_equal(A,B,Res). |
| 644 | | norm_pred(not_equal(A,B),Res) :- !,norm_equal(A,B,Res). |
| 645 | | norm_pred(member(A,B),member(AA,BB)) :- !,norm_pred(A,AA),norm_pred(B,BB). |
| 646 | | norm_pred(not_member(A,B),member(AA,BB)) :- !,norm_pred(A,AA),norm_pred(B,BB). |
| 647 | | norm_pred(less(A,B),less(AA,BB)) :- !,norm_pred(A,AA),norm_pred(B,BB). |
| 648 | | norm_pred(greater(A,B),less(BB,AA)) :- !,norm_pred(A,AA),norm_pred(B,BB). |
| 649 | | norm_pred(less_equal(A,B),less(BB,AA)) :- !,norm_pred(A,AA),norm_pred(B,BB). |
| 650 | | norm_pred(greater_equal(A,B),less(AA,BB)) :- !,norm_pred(A,AA),norm_pred(B,BB). |
| 651 | | norm_pred(b(B,_,_),Res) :- !, norm_pred(B,Res). |
| 652 | | norm_pred(set_extension(L),Res) :- !, Res=set_extension(NL), norm_pred(L,NL). |
| 653 | | norm_pred(integer(A),Res) :- !,Res=A. |
| 654 | | norm_pred(identifier(A),Res) :- !,Res=A. |
| 655 | | norm_pred([],Res) :- !, Res=[]. |
| 656 | | norm_pred([H|T],Res) :- !, Res=[NH|NT], norm_pred(H,NH), norm_pred(T,NT). |
| 657 | | norm_pred(X,X). |
| 658 | | |
| 659 | | |
| 660 | | norm_equal(b(identifier(ID),_,_),_B,Res) :- !,Res=ID. |
| 661 | | norm_equal(A,B,Res) :- norm_pred(A,AA),norm_pred(B,BB), |
| 662 | | (AA==boolean_false -> AAA=boolean_true ; AAA=AA), |
| 663 | | (BB==boolean_false -> BBB=boolean_true ; BBB=BB), |
| 664 | | (BBB @< AAA -> Res = equal(AAA,BBB) ; Res= equal(BBB,AAA)). |
| 665 | | /* |
| 666 | | operation_satisfiable(OpName,FilterPred) :- get_machine_operation(OpName,_,_,_), |
| 667 | | get_negated_guard(OpName,Guard,_NegGuard), |
| 668 | | conjunct_predicates([Guard,FilterPred],FGuard), |
| 669 | | print('CHECKING IF GUARD SATISFIABLE: '), print(OpName),nl, |
| 670 | | predicate_satisfiable(FGuard).*/ |
| 671 | | |
| 672 | | % Optionally: Remove certain complicated parts from the guards |
| 673 | | /* |
| 674 | | simplify_guard(b(Pred,pred,Info),SPred) :- simplify_guard2(Pred,Info,SPred). |
| 675 | | simplify_guard2(conjunct(A,B),Info,Res) :- !, |
| 676 | | simplify_guard(A,SA), simplify_guard(B,SB), |
| 677 | | conjoin(SA,SB,Info,Res). |
| 678 | | simplify_guard2(exists(P,B),_Info,R) :- !, R=b(truth,pred,[]), |
| 679 | | print('REMOVED: '),translate:print_bexpr(b(exists(P,B),pred,[])),nl. |
| 680 | | simplify_guard2(X,Info,b(X,pred,Info)). |
| 681 | | */ |
| 682 | | |
| 683 | | conjoin(b(truth,_,_),B,_,R) :- !,R=B. |
| 684 | | conjoin(b(falsity,_,_),_B,_,R) :- !,R=b(falsity,pred,[]). |
| 685 | | conjoin(A,b(truth,_,_),_,R) :- !,R=A. |
| 686 | | conjoin(_A,b(falsity,_,_),_,R) :- !,R=b(falsity,pred,[]). |
| 687 | | conjoin(A,B,Info,b(conjunct(A,B),pred,Info)). |
| 688 | | |
| 689 | | get_negated_guard(OpName,Guard,NegationOfGuard) :- get_negated_guard(OpName,Guard,NegationOfGuard,_Precise). |
| 690 | | get_negated_guard(OpName,Guard,NegationOfGuard,Precise) :- |
| 691 | | get_guard_and_precision(OpName,Guard,Precise), |
| 692 | | SGuard=Guard, |
| 693 | | %simplify_guard(Guard,SGuard), %% comment in to remove complicated parts |
| 694 | | create_negation(SGuard,NegationOfGuard). % we used to add try_smt Info; no longer relevant !? |
| 695 | | |
| 696 | | |
| 697 | | :- use_module(b_operation_guards,[get_simplified_operation_enabling_condition/5]). |
| 698 | | %:- use_module(b_ast_cleanup, [clean_up/3]). |
| 699 | | :- use_module(b_interpreter_components,[construct_optimized_exists/3]). |
| 700 | | |
| 701 | | % get a guard, by translating all parameters into existential quantifiers |
| 702 | | get_guard(OpName,Guard) :- get_guard_and_precision(OpName,Guard,_). |
| 703 | | get_guard_and_precision(OpName,Guard,Precise) :- |
| 704 | | get_simplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,Precise), |
| 705 | | % Precise is either precise or imprecise |
| 706 | | % TO DO: partition; avoid lifting becomes_such_that conditions |
| 707 | | % (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok) |
| 708 | | construct_optimized_exists(Parameters,EnablingCondition,Guard). |
| 709 | | |
| 710 | | /* --------------------------------------------------------- */ |
| 711 | | |
| 712 | | :- use_module(tools_printing,[print_error/1]). |
| 713 | | b_check_valid_state(State) :- |
| 714 | | (b_valid_state(State) -> true |
| 715 | | ; print_error('Invalid State:'), |
| 716 | | print_error(State) |
| 717 | | ). |
| 718 | | |
| 719 | | b_valid_state(State) :- |
| 720 | | b_get_machine_variables(Variables), |
| 721 | | b_check_variable_types(Variables,State). |
| 722 | | |
| 723 | | |
| 724 | | % TODO(DP,6.5.2008): removed type check |
| 725 | | :- assert_pre(b_state_model_check:b_check_variable_types(V,S), (list_skeleton(V),list_skeleton(S))). |
| 726 | | % (list_skeleton(V),list_skeleton(VT),list_skeleton(S))). |
| 727 | | :- assert_post(b_state_model_check:b_check_variable_types(_V,_S),true). |
| 728 | | |
| 729 | | b_check_variable_types([],_). |
| 730 | | b_check_variable_types([Var|VT],State) :- |
| 731 | | def_get_texpr_id(Var,VarID), get_texpr_type(Var,Type), |
| 732 | | (store:lookup_value_for_existing_id(VarID,State,Val), |
| 733 | | Val\==fail |
| 734 | | -> (kernel_objects:basic_type(Val,Type) |
| 735 | | -> true |
| 736 | | ; print_error('Type Error ! Variable,Value,Type: '),print_error(VarID), |
| 737 | | print_error(Val),print_error(Type) |
| 738 | | ), |
| 739 | | b_check_variable_types(VT,State) |
| 740 | | ; add_error(b_check_variable_types,'Variable not defined in state: ', VarID), |
| 741 | | add_error(b_check_variable_types,'Be sure that INITIALISATION initialises the variable: ', VarID), |
| 742 | | print_error(State) |
| 743 | | ). |
| 744 | | |
| 745 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 746 | | % constraint based assertion check |
| 747 | | :- use_module(preferences). |
| 748 | | |
| 749 | | cbc_static_assertions_check(Result) :- cbc_static_assertions_check(Result,[]). |
| 750 | | % currently supported options: tautology_check : check that assertions are tautologies |
| 751 | | cbc_static_assertions_check(Result,Options) :- |
| 752 | ? | get_cbc_assertions_predicate_to_solve(Options, Constants, TotalPredicate,true,_), |
| 753 | | enter_new_error_scope(ScopeID,cbc_static_assertions_check), |
| 754 | | start_ms_timer(Timer), |
| 755 | | (member(observe_state,Options) -> external_functions:observe_state(State) ; true), |
| 756 | ? | ( time_out_with_factor_call(cbc_static_assertions_check2(State,Constants, TotalPredicate),10,TO=time_out) |
| 757 | | % counter example was found or time out reached: |
| 758 | | -> (TO==time_out -> Result = time_out ; Result = counterexample_found(State)) |
| 759 | | % cbc_static_assertions check did not find a counter exmaple: |
| 760 | ? | ; critical_enumeration_warning_occured_in_error_scope -> Result = no_counterexample_found |
| 761 | | ; get_elapsed_walltime(Timer,WTime), |
| 762 | ? | cbc_static_assertions_contradiction_check(Constants,TotalPredicate,Result,Options,WTime) |
| 763 | | ), |
| 764 | | (debug_mode(on) -> print('cbc_static_assertions_check: '),stop_ms_timer(Timer) ; true), |
| 765 | | exit_error_scope(ScopeID,_ErrOcc,cbc_static_assertions_check). |
| 766 | | |
| 767 | | % in case of proof: check if we can establish a contradiction in the hypotheses |
| 768 | | cbc_static_assertions_contradiction_check(Constants,TotalPredicate,Result,Options,_) :- |
| 769 | ? | member(contradiction_check,Options), |
| 770 | | println_silent('Looking for contradiction in hypothesis'), |
| 771 | ? | get_cbc_assertions_predicate_to_solve(Options, Constants, TotalPredicate2,false,Goal), |
| 772 | | start_ms_timer(Timer), |
| 773 | | (time_out_with_factor_call(cbc_static_assertions_check2(_,Constants, TotalPredicate2),10,TO=time_out) |
| 774 | | -> debug_println(no_contradiction(TO)),fail ; true), |
| 775 | | get_elapsed_walltime(Timer,WTime), |
| 776 | | (critical_enumeration_warning_occured_in_error_scope |
| 777 | | -> print(no_contradiction(enumeration_warning)),nl,fail ; true), |
| 778 | | !, |
| 779 | | println_silent('*** CONTRADICTION IN HYPOTHESIS FOUND !'), |
| 780 | | translate:translate_bexpression_with_limit(Goal,GS), |
| 781 | | add_warning(contradiction_in_hypotheses, |
| 782 | | 'Prover double check result: Contradiction in hypotheses (or Bug) detected for goal: ',GS), |
| 783 | ? | compute_unsat_core_if_requested(Options,TotalPredicate2,WTime), |
| 784 | | Result = no_counterexample_exists(Constants,TotalPredicate,[contradiction_in_hypotheses]). |
| 785 | | cbc_static_assertions_contradiction_check(Constants,TotalPredicate,Result,Options,WTime) :- |
| 786 | | compute_unsat_core_if_requested(Options,TotalPredicate,WTime), |
| 787 | | Result = no_counterexample_exists(Constants,TotalPredicate,[]). |
| 788 | | |
| 789 | | cbc_static_assertions_check2(concrete_constants(NormalisedState),Constants, TotalPredicate) :- |
| 790 | ? | solve_cbc_predicate_over_constants(Constants,TotalPredicate,NormalisedState). |
| 791 | | |
| 792 | | |
| 793 | | %:- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate/4]). |
| 794 | | %solve_cbc_predicate_over_constants(_TypedConstants,TotalPredicate,NormalisedState) :- |
| 795 | | % %print(TypedConstants),nl, |
| 796 | | % translate:nested_print_bexpr(TotalPredicate),nl, |
| 797 | | % Solver=z3, |
| 798 | | % smt_solve_predicate(Solver,TotalPredicate,NormalisedState,Result), |
| 799 | | % % possible results: contradiction_found, no_solution_found(Reason), time_out, solution(_) |
| 800 | | % print(solver_res(Solver,Result)),nl, |
| 801 | | % (Result = contradiction_found -> !, fail ; Result = solution(_) -> !). |
| 802 | | solve_cbc_predicate_over_constants(Constants,TotalPredicate,NormalisedState) :- |
| 803 | | empty_state(EmptyState), |
| 804 | ? | set_up_typed_localstate(Constants,_FreshVars1,TypedVals,EmptyState,State,positive), |
| 805 | | b_global_sets:static_symmetry_reduction_for_global_sets(State), |
| 806 | | apply_kodkod_or_other_optimisations(Constants,TotalPredicate,TotPred), |
| 807 | | %predicate_level_optimizations(TotPred1,TotPred), % now done inside b_interpreter_components |
| 808 | | b_interpreter_components:reset_component_info(false), |
| 809 | | % TO DO: prioritise components containing parts/variables from Assertions (see set_projection_on_static_assertions/) |
| 810 | ? | b_interpreter_components:b_trace_test_components(TotPred,State,TypedVals,all), |
| 811 | | normalise_store(State,NormalisedState). |
| 812 | | |
| 813 | | |
| 814 | | |
| 815 | | % input Options: output: list of identifiers over which predicate solved + predicate itself |
| 816 | | get_cbc_assertions_predicate_to_solve(Options, Constants, TotalPredicate,NegateGoal,NegGoal) :- |
| 817 | ? | get_cbc_assertions_sequent(Options, Constants, Properties, GoalToProve), |
| 818 | | conjunct_predicates(GoalToProve,GoalC), |
| 819 | | (debug_mode(on) -> print('Trying to prove goal: '),nl,translate:nested_print_bexpr_as_classicalb(GoalC) ; true), |
| 820 | | (NegateGoal=true -> create_negation(GoalC,NegGoal) ; NegGoal=GoalC), |
| 821 | | %% print('Using Hypotheses: '),nl,translate:nested_print_bexpr_as_classicalb(Properties), %% |
| 822 | | conjunct_predicates([NegGoal,Properties],TotalPredicate). |
| 823 | | |
| 824 | | % ------------------------ |
| 825 | | |
| 826 | | get_cbc_assertions_sequent(Options, Constants, Properties, GoalToProve) :- |
| 827 | | b_get_machine_constants(AllConstants), |
| 828 | | (member(specific(Label),Options) -> WhichAss=specific(Label) |
| 829 | | ; member(main_assertions,Options) -> WhichAss=main |
| 830 | | ; WhichAss=all), |
| 831 | ? | b_get_assertions(WhichAss,static,Assertions), |
| 832 | | (get_preference(use_po,true), nonmember(tautology_check,Options) |
| 833 | | -> exclude(bmachine:is_discharged_assertion,Assertions,UnProvenAssertions) |
| 834 | | ; UnProvenAssertions = Assertions |
| 835 | | ), |
| 836 | ? | (member(tautology_check,Options) |
| 837 | | % used for ProB as an Atelier-B disprover/prover: the ASSERTIONS are an implication |
| 838 | | -> find_identifier_uses_l(UnProvenAssertions,[],Ids), |
| 839 | | include(id_mem(Ids),AllConstants,Constants), % only include constants used in tautology |
| 840 | | construct_sequent(UnProvenAssertions,Properties,GoalToProve) |
| 841 | | ; % Sequent: Properties |- UnProvenAssertions |
| 842 | | b_get_properties_from_machine(Properties), |
| 843 | | Constants = AllConstants, |
| 844 | | GoalToProve = UnProvenAssertions |
| 845 | | ). |
| 846 | | |
| 847 | | construct_sequent([IMPLICATION],HYP,[RHS]) :- |
| 848 | | is_an_implication(IMPLICATION,HYP,RHS),!. |
| 849 | | construct_sequent([b(negation(HYP),pred,I)],HYP,[RHS]) :- % relevant for test 1451 |
| 850 | ? | member(was(implication),I), |
| 851 | | !, |
| 852 | | RHS=b(falsity,pred,[]). |
| 853 | | construct_sequent(UPAssertions,b(truth,pred,[]),UPAssertions). |
| 854 | | |
| 855 | ? | id_mem(IDList,TID) :- get_texpr_id(TID,ID), member(ID,IDList). |
| 856 | | |
| 857 | | :- use_module(extrasrc(unsat_cores),[unsat_core_list_with_time_limit/5]). |
| 858 | | compute_unsat_core_if_requested(Options,Predicate,WTime) :- |
| 859 | | member(unsat_core,Options),!, |
| 860 | | format('Computing UNSAT CORE (~w ms to find initial contradiction)~n',[WTime]), |
| 861 | | UCOptions=[], |
| 862 | ? | unsat_core_list_with_time_limit(Predicate,WTime,UCOptions,no_solution_found,CorePredicates), |
| 863 | | nl,print('UNSAT CORE: '),nl, |
| 864 | | print('--------'),nl, |
| 865 | | translate:nested_print_bexpr_as_classicalb(CorePredicates), |
| 866 | | print('--------'),nl. |
| 867 | | compute_unsat_core_if_requested(_,_,_). |
| 868 | | |
| 869 | | |
| 870 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 871 | | |
| 872 | | copy_binding_skel(bind(Id,_),bind(Id,_)). |
| 873 | | |
| 874 | | execute_operation_by_predicate_in_state(InVarsState,OpName,Predicate,Operation,OutVariablesState) :- |
| 875 | ? | execute_operation_by_predicate_in_state_with_pos(InVarsState,OpName,Predicate,Operation,OutVariablesState,unknown). |
| 876 | | |
| 877 | | :- use_module(state_space,[visited_expression/2]). |
| 878 | | % execute an operation in a state with an additional predicate |
| 879 | | % the predicate can talk about parameters, return values, the after state |
| 880 | | % and the before state using $0 identifiers. |
| 881 | | % Predicate usually parsed by b_parse_machine_operation_pre_post_predicate |
| 882 | | execute_operation_by_predicate_in_state_with_pos(const_and_vars(ID,InVariablesState),OpName,Predicate,Operation, |
| 883 | | const_and_vars(ID,OutVariablesState),Pos) :- !, |
| 884 | | visited_expression(ID,concrete_constants(ConstantsState)), |
| 885 | ? | execute_operation_by_predicate_in_state2(ConstantsState,InVariablesState,OpName,Predicate, |
| 886 | | Operation,OutVariablesState,Pos). |
| 887 | | execute_operation_by_predicate_in_state_with_pos(InVariablesState,OpName,Predicate,Operation,OutVariablesState,Pos) :- |
| 888 | ? | execute_operation_by_predicate_in_state2([],InVariablesState,OpName,Predicate,Operation,OutVariablesState,Pos). |
| 889 | | |
| 890 | | :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]). |
| 891 | | execute_operation_by_predicate_in_state2(ConstantsState,InVariablesState,OpName,Predicate, |
| 892 | | Operation,NormalisedOutVariablesState,PositionInfo) :- |
| 893 | | b_get_machine_variables(Variables), |
| 894 | | maplist(copy_binding_skel,InVariablesState,OutVariablesState), |
| 895 | | copy_unmodified_variables(Variables,OpName,InVariablesState,OutVariablesState), |
| 896 | | % format(' ** Copied for ~w: ~w~n',[OpName,OutVariablesState]), |
| 897 | | init_wait_flags_with_call_stack(WF,[operation_call(OpName,ParamValues,PositionInfo)]), |
| 898 | | add_prob_deferred_set_elements_to_store(ConstantsState,ConstantsState1,visible), |
| 899 | | append(ConstantsState1,InVariablesState,In), |
| 900 | | append(ConstantsState1,OutVariablesState,Out), |
| 901 | | % for Event-B we have to add b_machine_temp_predicate |
| 902 | | % b_execute_operation_with_parameters(Name,LocalState,InState,Results,Parameters,OutState,ParamValues,ResultValues,Path,Info,WF,OR) |
| 903 | | b_execute_top_level_operation_wf(OpName,Operation,ParamValues,ResultValues,In,Out,_TransInfo,WF), |
| 904 | | % format(' ** Exec for ~w (~w) --> ~w: ~w~n',[OpName,ParamValues,ResultValues,OutVariablesState]), |
| 905 | | setup_local_state_for_operation(OpName,ParamValues,ResultValues,OpLocalState), |
| 906 | | maplist(create_primed_binding,InVariablesState,PrimedVars), |
| 907 | | append(PrimedVars,Out,PredState), |
| 908 | | % format(' ** LS for ~w: ~w~n',[OpName,OpLocalState]), |
| 909 | | % format(' ** PredState for ~w: ~w~n',[OpName,PredState]), |
| 910 | | % print(predicate(Predicate)),nl, |
| 911 | | b_test_boolean_expression(Predicate,OpLocalState,PredState,WF), |
| 912 | | % print(grounding_waitflags),nl, |
| 913 | ? | ground_wait_flags(WF), |
| 914 | | normalise_store(OutVariablesState,NormalisedOutVariablesState). |
| 915 | | |
| 916 | | gen_bind(TID,Val,bind(ID,Val)) :- def_get_texpr_id(TID,ID). |
| 917 | | |
| 918 | | :- use_module(probsrc(bmachine),[b_get_machine_operation_for_animation/4]). |
| 919 | | % generate an environment where operation parameters and results are stored: |
| 920 | | setup_local_state_for_operation(OpName,ParamValues,ResultValues,LocalState) :- |
| 921 | | b_get_machine_operation_for_animation(OpName,Results,Parameters,_Body), |
| 922 | | maplist(gen_bind,Parameters,ParamValues,ParamBindings), |
| 923 | | maplist(gen_bind,Results,ResultValues,ResultBindings), |
| 924 | | append(ResultBindings,ParamBindings,LocalState). |
| 925 | | |
| 926 | | |
| 927 | | :- use_module(btypechecker,[prime_atom0/2]). |
| 928 | | create_primed_binding(bind(ID,Val),bind(PID,Val)) :- prime_atom0(ID,PID). |
| 929 | | |
| 930 | | |
| 931 | | % ------------------------------------ |
| 932 | | |
| 933 | | % Determinacy Check for Constants |
| 934 | | % check if the values of the constants are forced to have one value |
| 935 | | |
| 936 | | :- use_module(bsyntaxtree, [safe_create_texpr/3, get_texpr_id/2]). |
| 937 | | cbc_constants_det_check(UseConstantsFromStateID) :- |
| 938 | | cbc_constants_det_check(UseConstantsFromStateID,[print_explanation],_,_,_,_), |
| 939 | | fail. |
| 940 | | cbc_constants_det_check(_). |
| 941 | | |
| 942 | | :- use_module(state_space,[is_concrete_constants_state_id/1]). |
| 943 | | tcltk_cbc_constants_det_check(list([list(['CONSTANT','FORCED', 'VALUE', 'Explanation', 'Source']) | Res ])) :- |
| 944 | | is_concrete_constants_state_id(StateID),!, |
| 945 | | set_unicode_mode, |
| 946 | | call_cleanup( |
| 947 | | findall(list([ID,FS,VS,CoreStr,CoreSrc]), |
| 948 | | (cbc_constants_det_check(StateID,[],ConstantID,Forced,ValStr,CorePred), |
| 949 | | get_core_str(Nr,CorePred,CoreStr,CoreSrc), |
| 950 | | (Nr=1 -> ID=ConstantID, VS = ValStr, FS = Forced ; ID = '', VS = '', FS = '')), |
| 951 | | Res), |
| 952 | | unset_unicode_mode). |
| 953 | | tcltk_cbc_constants_det_check(list([list(['SETUP_CONSTANTS first'])])) :- b_machine_has_constants,!. |
| 954 | | tcltk_cbc_constants_det_check(list([list(['MODEL HAS NO CONSTANTS'])])). |
| 955 | | |
| 956 | | :- use_module(error_manager,[get_tk_table_position_info/2]). |
| 957 | | :- use_module(bsyntaxtree,[conjunction_to_list/2, get_texpr_expr/2,get_texpr_id/2]). |
| 958 | | get_core_str(Nr,CorePred,TS,Src) :- |
| 959 | | (conjunction_to_list(CorePred,CL), CL \= [] -> true ; CL = [CorePred]), |
| 960 | | nth1(Nr,CL,P), |
| 961 | | get_preference(translation_limit_for_table_commands,Limit), |
| 962 | | translate_bexpression_with_limit(P,Limit,TS), |
| 963 | | get_tk_table_position_info(P,Src). |
| 964 | | |
| 965 | | :- use_module(bsyntaxtree,[predicate_components/2]). |
| 966 | | cbc_constants_det_check(UseConstantsFromStateID,Options,ConstantID,Forced,ValStr,CorePred) :- |
| 967 | | % we need one solution to start from (TODO: we could look at all set_constant solutions found) |
| 968 | | get_constants_state_for_id(UseConstantsFromStateID,UsedCState), |
| 969 | | format('~nChecking if value of constants in state ~w are forced~n',[UseConstantsFromStateID]), |
| 970 | | |
| 971 | | b_get_properties_from_machine(Properties), |
| 972 | | b_get_machine_constants(Constants), |
| 973 | | predicate_components(Properties,Components), |
| 974 | | nth1(Nr,Components,component(ComponentPred,CompIds)), % select component via backtracking |
| 975 | | CompIds \= [], |
| 976 | | format('Checking component ~w over identifiers ~w~n',[Nr,CompIds]), |
| 977 | | |
| 978 | | empty_state(EmptyState), |
| 979 | | set_up_typed_localstate(Constants,_FreshVars1,TypedVals1,EmptyState,State1,positive), |
| 980 | | init_wait_flags_with_call_stack(WF,[prob_command_context(cbc_constants_det_check,unknown)]), |
| 981 | | empty_avl(Ai), |
| 982 | | b_test_boolean_expression(ComponentPred,[],State1,WF,Ai,A2), % A2 is used below for after state |
| 983 | | b_tighter_enumerate_all_values(TypedVals1,WF), |
| 984 | | |
| 985 | | member(ConstantID,CompIds), |
| 986 | | member(bind(ConstantID,CVal),UsedCState), |
| 987 | | nl, |
| 988 | | member(TID,Constants), def_get_texpr_id(TID,ConstantID), |
| 989 | | get_texpr_type(TID,Type), |
| 990 | | safe_create_texpr(not_equal(TID,b(value(CVal),Type,[])),pred,NotEqual), |
| 991 | | (b_test_boolean_expression(NotEqual,[],State1,WF,A2,_), |
| 992 | | ground_wait_flags(WF) |
| 993 | | -> format_with_colour_nl(user_output,[green],'--- CONSTANT ~w can take on another value',[ConstantID]), |
| 994 | | Forced='FALSE', ValStr = '', |
| 995 | | CorePred = b(truth,pred,[]) |
| 996 | | ; translate_bvalue_with_limit(CVal,50,ValStr), |
| 997 | | format_with_colour_nl(user_output,[blue],'*** CONSTANT ~w has the forced value ~w',[ConstantID,ValStr]), |
| 998 | | Forced='TRUE', |
| 999 | | (get_preference(cbc_provide_explanations,false) |
| 1000 | | -> CorePred = b(unknown_truth_value(no_explanation_computed),pred,[]) |
| 1001 | | ; write('Generating explanation '), |
| 1002 | | unsat_cores:unsat_chr_core_with_fixed_conjuncts_auto_time_limit(ComponentPred,NotEqual,1000,CorePred) |
| 1003 | | -> (member(print_explanation,Options) -> translate:nested_print_bexpr_as_classicalb(CorePred) ; true) |
| 1004 | | ; CorePred = b(unknown_truth_value(fail),pred,[]) |
| 1005 | | ) |
| 1006 | | ). |
| 1007 | | |
| 1008 | | |
| 1009 | | |