b_state_model_check

add_binding(List,V) :- var(List), !, List = [bind(V,_)|_].

add_binding([],V) :- add_internal_error(add_binding,'Variable does not appear in store: ',V,unknown).

add_binding([bind(VV,_)|T],V) :-
    (V==VV -> true /* ok, found the variable */
    ; add_binding(T,V)).

b_check_valid_state(State) :-
    (b_valid_state(State) -> true
    ; print_error('Invalid State:'),
    print_error(State)
).

b_check_variable_types([],_).

b_check_variable_types([Var|VT],State) :-
    def_get_texpr_id(Var,VarID), get_texpr_type(Var,Type),
    (store:lookup_value_for_existing_id(VarID,State,Val),
    Val\==fail
    -> (kernel_objects:basic_type(Val,Type)
    -> true
    ; print_error('Type Error ! Variable,Value,Type: '),print_error(VarID),
    print_error(Val),print_error(Type)
    ),
    b_check_variable_types(VT,State)
    ; add_error(b_check_variable_types,'Variable not defined in state: ', VarID),
    add_error(b_check_variable_types,'Be sure that INITIALISATION initialises the variable: ', VarID),
    print_error(State)
).

b_find_dynamic_assertion_violation(NormalisedState) :-
    get_unproven_assertion(UPA),
    create_negation(UPA,NegUPA),
    b_set_up_valid_state_with_pred(NormalisedState,NegUPA,true,none).

b_find_redundant_invariant(RedundantInv,State,Redundant,EnumWarning,ErrOcc) :-
    b_get_invariant_from_machine(Invariant),
    conjunction_to_list(Invariant,InvList),
    select(RedundantInv,InvList,RestInvariantList),
    (silent_mode(on) -> true ;
    print('CHECKING REDUNDANCY: '),translate:print_bexpr(RedundantInv),nl),
    create_negation(RedundantInv,NegRed),
    conjunct_predicates(RestInvariantList,AdaptedInvariant),
    %translate:print_bexpr(AdaptedInvariant),nl,
    enter_new_error_scope(ScopeID,b_find_redundant_invariant),
    ( time_out_with_factor_call(predicate_satisfiable_relevant_ids(NegRed,AdaptedInvariant,State),5,
    TO=time_out)
    -> (TO==time_out -> Redundant=time_out ; Redundant=useful)
    ; Redundant = redundant),
    (critical_enumeration_warning_occured_in_error_scope -> EnumWarning=true
    ; EnumWarning=false),
    exit_error_scope(ScopeID,ErrOcc,b_find_redundant_invariant),
    printsilent('RESULT: '),printsilent(Redundant),nls.

b_set_up_valid_state(State) :- b_set_up_valid_state_with_pred(State,b(truth,pred,[]),true,none).

b_set_up_valid_state_with_pred(NormalisedState,Pred) :-
    b_set_up_valid_state_with_pred(NormalisedState,Pred,true,none).

b_set_up_valid_state_with_pred(NormalisedState,Pred,UseInvariant,UseConstantsFromStateID) :-
    %enter_new_error_scope(ScopeID,cbc_find_state),
    predicate_satisfiable_all_ids(Pred,State,UseInvariant,UseConstantsFromStateID),
    normalise_store(State,NormalisedState).

b_valid_state(State) :-
    b_get_machine_variables(Variables),
    b_check_variable_types(Variables,State).

cbc_check('INV_NO_RED',
    'INV_NO_RED: Find invariants which are redundant',
    Call,Res,Ok) :- Call = (tcltk_find_redundant_invariants(Res,Ok)).

cbc_check('INV_AXM_SAT',
    'INV_AXM_SAT: Check if there exists a state that satisfies the INVARIANT and the PROPERTIES (AXIOMS)',
    Call,Res,Ok) :-
    Call = (b_set_up_valid_state(State) -> Ok=true,translate_bstate(State,Res) ; Ok=false, Res='NO_VALID_STATE_FOUND').

cbc_check('DLK',
    'DLK: Check that INVARIANT does not allow a deadlocking state',
    Call,Res,Ok) :-
    Call = (cbc_deadlock_freedom_check(State) -> Ok=false,translate_bstate(State,Res) ; Ok=true, Res='NO_DEADLOCK_FOUND').

cbc_check('THM_STATIC',
    'THM_STATIC: Check that static ASSERTIONS (THEOREMS) follow from PROPERTIES (AXIOMS)',
    Call,TclRes,Ok) :-
    Call = (cbc_static_assertions_check(Res),translate_result(Res,Ok),functor(Res,TclRes,_)).

cbc_check(INVO,
    Label,
    Call,Res,Ok) :-
    b_top_level_operation(OpName),
    ajoin(['INV/',OpName],INVO),
    ajoin(['INV/',OpName,': Check that ',OpName,' preserves INVARIANT'],Label),
    Call = (state_model_check(OpName,invariant,_State,_Operation,NewState)
    -> Ok=false,translate_bstate(NewState,Res) ; Ok=true, Res='NO_INVARIANT_violation_found').

cbc_constants_det_check(UseConstantsFromStateID) :-
    cbc_constants_det_check(UseConstantsFromStateID,[print_explanation],_,_,_,_),
    fail.

cbc_constants_det_check(_).

cbc_constants_det_check(UseConstantsFromStateID,Options,ConstantID,Forced,ValStr,CorePred) :-
    % we need one solution to start from (TODO: we could look at all set_constant solutions found)
    get_constants_state_for_id(UseConstantsFromStateID,UsedCState),
    format('~nChecking if value of constants in state ~w are forced~n',[UseConstantsFromStateID]),
   
    b_get_properties_from_machine(Properties),
    b_get_machine_constants(Constants),
    predicate_components(Properties,Components),
    nth1(Nr,Components,component(ComponentPred,CompIds)), % select component via backtracking
    CompIds \= [],
    format('Checking component ~w over identifiers ~w~n',[Nr,CompIds]),
   
    empty_state(EmptyState),
    set_up_typed_localstate(Constants,_FreshVars1,TypedVals1,EmptyState,State1,positive),
    init_wait_flags_with_call_stack(WF,[prob_command_context(cbc_constants_det_check,unknown)]),
    empty_avl(Ai),
    b_test_boolean_expression(ComponentPred,[],State1,WF,Ai,A2), % A2 is used below for after state
    b_tighter_enumerate_all_values(TypedVals1,WF),
   
    member(ConstantID,CompIds),
    member(bind(ConstantID,CVal),UsedCState),
    nl,
    member(TID,Constants), def_get_texpr_id(TID,ConstantID),
    get_texpr_type(TID,Type),
    safe_create_texpr(not_equal(TID,b(value(CVal),Type,[])),pred,NotEqual),
    (b_test_boolean_expression(NotEqual,[],State1,WF,A2,_),
    ground_wait_flags(WF)
    -> format_with_colour_nl(user_output,[green],'--- CONSTANT ~w can take on another value',[ConstantID]),
    Forced='FALSE', ValStr = '',
    CorePred = b(truth,pred,[])
    ; translate_bvalue_with_limit(CVal,50,ValStr),
    format_with_colour_nl(user_output,[blue],'*** CONSTANT ~w has the forced value ~w',[ConstantID,ValStr]),
    Forced='TRUE',
    (get_preference(cbc_provide_explanations,false)
    -> CorePred = b(unknown_truth_value(no_explanation_computed),pred,[])
    ; write('Generating explanation '),
    unsat_cores:unsat_chr_core_with_fixed_conjuncts_auto_time_limit(ComponentPred,NotEqual,1000,CorePred)
    -> (member(print_explanation,Options) -> translate:nested_print_bexpr_as_classicalb(CorePred) ; true)
    ; CorePred = b(unknown_truth_value(fail),pred,[])
)
).

cbc_deadlock_freedom_check(State) :-
    create_texpr(truth,pred,[],True), Filter=0,
    cbc_deadlock_freedom_check(State,True,Filter).

cbc_deadlock_freedom_check(State,Goal,Filter) :-
    debug_println(19,cbc_deadlock_freedom_check(State,Filter)),flush_output,
    ( is_truth(Goal) ->
    get_all_guards_false_pred(Target)
    ;
    print('Adding additional goal predicate: '),nl,
    print_bexpr(Goal),nl,
    ( Filter=1 ->
    get_all_guards_false_pred(AllGFalse,Goal)
    ;
    get_all_guards_false_pred(AllGFalse)),
    conjunct_predicates([AllGFalse,Goal],Target)
    ),!,flush_output,
    statistics(runtime,[Start,_]),
    statistics(walltime,[WStart,_]),
    cbc_deadlock_freedom_check2(Target,RState,Start,WStart,false,TO), % TO DO: control SkipIrrelevantComponents by preference or GUI
    (TO==time_out -> State=time_out ; State=RState).

cbc_deadlock_freedom_check2(Target,NormalisedState,Start,WStart,SkipIrrelevantComponents,TO) :-
    get_texpr_expr(Target,T), T \= falsity,
    b_get_properties_from_machine(Properties),
    b_get_invariant_from_machine(Invariant),
    conjunct_predicates([Properties,Invariant,Target],Pred1),
    b_get_machine_variables(Variables),
    b_get_machine_constants(Constants), append(Constants,Variables,CV),
   
    apply_kodkod_or_other_optimisations(CV,Pred1,Pred),
    %predicate_level_optimizations(Pred2,Pred), % detect set partitions, etc..., now done inside b_interpreter_components
   
    set_up_typed_localstate_for_pred(CV,Pred,TypedVals,State),
    b_interpreter_components:reset_component_info(false),
    (debug_mode(on) -> translate:nested_print_bexpr_as_classicalb(Pred) ; true),
    %%visualize_graph:print_predicate_dependency_as_graph_for_dot(Pred,'~/Desktop/pdg.dot'),
    (SkipIrrelevantComponents==true
    -> predicate_identifiers(Target,TargetIds) % Warning: can skip over obvious inconsistencies TRUE:BOOL
    ; TargetIds=all),
    println_silent(target(TargetIds)),
    b_global_sets:static_symmetry_reduction_for_global_sets(State),
    time_out_with_factor_call(
    b_interpreter_components:b_trace_test_components(Pred,State,TypedVals,TargetIds),
    10, (nl,TO=time_out)),
    statistics(runtime,[Stop,_]), Time is Stop - Start,
    statistics(walltime,[WStop,_]), WTime is WStop - WStart,
    (TO==time_out -> println_silent(time_out_during_deadlock_checking(Time)), NormalisedState=State
    ; TO=no_time_out, println_silent(deadlock_counter_example_found(Time,WTime)),
    normalise_store(State,NormalisedState)
).

cbc_deadlock_freedom_check2(Target,_State,Start,WStart,_,no_time_out) :-
    (get_texpr_expr(Target,falsity) -> println_silent('Disjunction of guards obviously true') ; true),
    statistics(runtime,[Stop,_]), Time is Stop - Start,
    statistics(walltime,[WStop,_]), WTime is WStop - WStart,
    println_silent(no_deadlock_counter_example_found(Time,WTime)), %print_silent
    fail.

cbc_dynamic_assertions_check(Result) :-
    enter_new_error_scope(ScopeID,cbc_dynamic_assertions_check),
    start_ms_timer(Timer),
    ( time_out_with_factor_call(b_find_dynamic_assertion_violation(State),10,TO=time_out) ->
    (TO==time_out -> Result = time_out ; Result = counterexample_found(State))
    ; critical_enumeration_warning_occured_in_error_scope -> Result = no_counterexample_found
    ; Result = no_counterexample_exists
    ),
    (debug_mode(on) -> print('cbc_dynamic_assertions_check: '),stop_ms_timer(Timer) ; true),
    exit_error_scope(ScopeID,_ErrOcc,cbc_dynamic_assertions_check).

cbc_find_redundant_invariants(RedundantInvs,Timeout_occured) :-
    retractall(timeout_occured),
    findall(RI,
    (b_find_redundant_invariant(RedInv,_,R,EnumWarning,ErrOcc),
    translate:translate_bexpression(RedInv,InvString),
    generate_explanation(R,EnumWarning,ErrOcc,InvString,RI),
    (R==time_out -> assertz(timeout_occured) ; true)
    ),
    RedundantInvs),
    (timeout_occured -> Timeout_occured = true ; Timeout_occured=false).

cbc_model_check(OpName,InvOrAssertion,BeforeState,Operation,NewState) :-
    (nonvar(OpName),
    \+ b_is_operation_name(OpName), \+ b_is_initialisation_name(OpName)
    -> add_error(constraint_based_check,'Operation does not exist: ',OpName), fail
    ; true
    ),
    debug_println(9,operation_name(OpName)),
    b_get_properties_from_machine(Properties),
    b_get_invariant_from_machine(Invariant),
    b_get_machine_variables(Variables),
    b_get_machine_constants(Constants),
    % print_message(extracted_invariant(Variables,Invariant)),
   
    empty_state(EmptyState),
    set_up_typed_localstate(Constants,_FreshVars1,TypedVals1,EmptyState,State1,positive),
    b_global_sets:static_symmetry_reduction_for_global_sets(State1),
    (b_is_initialisation_name(OpName)
    -> State=State1,
    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
    TypedVals=TypedVals1
    ; BeforeState=State,
    set_up_typed_localstate(Variables,_FreshVars2,TypedVals2,State1,State,positive),
    append(TypedVals1,TypedVals2,TypedVals)
    ),
    init_wait_flags_with_call_stack(WF,[prob_command_context(cbc_model_check(OpName),unknown)]),
   
    % print_message(' set up start state:'), print_message(State),
    % translate:print_bexpr(Properties),
    empty_avl(Ai),
    b_test_boolean_expression(Properties,[],State,WF,Ai,A2), % A2 is used below for after state
    % print_message(' set up properties for constants'),
   
    get_target_pred(InvOrAssertion,OpName, Invariant, PriorPred,TargetPred),
   
    %print('Prior: '),translate:print_bexpr(PriorPred),nl,
    b_test_boolean_expression(PriorPred,[],State,WF,A2,_A3),
    % print_message(' set up invariant for start state'),
   
    set_up_transition_or_init(OpName,Operation,State1,State,NewState,_TransInfo,WF),
    debug_print(9,' finished setting up target state for operation:'), debug_println(9,OpName),
    %print_message(' target state:'), print_message(NewState),
    % 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
   
    predicate_level_optimizations(TargetPred,OptTargetPred),
   
    (debug_mode(on) -> translate:print_bexpr(OptTargetPred),nl ; true),
    b_test_boolean_expression(OptTargetPred,[],NewState,WF,A2,_Ao), % not A3 but A2; as different State
    debug_println(9,' finished setting up invariant of proven invariants and negation of invariant for target state'),
   
    % print(enum(TypedVals)),nl,
    b_tighter_enumerate_all_values(TypedVals,WF),
   
    %(debug_mode(on) -> ground_wait_flag0(WF),portray_waitflags(WF),print_bt_message(grounding_wait_flags) ; true),
    ground_wait_flags(WF).

cbc_static_assertions_check(Result) :- cbc_static_assertions_check(Result,[]).

cbc_static_assertions_check(Result,Options) :-
    get_cbc_assertions_predicate_to_solve(Options, Constants, TotalPredicate,true,_),
    enter_new_error_scope(ScopeID,cbc_static_assertions_check),
    start_ms_timer(Timer),
    (member(observe_state,Options) -> external_functions:observe_state(State) ; true),
    ( time_out_with_factor_call(cbc_static_assertions_check2(State,Constants, TotalPredicate),10,TO=time_out)
    % counter example was found or time out reached:
    -> (TO==time_out -> Result = time_out ; Result = counterexample_found(State))
    % cbc_static_assertions check did not find a counter exmaple:
    ; critical_enumeration_warning_occured_in_error_scope -> Result = no_counterexample_found
    ; get_elapsed_walltime(Timer,WTime),
    cbc_static_assertions_contradiction_check(Constants,TotalPredicate,Result,Options,WTime)
    ),
    (debug_mode(on) -> print('cbc_static_assertions_check: '),stop_ms_timer(Timer) ; true),
    exit_error_scope(ScopeID,_ErrOcc,cbc_static_assertions_check).

cbc_static_assertions_check2(concrete_constants(NormalisedState),Constants, TotalPredicate) :-
    solve_cbc_predicate_over_constants(Constants,TotalPredicate,NormalisedState).

cbc_static_assertions_contradiction_check(Constants,TotalPredicate,Result,Options,_) :-
    member(contradiction_check,Options),
    println_silent('Looking for contradiction in hypothesis'),
    get_cbc_assertions_predicate_to_solve(Options, Constants, TotalPredicate2,false,Goal),
    start_ms_timer(Timer),
    (time_out_with_factor_call(cbc_static_assertions_check2(_,Constants, TotalPredicate2),10,TO=time_out)
    -> debug_println(no_contradiction(TO)),fail ; true),
    get_elapsed_walltime(Timer,WTime),
    (critical_enumeration_warning_occured_in_error_scope
    -> print(no_contradiction(enumeration_warning)),nl,fail ; true),
    !,
    println_silent('*** CONTRADICTION IN HYPOTHESIS FOUND !'),
    translate:translate_bexpression_with_limit(Goal,GS),
    add_warning(contradiction_in_hypotheses,
    'Prover double check result: Contradiction in hypotheses (or Bug) detected for goal: ',GS),
    compute_unsat_core_if_requested(Options,TotalPredicate2,WTime),
    Result = no_counterexample_exists(Constants,TotalPredicate,[contradiction_in_hypotheses]).

cbc_static_assertions_contradiction_check(Constants,TotalPredicate,Result,Options,WTime) :-
    compute_unsat_core_if_requested(Options,TotalPredicate,WTime),
    Result = no_counterexample_exists(Constants,TotalPredicate,[]).

compute_unsat_core_if_requested(Options,Predicate,WTime) :-
    member(unsat_core,Options),!,
    format('Computing UNSAT CORE (~w ms to find initial contradiction)~n',[WTime]),
    UCOptions=[],
    unsat_core_list_with_time_limit(Predicate,WTime,UCOptions,no_solution_found,CorePredicates),
    nl,print('UNSAT CORE: '),nl,
    print('--------'),nl,
    translate:nested_print_bexpr_as_classicalb(CorePredicates),
    print('--------'),nl.

compute_unsat_core_if_requested(_,_,_).

conjoin(b(truth,_,_),B,_,R) :- !,R=B.

conjoin(b(falsity,_,_),_B,_,R) :- !,R=b(falsity,pred,[]).

conjoin(A,b(truth,_,_),_,R) :- !,R=A.

conjoin(_A,b(falsity,_,_),_,R) :- !,R=b(falsity,pred,[]).

conjoin(A,B,Info,b(conjunct(A,B),pred,Info)).

conjunct_and_sort_smt_predicates(List,Result) :-
    debug_println(9,'Counting basic predicates'),
    empty_avl(Ai), count(List,2,Ai,Ao),
    % portray_avl(Ao),nl,
    sort_smt_predicates(List,Ao,SList),
    %nl,print(sorted(SList)),nl,
    conjunct_smt_predicates(SList,Result) , debug_println(9,finished).

conjunct_smt_predicates([],b(truth,pred,[])).

conjunct_smt_predicates([P|T],Res) :- conjunct_smt_predicates(T,TRes),
    extract_info(P,TRes,Info), % extract e.g., wd condition info
    conjoin(P,TRes,[try_smt|Info],Res). % try_smt currently no longer useful ?

conjunction_to_count_list(C,AVL,List) :- is_a_conjunct(C,LHS,RHS),!,
    conjunction_to_count_list(LHS,AVL,L1),
    conjunction_to_count_list(RHS,AVL,R1),
    append(L1,R1,List). % TO DO: improve, use Difference Lists

conjunction_to_count_list(b(Pred,pred,Info),AVL,[count(Count,b(Pred,pred,Info))]) :- smt_predicate(Pred),!,
    norm_pred(Pred,NX),
    (avl_fetch(NX,AVL,Count) -> true ; Count=0).

conjunction_to_count_list(P,_AVL,[count(0,P)]).

construct_sequent([IMPLICATION],HYP,[RHS]) :-
    is_an_implication(IMPLICATION,HYP,RHS),!.

construct_sequent([b(negation(HYP),pred,I)],HYP,[RHS]) :- % relevant for test 1451
    member(was(implication),I),
    !,
    RHS=b(falsity,pred,[]).

construct_sequent(UPAssertions,b(truth,pred,[]),UPAssertions).

copy_binding_skel(bind(Id,_),bind(Id,_)).

copy_unmodified_variables(Variables,OpName,OldStore,NewStore) :-
    ( get_operation_info(OpName,SubstitutionInfo) ->
    ( memberchk(modifies(ModIDs),SubstitutionInfo) ->
    get_texpr_ids(Variables,Ids),
    exclude(is_modified_var(ModIDs),Ids,UnmodifiedIds),
    maplist(copy_var(OldStore,NewStore),UnmodifiedIds)
    ;
    add_internal_error('Operation/Event has no modifies info: ',
    copy_unmodified_variables(Variables,OpName,OldStore,NewStore))
    % assume that all variables modified: no copy_var calls
    )
    ; OpName = 'INITIALISATION' -> true % nothing to copy
    ; OpName = 'SETUP_CONSTANTS' -> true % nothing to copy
    ;
    add_internal_error('Unknown Operation/Event:', copy_unmodified_variables(Variables,OpName,OldStore,NewStore)),
    fail
).

copy_var(OldStore,NewStore,Id) :-
    lookup_value(Id,OldStore,V),lookup_value(Id,NewStore,VNew),
    equal_object(V,VNew).

count(b(Pred,pred,_Info),Rel,Ai,Ao) :- !,count2(Pred,Rel,Ai,Ao).

count([],_,Ai,Ao) :- !,Ao=Ai.

count([H|T],Rel,Ai,Ao) :- !,count(H,Rel,Ai,Aii), count(T,Rel,Aii,Ao).

count(R,_,_,_) :- add_error_fail(count,'Illegal argument to count: ',R).

count2(negation(Pred),Rel,Ai,Ao) :- !, count(Pred,Rel,Ai,Ao).

count2(conjunct(A,B),Rel,Ai,Ao) :- !, count(A,Rel,Ai,Aii), count(B,Rel,Aii,Ao).

count2(Pred,Rel,Ai,Ao) :- disjunctive_pred(Pred,A,B),!,
    (Rel>1
    -> R1 is Rel-1, count(A,R1,Ai,Aii), count(B,R1,Aii,Ao)
    ; Ai=Ao).

count2(Pred,Rel,Ai,Ao) :- smt_predicate(Pred),!, norm_pred(Pred,NP),
    (avl_fetch(NP,Ai,C1) -> Count is C1+Rel ; Count = Rel),
    avl_store(NP,Ai,Count,Ao).

count2(_Pred,_Rel,A,A).

create_primed_binding(bind(ID,Val),bind(PID,Val)) :- prime_atom0(ID,PID).

create_target_state(Variables,Values,ConstantsState,NewState,WF) :-
    set_up_typed_localstate(Variables,Values,TypedVals,ConstantsState,NewState,positive),
    b_tighter_enumerate_all_values(TypedVals,WF).

disjunctive_pred(disjunct(A,B),A,B).

disjunctive_pred(implication(A,B),A,B).

disjunctive_pred(equivalence(A,B),A,B).

event_b_transition(OpName,Operation,State,NewState,TransInfo,WF) :-
    b_get_machine_operation(OpName,[],Parameters,TEvent,eventb_operation(ChangeSet,Values,Operation),_),
    copy_variable_store(State,ChangeSet,_,NewState),
    b_event_constraints(TEvent,Parameters,Values,State,NewState,TransInfo,WF).

execute_operation_by_predicate_in_state(InVarsState,OpName,Predicate,Operation,OutVariablesState) :-
    execute_operation_by_predicate_in_state_with_pos(InVarsState,OpName,Predicate,Operation,OutVariablesState,unknown).

execute_operation_by_predicate_in_state2(ConstantsState,InVariablesState,OpName,Predicate,
    Operation,NormalisedOutVariablesState,PositionInfo) :-
    b_get_machine_variables(Variables),
    maplist(copy_binding_skel,InVariablesState,OutVariablesState),
    copy_unmodified_variables(Variables,OpName,InVariablesState,OutVariablesState),
    % format(' ** Copied for ~w: ~w~n',[OpName,OutVariablesState]),
    init_wait_flags_with_call_stack(WF,[operation_call(OpName,ParamValues,PositionInfo)]),
    add_prob_deferred_set_elements_to_store(ConstantsState,ConstantsState1,visible),
    append(ConstantsState1,InVariablesState,In),
    append(ConstantsState1,OutVariablesState,Out),
    % for Event-B we have to add b_machine_temp_predicate
    % b_execute_operation_with_parameters(Name,LocalState,InState,Results,Parameters,OutState,ParamValues,ResultValues,Path,Info,WF,OR)
    b_execute_top_level_operation_wf(OpName,Operation,ParamValues,ResultValues,In,Out,_TransInfo,WF),
    % format(' ** Exec for ~w (~w) --> ~w: ~w~n',[OpName,ParamValues,ResultValues,OutVariablesState]),
    setup_local_state_for_operation(OpName,ParamValues,ResultValues,OpLocalState),
    maplist(create_primed_binding,InVariablesState,PrimedVars),
    append(PrimedVars,Out,PredState),
    % format(' ** LS for ~w: ~w~n',[OpName,OpLocalState]),
    % format(' ** PredState for ~w: ~w~n',[OpName,PredState]),
    % print(predicate(Predicate)),nl,
    b_test_boolean_expression(Predicate,OpLocalState,PredState,WF),
    % print(grounding_waitflags),nl,
    ground_wait_flags(WF),
    normalise_store(OutVariablesState,NormalisedOutVariablesState).

execute_operation_by_predicate_in_state_with_pos(const_and_vars(ID,InVariablesState),OpName,Predicate,Operation,
    const_and_vars(ID,OutVariablesState),Pos) :- !,
    visited_expression(ID,concrete_constants(ConstantsState)),
    execute_operation_by_predicate_in_state2(ConstantsState,InVariablesState,OpName,Predicate,
    Operation,OutVariablesState,Pos).

execute_operation_by_predicate_in_state_with_pos(InVariablesState,OpName,Predicate,Operation,OutVariablesState,Pos) :-
    execute_operation_by_predicate_in_state2([],InVariablesState,OpName,Predicate,Operation,OutVariablesState,Pos).

gen_bind(TID,Val,bind(ID,Val)) :- def_get_texpr_id(TID,ID).

generate_explanation(R,EnumWarning,ErrOcc,InvString,Res) :-
    (EnumWarning=true -> L1=[' /* ENUM WARNING */ '|L2] ; L1=L2),
    (ErrOcc=true -> L2=[' /* REQUIRED FOR WELL-DEFINEDNESS */ '] ; L2=[]),
    (R=redundant -> ajoin([InvString|L1],Res)
    ; R=useful -> EnumWarning=true, ajoin(['ENUMERATION WARNING (POSSIBLY USEFUL): ',InvString|L2],Res)
    ; R=time_out -> ajoin(['TIME OUT (POSSIBLY USEFUL): ',InvString|L1],Res)
).

get_all_guards_false_pred(AllGuardsFalsePred) :-
    findall(NegGuard,
    (b_is_operation_name(OpName),
    get_negated_guard(OpName,_,NegGuard)), ListOfNegGuards),
    conjunct_and_sort_smt_predicates(ListOfNegGuards,AllGuardsFalsePred).

get_all_guards_false_pred(AllGuardsFalsePred,FilterPred) :-
    findall(NegGuard,
    (b_is_operation_name(OpName),
    get_negated_guard(OpName,Guard,NegGuard),
    conjunct_predicates([Guard,FilterPred],FGuard),
    nls,printsilent('---> CHECKING IF GUARD SATISFIABLE: '), printsilent(OpName),nls,
    predicate_satisfiable(FGuard) % if Guard not satisfiable given FilterPred: remove it
    ), ListOfNegGuards),
    conjunct_and_sort_smt_predicates(ListOfNegGuards,AllGuardsFalsePred).

get_cbc_assertions_predicate_to_solve(Options, Constants, TotalPredicate,NegateGoal,NegGoal) :-
    get_cbc_assertions_sequent(Options, Constants, Properties, GoalToProve),
    conjunct_predicates(GoalToProve,GoalC),
    (debug_mode(on) -> print('Trying to prove goal: '),nl,translate:nested_print_bexpr_as_classicalb(GoalC) ; true),
    (NegateGoal=true -> create_negation(GoalC,NegGoal) ; NegGoal=GoalC),
    %% print('Using Hypotheses: '),nl,translate:nested_print_bexpr_as_classicalb(Properties),
    conjunct_predicates([NegGoal,Properties],TotalPredicate).

get_cbc_assertions_sequent(Options, Constants, Properties, GoalToProve) :-
    b_get_machine_constants(AllConstants),
    (member(specific(Label),Options) -> WhichAss=specific(Label)
    ; member(main_assertions,Options) -> WhichAss=main
    ; WhichAss=all),
    b_get_assertions(WhichAss,static,Assertions),
    (get_preference(use_po,true), nonmember(tautology_check,Options)
    -> exclude(bmachine:is_discharged_assertion,Assertions,UnProvenAssertions)
    ; UnProvenAssertions = Assertions
    ),
    (member(tautology_check,Options)
    % used for ProB as an Atelier-B disprover/prover: the ASSERTIONS are an implication
    -> find_identifier_uses_l(UnProvenAssertions,[],Ids),
    include(id_mem(Ids),AllConstants,Constants), % only include constants used in tautology
    construct_sequent(UnProvenAssertions,Properties,GoalToProve)
    ; % Sequent: Properties |- UnProvenAssertions
    b_get_properties_from_machine(Properties),
    Constants = AllConstants,
    GoalToProve = UnProvenAssertions
).

get_core_str(Nr,CorePred,TS,Src) :-
    (conjunction_to_list(CorePred,CL), CL \= [] -> true ; CL = [CorePred]),
    nth1(Nr,CL,P),
    get_preference(translation_limit_for_table_commands,Limit),
    translate_bexpression_with_limit(P,Limit,TS),
    get_tk_table_position_info(P,Src).

get_guard(OpName,Guard) :- get_guard_and_precision(OpName,Guard,_).

get_guard_and_precision(OpName,Guard,Precise) :-
    get_simplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,Precise),
    % Precise is either precise or imprecise
    % TO DO: partition; avoid lifting becomes_such_that conditions
    % (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok)
    construct_optimized_exists(Parameters,EnablingCondition,Guard).

get_negated_guard(OpName,Guard,NegationOfGuard) :- get_negated_guard(OpName,Guard,NegationOfGuard,_Precise).

get_negated_guard(OpName,Guard,NegationOfGuard,Precise) :-
    get_guard_and_precision(OpName,Guard,Precise),
    SGuard=Guard,
    %simplify_guard(Guard,SGuard), %% comment in to remove complicated parts
    create_negation(SGuard,NegationOfGuard). % we used to add try_smt Info; no longer relevant !?

get_target_pred(invariant,OpName, Invariant, PriorPred, TargetPred) :-
    (b_is_initialisation_name(OpName) -> create_texpr(truth,pred,[],PriorPred) ; PriorPred=Invariant),
    % Retrieve Information on proof status of the invariant
    (get_preference(use_po,true),get_proven_invariant(OpName,ProvenInvariant) -> true
    ; create_texpr(truth,pred,[],ProvenInvariant), println_silent(no_proven_invariant_info)
    ),
    (get_preference(use_po,false) -> UncheckedInvariant=Invariant
    ; b_specialized_invariant_for_op(OpName,UncheckedInvariant) -> true
    ; UncheckedInvariant=Invariant, println_silent(no_specialized_invariant_info_for_op(OpName))
    ),
    %print_message('proven invariant:'),print(proven(ProvenInvariant)),
    create_negation(UncheckedInvariant,NegUncheckedInvariant),
    % we conjoin the predicates so that predicate-level optimizations can be applied (TO DO: also allow Properties to be used)
    conjunct_predicates([ProvenInvariant,NegUncheckedInvariant],TargetPred).

get_target_pred(assertions,OpName, Invariant, PriorPred, TargetPred) :-
    % TODO: deal with initialisation for PriorPred
    get_unproven_assertion(UPA),
    create_negation(UPA,NegUPA),
    format('Trying to find Assertion Violation after ~w~n Target:',[OpName]),translate:print_bexpr(NegUPA),nl,nl,
    conjunct_predicates([Invariant,UPA],PriorPred),
    conjunct_predicates([Invariant,NegUPA],TargetPred).

get_unproven_assertion(UPA) :-
    b_get_assertions(main,dynamic,Assertions),
    (get_preference(use_po,true)
    -> exclude(bmachine:is_discharged_assertion,Assertions,UnProvenAssertions)
    ; UnProvenAssertions = Assertions
    ),
    conjunct_predicates(UnProvenAssertions,UPA).

get_unsorted_all_guards_false_pred(AllGuardsFalsePred) :-
    findall(NegGuard,
    (b_is_operation_name(OpName),
    get_negated_guard(OpName,_,NegGuard)), ListOfNegGuards),
    conjunct_predicates(ListOfNegGuards,AllGuardsFalsePred).

id_mem(IDList,TID) :- get_texpr_id(TID,ID), member(ID,IDList).

is_event_b_transition(OpName) :-
    b_get_machine_operation(OpName,[],_Parameters,_TEvent,eventb_operation(_ChangeSet,_Values,_Operation),_),!.

is_modified_var(ModIDs,Id) :-
    memberchk(Id,ModIDs).

norm_equal(b(identifier(ID),_,_),_B,Res) :- !,Res=ID.

norm_equal(A,B,Res) :- norm_pred(A,AA),norm_pred(B,BB),
    (AA==boolean_false -> AAA=boolean_true ; AAA=AA),
    (BB==boolean_false -> BBB=boolean_true ; BBB=BB),
    (BBB @< AAA -> Res = equal(AAA,BBB) ; Res= equal(BBB,AAA)).