| 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(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_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 |