cbc_refinement_checks

action_simulation(Axioms,Invariant,Properties,['Action Simulation:'|ResultsFlat],ViolationFound) :-
    % action simulation:
    % A & I & J & H & W & Tau => Q_i
    % find all candidates for evt/act/SIM proof obligations
    findall(RLEVENT,
    (b_get_machine_operation(_Name,_R,_P,Body,_OType,_),
    get_texpr_expr(Body,RLEVENT)),
    ListOfOperations),
    maplist(action_simulation(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound),
    merge_violation_found(SubViolationFound,ViolationFound),
    append(Results,ResultsFlat).

action_simulation(Axioms,Invariant,Properties,
    rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,VWit,PWit,_Unmod,AbsEvents),
    ResultsFlat,ViolationFound) :-
    % concrete before-after-predicate
    b_get_machine_variables(Vars),
    b_get_machine_constants(Consts),
    append(Vars,Consts,Both),
    before_after_predicate_list_conjunct_with_equalities(Actions,Both,Tau),
    maplist(extract_witness_predicate,VWit,VWitPreds),
    maplist(extract_witness_predicate,PWit,PWitPreds),
    append([Axioms,[Invariant,Properties,Guards,Tau],VWitPreds,PWitPreds],LHSPreds),
    conjunct_predicates(LHSPreds,LHS),
   
    % map over all abstract events
    maplist(action_simulation2(Name,LHS),AbsEvents,Results,SubViolationFound),
    merge_violation_found(SubViolationFound,ViolationFound),
    append(Results,ResultsFlat).

action_simulation2(Name,LHS,AbsEvent,Result,ViolationFound) :-
    get_texpr_expr(AbsEvent,rlevent(_AbsName,_Section,_Stat,_AbsParameters,_Guards,_Thm,Actions,_VWit,_PWit,_Unmod,_AbsEvents)),
    % map over all abstract actions
    maplist(action_simulation3(Name,LHS),Actions,Result,SubViolationFound),
    merge_violation_found(SubViolationFound,ViolationFound).

action_simulation3(Name,LHS,Action,Result,ViolationFound) :-
    modifies_concrete_var(Action), !,
    get_rodin_name(Action,ActionName),
   
    % before after predicate of abstract action, negate, solve
    b_get_machine_variables(AllVars),
    exclude(is_concrete_var,AllVars,AbstractVars),
    before_after_predicate_with_equalities(Action,AbstractVars,BAPred),
    create_negation(BAPred,NegatedBAPred),
    conjunct_predicates([NegatedBAPred,LHS],Pred),
   
    cbc_solve_predicate(Pred,State,Res),
    assign_violation_found(Res,ViolationFound,ResTxt),
   
    % result string
    ajoin([Name,'/',ActionName,'/SIM: ','Counter-Example found: ', ResTxt],Result),
    % print
    formatsilent(' * ~w~n',[Result]),
    (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl).

action_simulation3(_Name,_LHS,_Action,[],false).

all_abstract_parameters([],[]).

all_abstract_parameters([Event|FurtherEvents],ParametersOut) :-
    get_texpr_expr(Event,rlevent(_Name,_Section,_Stat,Parameters,_Guards,_Thm,_Actions,_VWit,_PWit,_Unmod,_AbsEvents)),
    all_abstract_parameters(FurtherEvents,FurtherParameters), append(Parameters,FurtherParameters,ParametersOut).

assign_violation_found(contradiction_found,false,Txt) :- !, Txt='NONE EXISTS'.

assign_violation_found(solution(S),true,S) :- !.

assign_violation_found(time_out,R,time_out) :- !, R= time_out.

assign_violation_found(X,false,'NONE FOUND'(X)).

cbc_refinement_check(List,ViolationFound) :-
    (animation_minor_mode(eventb)
    -> eventb_refinement_check(List,ViolationFound)
    ; classical_refinement_check(List,ViolationFound)).

cbc_solve_predicate(Pred,State,Res) :- TimeoutFactor=1,
    solve_predicate(Pred,State,TimeoutFactor,[clean_up_pred,use_smt_mode/true,use_clpfd_solver/true],Res).

classical_refinement_check(ResultList,ViolationFound) :-
    % fetch Axioms and Invariant/properties first
    full_b_machine(Machine),
    b_get_refined_machine(AbsMachine)
    -> b_get_invariant_from_machine(Invariant0),
    add_labels_to_texpr(Invariant0,['Invariant I'], Invariant),
    b_get_linking_invariant_from_machine(LinkingInvariant0),
    add_labels_to_texpr(LinkingInvariant0,['Linking Invariant J'], LinkingInvariant),
    % check initialisation po
    initialisation_pos(LinkingInvariant,Machine,AbsMachine,IniPos,V1),
    % check all operation pos
    get_all_operations_from_machine(Machine,ConcreteOperations),
    get_all_operations_from_machine(AbsMachine,AbstractOperations),
    operations_pos(ConcreteOperations,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,ListOpPos,V2),
    append([[IniPos],['\n'],ListOpPos],ResultList),
    merge_violation_found([V1,V2],ViolationFound)
    ; ResultList = ['Not a Refinement Machine'].

create_equals([],[],[]).

create_equals([Id|Ids],[Expr|Exprs],[TPred|SubPreds]) :-
    safe_create_texpr(equal(Id,Expr),pred,TPred),
    create_equals(Ids,Exprs,SubPreds).

eventb_refinement_check(ResultList,ViolationFound) :-
    % fetch Axioms and Invariant/properties first
    full_b_machine(Machine),
    (get_section(axioms,Machine,Axioms) -> true ; Axioms = []),
    b_get_invariant_from_machine(Invariant),
    b_get_properties_from_machine(Properties),
    % evt/p/WFIS
    witness_feasibility(Axioms,Invariant,Properties,ListWF,V1),
    % evt/grd/GRD proof obligations
    guard_strengthening(Axioms,Invariant,Properties,ListGS,V2),
    % evt/act/SIM
    action_simulation(Axioms,Invariant,Properties,ListAS,V3),
    append([ListWF,['\n'],ListGS,['\n'],ListAS],ResultList),
    merge_violation_found([V1,V2,V3],ViolationFound).

extract_witness_predicate(Witness,Pred) :-
    get_texpr_expr(Witness,witness(_Id,Pred)).

get_all_operations_from_machine(Machine,Operations) :-
    get_section(operation_bodies,Machine,Ops),
    findall(operation(Name,Results,Parameters,Body),
    (get_texpr_expr(Op,operation(TId,Results,Parameters,Body)),
    get_texpr_id(TId,op(Name)),member(Op,Ops)),
    Operations).

guard_strengthening(Axioms,Invariant,Properties,['Guard Strengthening:'|ResultsFlat],ViolationFound) :-
    % guard strengthening:
    % A & I & J & H & W => G_i
    % guard strengthening (merge):
    % A & I & J & H & W & Tau => G_1 or ... or G_n
    % find all candidates for evt/grd/GRD proof obligations
    findall(RLEVENT,
    (b_get_machine_operation(_Name,_R,_P,Body,_OType,_),
    get_texpr_expr(Body,RLEVENT)),
    ListOfOperations),
    maplist(guard_strengthening_aux(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound),
    append(Results,ResultsFlat),
    merge_violation_found(SubViolationFound,ViolationFound).

guard_strengthening_aux(_Axioms,_Invariant,_Properties,
    rlevent(_Name,_Section,_Stat,_Parameters,_Guards,_Thm,_Actions,_VWit,_PWit,_Unmod,[]),
    [],false) :- !. % nothing to check

guard_strengthening_aux(Axioms,Invariant,Properties,
    rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,_Actions,VWit,PWit,_Unmod,[AbsEvent]),
    Results,ViolationFound) :- !,
    get_texpr_expr(AbsEvent,ABSRLEVENT),
    ABSRLEVENT = rlevent(_AbsName,_Absection,_AbsStat,_AbsParameters,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsEvents),
    conjunction_to_list(AbsGrds,AbsGrdsList),
    % map over all abstract guards
    maplist(guard_strengthening_single_event(Name,Axioms,Invariant,Properties,VWit,PWit,Guards),AbsGrdsList,Results,SubViolationFound),
    merge_violation_found(SubViolationFound,ViolationFound).

guard_strengthening_aux(Axioms,Invariant,Properties,
    rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,VWit,PWit,_Unmod,AbsEvents),
    [Result],ViolationFound) :-
    % concrete before-after-predicate
    b_get_machine_variables(Vars),
    b_get_machine_constants(Consts),
    append(Vars,Consts,Both),
    before_after_predicate_list_conjunct_with_equalities(Actions,Both,Tau),
    % collect all abstract guards G_i and negate
    findall(AbsGrds,
    (member(Evt,AbsEvents),
    get_texpr_expr(Evt,rlevent(_AbsName,_AbsSection,_AbsStat,_AbsParams,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsAbsEvents))),
    ListOfAbstractGuards),
    maplist(create_negation,ListOfAbstractGuards,NegatedAbstractGuards),
   
    % build up predicate A & I & J & H & W & Tau => G_1 or ... or G_n
    maplist(extract_witness_predicate,VWit,VWitPreds),
    maplist(extract_witness_predicate,PWit,PWitPreds),
   
    append([Axioms,[Invariant,Properties,Guards,Tau],VWitPreds,PWitPreds,NegatedAbstractGuards],LHSPred),
    conjunct_predicates(LHSPred,Pred),
    cbc_solve_predicate(Pred,State,Res),
   
    assign_violation_found(Res,ViolationFound,ResTxt),
   
    % result string and print
    ajoin([Name,'/MRG: ','Counter-Example found: ', ResTxt],Result),
    formatsilent(' * ~w~n',[Result]),
    (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl).

guard_strengthening_single_event(OpName,_Axioms,_Invariant,_Properties,_VWit,_PWit,_Guards,AbsGrd,Result,false) :-
    get_rodin_name(AbsGrd,GuardName),
    formatsilent('~nChecking single event guard strengthening for: ~w of ~w~n',[GuardName,OpName]),
    b_machine_name(MainMachineName), % we assume that we prove the guard strengthening for the main machine !
    bmachine:discharged_guard_strengthening(MainMachineName,AbstractEvent,GuardName,OpName),
    formatsilent('Guard ~w of ~w is already proven for event ~w:~w !~n',[GuardName,AbstractEvent,MainMachineName,OpName]),
    get_preference(use_po,true),
    !,
    ajoin([OpName,'/',GuardName,'/GRD: ','already proven'],Result).

guard_strengthening_single_event(OpName,Axioms,Invariant,Properties,VWit,PWit,Guards,AbsGrd,Result,ViolationFound) :-
    get_rodin_name(AbsGrd,GuardName),
    % build up predicate and check
    maplist(extract_witness_predicate,VWit,VWitPreds),
    maplist(extract_witness_predicate,PWit,PWitPreds),
    create_negation(AbsGrd,NegAbsGrd),
   
    append([Axioms,[Invariant,Properties,Guards,NegAbsGrd],VWitPreds,PWitPreds],Predicates),
    conjunct_predicates(Predicates,Pred),
   
    cbc_solve_predicate(Pred,State,Res),
    assign_violation_found(Res,ViolationFound,ResTxt),
   
    % result string and print
    ajoin([OpName,'/',GuardName,'/GRD: ','Counter-Example found: ', ResTxt],Result),
    formatsilent(' * ~w~n',[Result]),
    (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl).

initialisation_pos(LinkingInvariant,Machine,AbsMachine,Result,ViolationFound) :-
    % get the two initialisations
    get_section(initialisation,Machine,ConcreteInitialisation),
    get_section(initialisation,AbsMachine,AbstractInitialisation),
   
    % set up proof obligation [T1] not [T] not J (Schneider p.222)
    create_negation(LinkingInvariant,NegLinkingInvariant),
   
    set_reference_machine(AbsMachine),
    weakest_precondition(AbstractInitialisation,NegLinkingInvariant,TempPred),
    delete_reference_machine,
   
    create_negation(TempPred,NotTNotJ),
    weakest_precondition(ConcreteInitialisation,NotTNotJ,PO),
    create_negation(PO,CounterExPO),
   
    cbc_solve_predicate(CounterExPO,State,Res),
    assign_violation_found(Res,ViolationFound,ResTxt),
   
    % result string and print
    ajoin(['Initialisation [T1] not [T] not J: Counter-Example found: ', ResTxt],Result),
    formatsilent(' * ~w~n',[Result]),
    (debug_mode(off) -> true ; nested_print_bexpr(CounterExPO), write(State),nl).

is_concrete_var(b(identifier(Name),_,_)) :- !,
    is_concrete_var(Name).

is_concrete_var(VarName) :-
    b_get_machine_variables(Variables),
    b_machine_name(TopLevelName), % can have prefix MAIN_MACHINE_FOR_
    member(b(identifier(VarName),_Type,Infos),Variables),
    member(occurrences(Machines),Infos),
    member(TopLevelName,Machines).

merge_violation_found(L,true) :-
    some('=='(true),L), !.

merge_violation_found(L,R) :-
    some('=='(time_out),L), !, R=time_out.

merge_violation_found(_,false).

modifies_concrete_var(Action) :-
    get_texpr_info(Action,Info),
    member(modifies(ListOfVars), Info),
    some(is_concrete_var,ListOfVars).

operations_pos([],_I,_LI,_AM,_A,[],false).

operations_pos([operation(Name,Results,_Parameters,_Body)|FurtherOps],Invariant,
    LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound) :-
    % there might be no abstract operation with the same name (includes, etc.)
    \+ (member(operation(Name,_AbsResults,_AbsParameters,_AbsBody),AbstractOperations)), !,
    operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound).

operations_pos([operation(Name,Results,_Parameters,Body)|FurtherOps],Invariant,
    LinkingInvariant,AbsMachine,AbstractOperations,[PreRefPoResult,RefPoResult|ListOpPos],ViolationFound) :-
    % first find the matching abstract operation
    member(operation(Name,_AbsResults,_AbsParameters,AbsBody),AbstractOperations),
   
    % check if we have preconditions - otherwise we assume true
    (get_texpr_expr(Body,precondition(Precondition0,RealBody)) -> true
    ; RealBody=Body, create_texpr(truth,pred,[],Precondition0)),
    add_labels_to_texpr(Precondition0,['P1 (concrete PRE)'], Precondition),
    (get_texpr_expr(AbsBody,precondition(AbsPrecondition0,AbsRealBody))
    -> true
    ; AbsRealBody=AbsBody, create_texpr(truth,pred,[],AbsPrecondition0)
    ),
    add_labels_to_texpr(AbsPrecondition0,['P (abstract PRE)'], AbsPrecondition),
   
    % refinement po for the preconditions
    create_negation(Precondition,NegPrecondition), % description
    conjunct_predicates([Invariant,LinkingInvariant,AbsPrecondition,NegPrecondition],PreRefPo),
    cbc_solve_predicate(PreRefPo,State,PreRefPoRes),
    assign_violation_found(PreRefPoRes,V2,RTxt2),
   
    % result string and print
    % This PO is in Section 14.3, page 225 of Schneider's B Book; part of obligation 4 on page 530 of Abrial's B Book
    ajoin([Name, ' Precondition Refinement I & J & P => P1: Counter-Example found: ', RTxt2],PreRefPoResult),
    formatsilent(' * ~w~n',[PreRefPoResult]),
    (debug_mode(off) -> true ; nested_print_bexpr(PreRefPo), write(State),nl),
   
    % for the refinement of operations, we need to rename existing output variables (i.e. prime them)
    prime_identifiers(Results,PrimedResults),
    list_renamings_to_primed_vars(Results,Renamings),
    rename_bt(RealBody,Renamings,RealBodyWithPrimedVariables),
    create_equals(Results,PrimedResults,EqualResultsPred),
   
    % refinement po for the operation
    % I & J & P => [S1[out'/out]] not S not (J & out'=out)
    conjunct_predicates([LinkingInvariant|EqualResultsPred],RHS),
    create_negation(RHS,NegRHS),
   
    set_reference_machine(AbsMachine),
    weakest_precondition(AbsRealBody,NegRHS,RHS2),
    delete_reference_machine,
   
    create_negation(RHS2,NegRHS2),
    weakest_precondition(RealBodyWithPrimedVariables,NegRHS2,RHS3),
    create_negation(RHS3,NegRHS3),
    conjunct_predicates([Invariant,LinkingInvariant,Precondition,NegRHS3],RefPo),
   
    cbc_solve_predicate(RefPo,State2,RefPoRes),
    assign_violation_found(RefPoRes,V1,RTxt),
    % result string and print
    ajoin([Name, ' Refinement I & J & P => S1 not S not J: Counter-Example found: ', RTxt],RefPoResult),
    formatsilent(' * ~w~n',[RefPoResult]),
    (debug_mode(off) -> true ; nested_print_bexpr(RefPo), write(State2),nl),
   
    operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,ListOpPos,SubViolationFound),
   
    merge_violation_found([V1,V2,SubViolationFound],ViolationFound).

witness_feasibility(Axioms,Invariant,Properties,['Witness Feasibility:'|FlatResults],ViolationFound) :-
    % action simulation:
    % A & I & J & H & W & Tau => Q_i
    % find all candidates for evt/act/SIM proof obligations
    findall(RLEVENT,
    (b_get_machine_operation(_Name,_R,_P,Body,_OType,_OpPos),
    get_texpr_expr(Body,RLEVENT)),
    ListOfOperations),
    maplist(witness_feasibility_aux(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound),
    append(Results,FlatResults),
    merge_violation_found(SubViolationFound,ViolationFound).

witness_feasibility_aux(Axioms,Invariant,Properties,
    rlevent(Name,_Section,_Stat,Parameters,Guards,_Thm,_Actions,_VWit,PWit,_Unmod,AbsEvents),
    ResultsParameters,ViolationFound) :-
    % feasibility for parameters - the abstract events have a parameter
    % that is not a parameter of the concrete events
    all_abstract_parameters(AbsEvents,AllAbsParameters),
    subtract(AllAbsParameters,Parameters,ParametersForWfisPos),
   
    conjunct_predicates([Invariant,Properties,Guards|Axioms],LHSPred),
   
    % map over all abstract events
    maplist(witness_feasibility_parameters(Name,LHSPred,PWit),ParametersForWfisPos,ResultsParameters,SubViolationFound),
    merge_violation_found(SubViolationFound,ViolationFound).

witness_feasibility_parameters(Name,LHSPred,PWit,Parameter,Result,ViolationFound) :-
    % find matching witness - same identifier
    get_texpr_id(Parameter,Identifier),
    member(Witness,PWit), get_texpr_expr(Witness,witness(WitnessIdentifier,Pred)),
    get_texpr_id(WitnessIdentifier,Identifier), !,
   
    % set up PO: A & I & J & H => exists p : W_p
    construct_optimized_exists([Parameter],Pred,ExistsPred),
    create_negation(ExistsPred,NegatedExistsPred),
    conjunct_predicates([LHSPred,NegatedExistsPred],CounterExamplePred),
   
    cbc_solve_predicate(CounterExamplePred,State,Res),
    assign_violation_found(Res,ViolationFound,ResTxt),
   
    % result string
    ajoin([Name,'/',Identifier,'/WFIS: ','Counter-Example found: ', ResTxt],Result),
    % print
    formatsilent(' * ~w~n',[Result]),
    (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl).