enabling_predicates

compute_enabling_predicate(OpName,OmitOpNameGuard,Pred,FindInvViolations,Res) :-
    b_get_machine_operation(OpName,_Res,Par,Body),
    (FindInvViolations==1 ->
    b_get_invariant_from_machine(Inv),
    conjunct_predicates([Inv,Pred],Pred1)
    ;
    Pred1 = Pred
    ),
    % TODO: add a case for Event-B
    % compute wp when the source operation is deterministic
    get_preference(enable_graph_depth,Depth),
    (Depth==0 ->
    WP = b(truth,pred,[])
    %add_warning(weakest_precondition,'Weakest precondition cannot be computed: ',(body(Body),pred(Pred))),
    %Res = invariant
    ;
    create_event_body(OpName,Par,Body,NewBody),
    compute_ep(NewBody,OmitOpNameGuard,Pred1,WP1),
    %remove_all_infos(WP1,WP2), % consider to use remove_all_infos/2 (problem: all nodeid's will be replaced by a variable,
    % this causes instatiations errors when using predicate simplifier.)
    remove_nodeid_infos(WP1,WP)
    ),
    print_weakest_precondition(OpName,Body,Pred,WP),
    %% print(weakest_precondition(WP)),nl,
    simplify_b_predicate(WP,Simplified),
    print_b_expression(Simplified),
    Res=predicate(Simplified).

compute_ep(Body,OmitBodyGuard,Pred,WP) :-
    (OmitBodyGuard==true ->
    get_texpr_expr(Body,Expr),
    compute_ep1(Expr,Pred,WP)
    ;
    weakest_precondition(Body,Pred,WP)
).

compute_ep1(precondition(_Condition,Action),Pred,WP) :- !,
    % here we do not add the Condition as a conjunct
    weakest_precondition(Action,Pred,WP).

compute_ep1(select([When]),Pred,WP) :- !,
    get_texpr_expr(When,select_when(_PreCond, Body)),
    weakest_precondition(Body,Pred,WP).

compute_ep1(any(Parameters,Guard,Action),Pred,WP) :- !,
    remove_free_predicates(Parameters,Guard,NewGuard),
    weakest_precondition(Action,Pred,InnerWP),
    safe_create_texpr(conjunct(NewGuard,InnerWP),pred,UnquantifiedWP),
    create_or_merge_exists(Parameters,UnquantifiedWP,WP).

compute_ep1(rlevent(_Name,_Section,_Stat,Parameters,Guard,_Thm,Act,_VWit,_PWit,_Unmod,_AbsEvents),Pred,EP) :- !,
    %% debug:debug_println(9,rlevent(_Name,_Section,_Stat,Parameters,Guard,_Thm,Act,_VWit,_PWit,_Unmod,_AbsEvents)),
    % we have "ANY t WHERE Q THEN T END" statement (here we need to add the guard to the WP)
    % we can sort out the free predicates from Q (at the point of testing the WP we know that there is a representation of the non-deterministic event)
    remove_free_predicates(Parameters,Guard,RestrictedGuard),
    % we normalise each event for the case that there are non-deterministic assignments
    (is_list(Act) ->
    normalise_to_deterministic_actions_event(Act,NewBody,Parameters,NewParameters,RestrictedGuard,NewGuard)
    ;
    normalise_to_deterministic_actions_event([Act],NewBody,Parameters,NewParameters,RestrictedGuard,NewGuard)
    ),
    weakest_precondition(NewBody,Pred,WP),
    (NewParameters = [] ->
    EP = WP
    ;
    safe_create_texpr(conjunct(NewGuard,WP),pred,UnquantifiedEP),
    create_exists(NewParameters,UnquantifiedEP,EP)
).

compute_ep1(Body,Pred,EP) :-
    create_texpr(Body,subst,[],WrappedBody),
    weakest_precondition(WrappedBody,Pred,EP).

create_event_body(OpName,Par,Body,Res) :-
    create_event_body1(OpName,Par,Body,Res).

create_event_body1(_OpName,[],Body,Res) :- !,
    Res = Body.

create_event_body1(OpName,Par,Body,Res) :-
    is_list(Par),!,
    get_texpr_expr(Body,Expr),
    get_precondition_body(Expr,Par,OpName,InterimRes),
    create_texpr(InterimRes,subst,[],Res).

create_event_body1(OpName,Par,Body,_Res) :-
    add_error(create_event_body,'The Parameters should be wrapped in a prolog list: ', OpName:Par/Body),fail.

filter_out_global_guards([],_Ids,[]).

filter_out_global_guards([TExpr|TExprs],Ids,Res) :-
    (some_id_occurs_in_expr(Ids,TExpr) ->
    Res=[TExpr|Res1]
    ;
    Res = Res1
    ), filter_out_global_guards(TExprs,Ids,Res1).

gen_rename(TID1,TID2,rename(ID1,ID2)) :- def_get_texpr_id(TID1,ID1), def_get_texpr_id(TID2,ID2).

get_precondition_body(precondition(Condition,Action),Par,_OpName,Res) :- !,
    Res = any(Par,Condition,Action).

get_precondition_body(Body,_Par,_OpName,Res) :-
    functor(Body,rlevent,11),!,
    Res = Body.

get_precondition_body(OpName,Stmt,_Pre,_InnerBody) :-
    add_error(get_precondition_body,'Statement not covered yet: ', OpName:Stmt).

normalise_nondeterministic_actions([],[],[],[]).

normalise_nondeterministic_actions([Act|Acts],Parameters,NewConjuncts,NewActs) :-
    get_texpr_expr(Act,Expr),
    (Expr = becomes_element_of(IDs,Set) ->
    prime_identifiers(IDs,Params),
    weakest_preconditions: create_members(Set,Params,SetCond),
    create_texpr(assign(IDs,Parameters),subst,[],PrimeAssign),
    append(Params,Parameters1,Parameters),
    NewConjuncts=[SetCond|NewConjuncts1],
    NewActs = [PrimeAssign|NewActs1]
    ; Expr = becomes_such(Vars,Condition) -> % x:| x
    % also see get_operation_enabling_condition2
    sort(Vars,Vars1),
    prime_identifiers0(Vars1,PrimedVars), % generate $0 versions for Vars
    maplist(gen_rename,Vars1,PrimedVars,RenameList1), % id -> id$0
    maplist(gen_rename,PrimedVars,Vars1,RenameList2), % id$0 -> id
    append(RenameList1,RenameList2,RenameList),
    rename_bt(Condition,RenameList,Condition1),
    NewConjuncts=[Condition1|NewConjuncts1],
    create_texpr(assign(Vars1,PrimedVars),subst,[],PrimeAssign),
    append(PrimedVars,Parameters1,Parameters),
    NewActs = [PrimeAssign|NewActs1]
    ;
    NewConjuncts = NewConjuncts1,
    NewActs = [Act|NewActs1],
    Parameters = Parameters1
    ),
    normalise_nondeterministic_actions(Acts,Parameters1,NewConjuncts1,NewActs1).