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