enabling_analysis

add_to_time_out(Extra,OriginalTimeout,New) :-
    (OriginalTimeout < 300 % default for timeout_cbc_analysis is 300
    -> E is (Extra * OriginalTimeout) // 300
    ; E is Extra
    ),
    add_time_outs(OriginalTimeout,E,New).

b_get_sorted_op(Op) :- findall(Op, b_top_level_operation(Op), Ops),
    sort(Ops,SOps), member(Op,SOps).

can_be_modified(ModifiedVars,Pred,Res) :-
    some_id_occurs_in_expr(ModifiedVars,Pred),!, Res='<'.

can_be_modified(_,_,'>').

cbc_dependence_analysis(OpName1,OpName2,Res) :-
    b_top_level_operation(OpName1),
    b_get_read_write_vars(OpName1,GReads1,AReads1,Reads1,Writes1),
    b_get_sorted_op(OpName2),
    (OpName1=OpName2 -> action_dependent_to_itself(OpName1,GReads1,Writes1,Res) % TO DO: check if it is possible that for two different parameter values of the same event there is dependence
    ; OpName2 @< OpName1 -> Res = '-' % our checking is symmetric; only check one pair
    ;
    b_get_read_write_vars(OpName2,GReads2,AReads2,Reads2,Writes2),
    formatsilent("CHECKING DEPENDENCE: ~w gr:~w / ar:~w / w:~w <--> ~w gr:~w / ar:~w / w:~w~n",[OpName1,GReads1,AReads1,Writes1,OpName2,GReads2,AReads2,Writes2]),
    ( syntactical_independence(Reads1,Writes1,Reads2,Writes2) -> Res = syntactic_independent
    ; vars_ord_intersect(Writes1,Writes2) -> Res = race_dependent
    ; (vars_ord_intersect(AReads1,Writes2);vars_ord_intersect(AReads2,Writes1)) -> Res = race_dependent
    % TO DO: in this case check if there is indeed a race dependence (e.g. in scheduler new and ready_active are actually independent !)
    % Set up [OpName1,OpName2], [OpName2,OpName1] and see if for ord_intersect(Writes1,Writes2) we can find different values
    ;
    % get constraints for G_{Op_1} \leadsto{Op_2} not(G_{Op_1})
    get_negated_guard(OpName1,PosGuard1,NegGuard1),
    get_conj_inv_predicate([NegGuard1],1,NegGuard1_Inv),
    % get constraints for G_{Op_2} \leadsto{Op_1} not(G_{Op_2})
    get_negated_guard(OpName2,PosGuard2,NegGuard2),
    get_conj_inv_predicate([NegGuard2],1,NegGuard2_Inv),
    conjunct_predicates([PosGuard1,PosGuard2],GuardsConj),
    (vars_ord_intersect(GReads1,Writes2),
    testcase_path_timeout_catch(pred(GuardsConj),500,[OpName2],NegGuard1_Inv,_Constants,_Ops,_TestS,_TI,R1)
    -> formatsilent(" ~w may disable ~w (~w)!~n",[OpName2,OpName1,R1]),
    (is_timeout(R1) -> Res=timeout_dependent; Res = dependent)
    ; (vars_ord_intersect(GReads2,Writes1),
    testcase_path_timeout_catch(pred(GuardsConj),500,[OpName1],NegGuard2_Inv,_,_,_,_,R2))
    -> formatsilent(" ~w may disable ~w (~w)!~n",[OpName1,OpName2,R2]),
    (is_timeout(R2) -> Res=timeout_dependent; Res = dependent)
    ; Res = independent))).

cbc_enable_analysis(OpName1,OpName2,Enable,ExtraTimeout) :-
    init_or_op(OpName1),
    if(cbc_enable_analysis_cache(OpName1,OpName2,Result,ExtraTimeout),
    Result = Enable, % already computed
    (% now compute all enablings form OpName1
    cbc_enable_analysis_calc(OpName1,Op2,R,ExtraTimeout),
    assertz(cbc_enable_analysis_cache(OpName1,Op2,R,ExtraTimeout)),
    fail
    ;
    % now look up:
    cbc_enable_analysis_cache(OpName1,OpName2,Enable,ExtraTimeout)
)).

cbc_enable_analysis_calc(OpName1,OpName2,Enable,ExtraTimeout) :-
    OpName1='INITIALISATION',printsilent('CHECKING ENABLING AFTER INITIALISATION'),nls,
    b_top_level_operation(OpName2),
    printsilent('INITIALISATION'), printsilent(' ---> '), printsilent(OpName2), printsilent(' :: '),
    add_to_time_out(ExtraTimeout,200,Timeout),
    ( testcase_path_timeout_catch(init,Timeout,[OpName2],b(truth,pred,[]),_Constants,_Ops,_TestS,_TI,R)
    -> printsilent(R), printsilent(' : '),
    get_negated_guard(OpName2,_,NegGuard),
    (testcase_path_timeout_catch(init,Timeout,[],NegGuard,_Constants2,_Ops2,_TestS2,_TI2,R2)
    -> printsilent(R2), printsilent(' : '),Enable=possible
    ; Enable=guaranteed)
    ; Enable=impossible),
    printsilent(Enable),nls.

cbc_enable_analysis_calc(OpName1,OpName2,Enable,ExtraTimeout) :-
    b_top_level_operation(OpName1),
    b_get_read_write(OpName1,Reads1,Writes1),
    %b_get_operation_read_guard_vars(OpName1,true,Reads1,_Precise),
    %get_negated_guard(OpName1,PosGuard1,_NegGuard1),
    formatsilent("CHECKING ENABLING AFTER: ~w r:~w / w:~w~n",[OpName1,Reads1,Writes1]),
    b_top_level_operation(OpName2),
    formatsilent('~w ---> ~w :: ',[OpName1,OpName2]),
    cbc_enable_calc_aux(OpName1,Writes1,OpName2,Enable,ExtraTimeout),
    formatsilent('Enable=~w~n',[Enable]).

cbc_enable_calc_aux(OpName1,_Writes1,_OpName2,Enable,ExtraTimeout) :-
    (ExtraTimeout>500 -> infeasible_operation(OpName1)
    ; infeasible_operation_cache(OpName1)), % only check cached version
    !,
    Enable=infeasible.

cbc_enable_calc_aux(_OpName1,_Writes1,OpName2,Enable,ExtraTimeout) :-
    (ExtraTimeout>500 -> infeasible_operation(OpName2)
    ; infeasible_operation_cache(OpName2)), % only check cached version
    !,
    Enable=impossible_infeasible.

cbc_enable_calc_aux(OpName1,_Writes1,OpName2,Enable,_) :-
    % first check if we can syntactically determine independence
    syntactic_independence(OpName1,OpName2,Res),
    !,
    Enable=Res.

cbc_enable_calc_aux(OpName1,Writes1,OpName2,Enable,ExtraTimeout) :-
    % now we do the semantic checks
    add_to_time_out(ExtraTimeout,200,Timeout1),
    add_to_time_out(ExtraTimeout,300,Timeout2),
   
    get_negated_guard(OpName2,PosGuard2,NegGuard2),
    filter_predicate(PosGuard2,Writes1,FilteredPosGuard2),
    create_negation(FilteredPosGuard2,FilteredNegGuard2),
    cbc_enable_calc_aux2(OpName1,OpName2,Enable,Timeout1,Timeout2,PosGuard2,NegGuard2,FilteredNegGuard2).

cbc_enable_calc_aux2(OpName1,OpName2,Enable,Timeout1,Timeout2,PosGuard2,NegGuard2,FilteredNegGuard2) :-
    %format('Check if ~w can be enabled after ~w ~n',[OpName2,OpName1]),
    %print(' Pos Guard: '),translate:print_bexpr(PosGuard2),nl,
    %((OpName1=winc,OpName2=winc) -> trace ; true),
    testcase_path_timeout_catch(invariant,Timeout1,[OpName1],PosGuard2,_Csts,_Ops,_TestS,_TI,R), % advantage over version with [OpName1,OpName2] : one less state to setup and enumerate; but inner guards may not be checked
    !,
    printsilent(can_be_enabled_after(R)), printsilent(' : '),
    % print('Neg Guard: '),translate:print_bexpr(NegGuard2),nl,
    % TO DO: first check whether OpName2 can be disabled given Invariant ?
    (testcase_path_timeout_catch(invariant,Timeout1,[OpName1],NegGuard2,_Csts2,_Ops2,_TestS2,_TI2,R2)
    -> printsilent(can_be_disabled_after(R2)), printsilent(' : '),
    % TO DO: test if NegGuard2 holds initially it is possible to execute [OpName1,OpName2]; if not: OpName1 cannot enable OpName2, only keep it -> Enable=keep_possible
    % then we could check if OpName1 can disable OpName2: PosGuard2,[OpName1],NegGuard2
    (OpName1\=OpName2, % otherwise OpName2 must be enabled if [OpName1] can be executed
    %testcase_path_timeout_catch(pred(NegGuard2),Timeout2,[OpName1,OpName2],b(truth,pred,[]),_,_,_,_,R3)
    testcase_path_timeout_catch(pred(NegGuard2),Timeout2,[OpName1],PosGuard2,_,_,_,_,R3)
    -> printsilent(can_enable(R3)), printsilent(' : '),
    %nl, translate:print_bexpr(PosGuard2),nl,print(OpName1),nl,translate:print_bexpr(NegGuard2),nl,
    %print('FILTERED: '), translate:print_bexpr(FilteredNegGuard2),nl,
    (testcase_path_timeout_catch(pred(PosGuard2),Timeout2,[OpName1],FilteredNegGuard2,_,_,_,_,R4)
    -> printsilent(can_disable(R4)), printsilent(' : '),
    (contains_timeout([R,R2,R3,R4]) -> Enable=timeout_possible ; Enable=possible)
    ; printsilent('cannot_disable : '),
    (contains_timeout([R,R2,R3]) -> Enable=timeout_possible_enable ; Enable=possible_enable) /* Opname cannot disable OpName2; only enable it */
    )
    ; /* OpName1 cannot enable OpName2; only preserve it */
    printsilent('cannot_enable : '),
    (testcase_path_timeout_catch(pred(PosGuard2),Timeout2,[OpName1],FilteredNegGuard2,_,_,_,_,R4)
    -> printsilent(can_disable(R4)), printsilent(' : '),
    (contains_timeout([R,R2,R4]) -> Enable=timeout_possible_disable; Enable=possible_disable)
    ; (contains_timeout([R,R2]) -> Enable=timeout_keep; Enable=keep) /* Opname cannot enable or disable */
    )
    )
    ; (is_timeout(R) -> Enable=timeout_guaranteed; Enable=guaranteed)
).

cbc_enable_calc_aux2(OpName1,_OpName2,Enable,_Timeout1,Timeout2,PosGuard2,_NegGuard2,FilteredNegGuard2) :-
    % OpName2 can never be enabled after OpName1; check whether it can be enabled before
    % Note: we could replace FilteredNegGuard2 by truth
    testcase_path_timeout_catch(pred(PosGuard2),Timeout2,[OpName1],FilteredNegGuard2,_,_,_,_,R4),
    !,
    printsilent(can_disable(R4)), printsilent(' : '),
    (is_timeout(R4) -> Enable=timeout_impossible; Enable=impossible).

cbc_enable_calc_aux2(_OpName1,_OpName2,Enable,_,_,_PosGuard2,_NegGuard2,_FilteredNegGuard2) :-
    % OpName2 can never ben enabled after nor before
    Enable=impossible_keep.

cbc_quick_cfg_analysis(OpName1,OpName2,Res) :-
    OpName1='INITIALISATION',
    b_top_level_operation(OpName2),
    b_get_read_write(OpName2,Reads2,Writes2),
    formatsilent(user_output,"COMPUTING CFG: INITIALISATION --> ~w r:~w / w:~w~n~n",
    [OpName2,Reads2,Writes2]),
    ( testcase_path_timeout_catch(init,250,[OpName2],b(truth,pred,[]),_Constants,_Ops,_TestS,_TI,R1)
    -> formatsilent(user_output," ~w can be enabled by ~w (~w)!~n",[OpName2,OpName1,R1]),
    (is_timeout(R1) -> Res=timeout_possible; Res = possible)
    ; formatsilent(user_output," ~w cannot be enabled by ~w!~n",[OpName2,OpName1]),
    Res = cannot_enable
).

cbc_quick_cfg_analysis(OpName1,OpName2,Res) :-
    b_top_level_operation(OpName1), % top_level
    b_get_read_write(OpName1,Reads1,Writes1),
    %get_negated_guard(OpName1,PosGuard1,NegGuard1),
    b_get_sorted_op(OpName2),
    (b_get_read_write(OpName2,Reads2,Writes2),
    formatsilent(user_output,"COMPUTING CFG: ~w r:~w / w:~w --> ~w r:~w / w:~w~n~n",
    [OpName1,Reads1,Writes1,OpName2,Reads2,Writes2]),
    (\+ vars_ord_intersect(Writes1,Reads2)
    -> (vars_ord_intersect(Writes1,Writes2)
    -> Res = race_dependent, formatsilent(user_output," ~w cannot be enabled/disabled by ~w!~n",[OpName2,OpName1])
    ; Res = syntactic_independent, formatsilent(user_output," ~w cannot be enabled/disabled/modified by ~w!~n",[OpName2,OpName1])
    )
    ; get_negated_guard(OpName2,PosGuard2,NegGuard2),
    garbage_collect,
    print('Guard: '), translate:print_bexpr(PosGuard2),nl,
    ((testcase_path_timeout_catch(typing(NegGuard2),60,[OpName1],PosGuard2,_,_,_,_,_R0), % quick check without invariants & properties
    % TO DO: project constants, variables onto the ones really needed
    testcase_path_timeout_catch(pred(NegGuard2),250,[OpName1],PosGuard2,_Constants,_Ops,_TestS,_TI,R1))
    -> formatsilent(user_output," ~w can be enabled by ~w (~w)!~n",[OpName2,OpName1,R1]),
    (is_timeout(R1) -> Res=timeout_possible; Res = possible)
    ; formatsilent(user_output," ~w cannot be enabled by ~w!~n",[OpName2,OpName1]),
    Res = cannot_enable)
)
).

cfg_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
    cbc_quick_cfg_analysis(NodeID,SuccID,Res),
    translate_res(Res,NodeID,SuccID,Label,Color,Style).

check_if_feasible_operation(OpName1,UseInvariant,TimeoutFactor,Res,NormalisedResultState) :-
    b_top_level_operation(OpName1),
    (debug_mode(on)
    -> print(checking_feasibility(OpName1)),nl,tools:start_ms_timer(TIMER) ; true),
    if(check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,State),true,
    (add_internal_error('Failed:',check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,State)),fail)),
    % TO DO: add missing variables and put into order
    normalise_enabling_store(State,NormalisedResultState),
    %b_interpreter:sort_variable_binding(NormalisedResultState,SortedStore),
    stop_ms_timer_with_debug_msg(TIMER,feasible(OpName1)).

check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,ResultState) :-
    get_negated_guard(OpName1,PosGuard1,_NegGuard1,Precise),
    % format('Guard is ~w for ~w~n',[Precise,OpName1]),
    Precise = precise,
    !,
    % Warning: guard is under approximation for sequential composition, while loops, ...
    get_conj_inv_predicate([PosGuard1],UseInvariant,Pred),
    (debug_mode(on) -> translate:nested_print_bexpr(Pred),nl ; true),
    % visualize_graph:print_predicate_dependency_as_graph_for_dot(Pred,'~/Desktop/out.dot'),
    (solve_predicate_with_chr(Pred,State,TimeoutFactor,[full_machine_state],RR)
    -> %print(state(_State)),nl, print(result(RR)),nl,
    ((RR=no_solution_found(unfixed_deferred_sets) ; RR = contradiction_found)
    -> Res = impossible, ResultState = '$UNKNOWN_STATE'
    %,format('Computing unsat core for infeasible ~w~n',[OpName1]),unsat_cores:unsat_core(Pred,no_solution_found,Core),print('CORE: '),nl,translate:nested_print_bexpr_as_classicalb(Core),nl
    ; RR=solution(_) -> Res = possible,
    (debug_mode(on) -> print('SOLUTION: '),translate:print_bstate(State),nl ; true),
    ResultState = State
    ; simplify_for_output(RR,Res), ResultState = '$UNKNOWN_STATE' )
    ; add_internal_error('Failed to compute feasibility for: ',OpName1),
    translate:print_bexpr(Pred),nl,
    Res = internal_error, ResultState = '$UNKNOWN_STATE').

check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,ResultState) :-
    formatsilent('Guard computation is imprecise for ~w. Not using predicate solver (but B interpreter).~n',[OpName1]),
    % this version uses sap:testcase_path: this works for things like sequential composition and WHILE loops better
    get_time_out_with_factor(TimeoutFactor,TO),
    (UseInvariant=1 -> INV=invariant ; INV=typing),
    (testcase_path_timeout_catch(INV,TO,[OpName1],b(truth,pred,[]),_Constants,Ops,StateSequence,_TI,R1)
    -> (is_timeout(R1) -> Res=timeout ; Res = possible),
    (nonvar(StateSequence),StateSequence=[ResultState|_] -> true ; ResultState = '$UNKNOWN_STATE'),
    (debug_mode(off) -> true
    ; print(feasibility_result(OpName1,R1,Ops)),nl,
    (ResultState = '$UNKNOWN_STATE' -> true
    ; print('SOLUTION: '),translate:print_bstate(ResultState),nl)
    )
    ; Res=impossible,ResultState = '$UNKNOWN_STATE').

combine_simult_result(solution(_),solution(_),R) :- !,R=possible.

combine_simult_result(solution(_),B,R) :-
    (B = contradiction_found ; B = no_solution_found(unfixed_deferred_sets)), !,
    R=guaranteed.

combine_simult_result(A,B,Res) :- functor(A,FA,_), functor(B,FB,_),
    ajoin([FA,'_',FB],Res).

compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,[Enable,KeepEnabled,Disable,KeepDisabled]) :-
    b_top_level_operation(OpName1),
    b_get_read_write(OpName1,_,Writes1),
    b_get_operation_read_guard_vars(OpName1,true,Reads1,_Precise),
    formatsilent("CHECKING ENABLING RELATION AFTER: ~w r:~w / w:~w~n",[OpName1,Reads1,Writes1]),
    b_top_level_operation(OpName2),
    get_negated_guard(OpName2,PosGuard2,_NegGuard2),
    partition_predicate(PosGuard2,Writes1,FilteredPosGuard2,StaticPosGuard2),
    create_negation(FilteredPosGuard2,FilteredNegGuard2),
    Timeout1 is 300+ExtraTimeout,
    formatsilent('~w ---> ~w :: ',[OpName1,OpName2]),
    %print(' FPOS: '),translate:print_bexpr(FilteredPosGuard2),nl,
    %print('Neg Guard: '),translate:print_bexpr(NegGuard2),nl,
    %print(' Filtered: '),translate:print_bexpr(FilteredNegGuard2),nl,
    % TO DO: use syntactic conditions
    my_testcase_path_timeout(pred(PosGuard2),Timeout1,[OpName1],FilteredPosGuard2,KeepEnabled),
    my_testcase_path_timeout(pred(PosGuard2),Timeout1,[OpName1],FilteredNegGuard2,Disable),
    (OpName1==OpName2 -> KeepDisabled=false, Enable=false
    ; conjunct_predicates([StaticPosGuard2,FilteredNegGuard2],NegEnableGuard2), % as StaticPosGuard2 must be same before after: it must be true before to be true after
    my_testcase_path_timeout(pred(NegEnableGuard2),Timeout1,[OpName1],FilteredPosGuard2,Enable),
    % this is the unoptimised call:
    %my_testcase_path_timeout(pred(NegGuard2),Timeout1,[OpName1],NegGuard2,KeepDisabled),
    % we do two calls for KeepDisabled: pred(NegStaticGuard2) true after, or StaticGuard2 & NegFiltered -> NegFiltered
    create_negation(StaticPosGuard2,StaticNegGuard2),
    my_testcase_path_timeout(pred(StaticNegGuard2),Timeout1,[OpName1],b(truth,pred,[]),KeepDisabled1),
    (KeepDisabled1 = ok -> KeepDisabled=ok
    ; my_testcase_path_timeout(pred(NegEnableGuard2),Timeout1,[OpName1],FilteredNegGuard2,KeepDisabled)
    ),
    formatsilent(' KeepEnabled=~w, Disable=~w, Enable=~w, KeepDisabled=~w~n',
    [KeepEnabled,Disable,Enable,KeepDisabled])
).

contains_timeout(List) :- (member(timeout,List) -> true ; member(clpfd_overflow,List) -> true).

eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,black) :-
    op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,_Color).

eop_node_predicate('INITIALISATION',SubGraph,'INITIALISATION',Shape,Style,Color) :- SubGraph=none,
    Shape=hexagon, Style=none, Color=olivedrab2.

feasible_operation(Op,Res) :- feasible_operation_cache(Op,CR),!,Res=CR.

feasible_operation(Op,Res) :- UseInvariant=1,
    check_if_feasible_operation(Op,UseInvariant,fixed_time_out(500),CR,_),
    assertz(feasible_operation_cache(Op,CR)),
    Res=CR.

feasible_operation_with_timeout(Op,TimeOut,Res) :- feasible_operation_cache(Op,CR),
    (CR \= unknown ; TimeOut =< 500), !, Res=CR.

feasible_operation_with_timeout(Op,TimeOut,Res) :- check_if_feasible_operation(Op,1,fixed_time_out(TimeOut),CR,_),
    retractall(feasible_operation_cache(Op,_)), % must be unknown if it was asserted before
    assertz(feasible_operation_cache(Op,CR)),
    Res=CR.

filter_predicate(Pred,ModifiedVars,FilteredPred) :- partition_predicate(Pred,ModifiedVars,FilteredPred,_).

impossible(impossible).

impossible(impossible_keep).

impossible(impossible_disable).

impossible(impossible_infeasible).

impossible(infeasible).

independent(independent,yellow).

independent(syntactic_keep,lightgray).

independent(syntactic_independent,lightgray).

independent(syntactic_fully_independent,lightgray).

independent(syntactic_unchanged,lightgray).

independent(activation_indepdendent,lightgray).

infeasible_operation(Op) :- feasible_operation_cache(Op,CR),!, CR=impossible.

infeasible_operation(Op) :- operation_not_yet_covered(Op),
    feasible_operation(Op,impossible). % will also assert feasible_operation_cache

infeasible_operation_cache(Op) :- feasible_operation_cache(Op,impossible).

init_or_op('INITIALISATION').

init_or_op(OpName1) :- b_top_level_operation(OpName1). %b_get_machine_operation(OpName1,_,_,_).

insert_commas('$all',_,['ALL']).

insert_commas([],_,[]).

insert_commas([H],_,R) :- !, R=[H].

insert_commas([H|T],N,[H,Sep|IT]) :-
    (N>5 -> N1=0, Sep=',\\n' ; N1 is N+1, Sep=', '),
    insert_commas(T,N1,IT).

is_timeout_enabling_result(timeout_keep).

is_timeout_enabling_result(timeout_possible).

is_timeout_enabling_result(timeout_possible_disable).

is_timeout_enabling_result(timeout_possible_enable).

is_timeout_enabling_result(timeout).

is_timeout_enabling_result(timeout_dependent).

is_timeout_enabling_result(timeout_guaranteed).

is_timeout_enabling_result(timeout_impossible).

my_testcase_path_timeout(Before,Timeout,Path,After,Result) :-
    (testcase_path_timeout_catch(Before,Timeout,Path,After,_,_,_,_,Result) -> true
    ; Result = false).

normalise_enabling_store('$UNKNOWN_STATE',R) :- !, R='$UNKNOWN_STATE'.

normalise_enabling_store(CState,State) :- normalise_store(CState,State).

op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :-
    get_preference(dot_enabling_show_readwrites,false), !,
    SubGraph=none, Shape=box, Style=none,
    b_top_level_operation(Op), NodeID = Op, NodeDesc=Op, Color=blue.

op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- SubGraph=none,
    Shape=record, Style=none,
    b_top_level_operation(Op), NodeID = Op,
    %NodeDesc = NodeID,
    b_get_read_write(Op,Reads2,Writes1),
    b_get_operation_read_guard_vars(Op,false,ReadsGrd,_Precise),
    insert_commas(ReadsGrd,0,R1), insert_commas(Reads2,0,R2), insert_commas(Writes1,0,W1),
    append(W1,['}|'],W2),
    append(R1,['\\n|reads: '|R2],Reads),
    append(Reads,['\\n|writes: '|W2],As),
    ajoin(['|{',Op,'\\n|reads (guard): '|As],NodeDesc),
    Color=blue.

operation_can_be_enabled_by(OpName1,OpName2,TIMEOUT,Res) :-
    b_top_level_operation(OpName1),
    b_get_read_write(OpName1,_Reads1,Writes1),
    b_top_level_operation(OpName2),
    formatsilent("~nCHECKING if ~w (~w) can enable ~w~n",[OpName1,Writes1,OpName2]),
    \+ static_cannot_enable(OpName1,OpName2),
    get_negated_guard(OpName2,PosGuard2,_NegGuard2),
    filter_predicate(PosGuard2,Writes1,FilteredPosGuard2),
    create_negation(FilteredPosGuard2,FilteredNegGuard2),
    % TIMEOUT used to be hardwired to 500
    % print('Before: '), translate:print_bexpr(FilteredNegGuard2),nl,print('After: '), translate:print_bexpr(PosGuard2),nl,
    testcase_path_timeout_catch(pred(FilteredNegGuard2),TIMEOUT,[OpName1],PosGuard2,_,_,_,_,Res),
    println_silent(can_be_enabled_result(Res)).

operation_sequence_possible(OpName1,OpName2,Res) :-
    static_cannot_enable(OpName1,OpName2), %\+ static_activation_dependent(OpName1,OpName2),
    !,
    Res = activation_independent.

operation_sequence_possible(OpName1,OpName2,Res) :-
    % we assume OpName2 is feasible on its own
    get_negated_guard(OpName2,PosGuard2,_NegGuard2),
    Timeout1 = 200,
    % print('Guard: '),translate:print_bexpr(PosGuard2),nl,
    (testcase_path_timeout_catch(invariant,Timeout1,[OpName1],PosGuard2,_Csts,_Ops,_TestS,_TI,Res)
    -> true
    ; Res = impossible
).

partition_predicate(Pred,Var,FilteredPred,Rest) :- var(Var),!,
    add_internal_error('Missing write variables:',partition_predicate(Pred,Var,FilteredPred,Rest)),
    partition_predicate(Pred,'$all',FilteredPred,Rest).

partition_predicate(Pred,'$all',FilteredPred,Rest) :- !, FilteredPred=Pred, Rest=b(truth,pred,[]).

partition_predicate(Pred,ModifiedVars,FilteredPred,Rest) :-
    conjunction_to_list(Pred,List),
    partition(can_be_modified(ModifiedVars),List,FilteredList,[],UnFilteredList),
    conjunct_predicates(FilteredList,FilteredPred),
    conjunct_predicates(UnFilteredList,Rest).

print_csv_el(H) :- format(' ~w',[H]).

print_csv_list([]) :- !,nl.

print_csv_list([H]) :- !,print(H),nl.

print_csv_list([H|T]) :- !,print(H), print(','), print_csv_list2(T).

print_csv_list(X) :- print(illegal_list(X)),nl, add_internal_error('Illegal list: ', print_csv_list(X)).

print_csv_list2([H]) :- !,print_enable_info(H),nl.

print_csv_list2([H|T]) :- !,print_enable_info(H), print(','), print_csv_list2(T).

print_csv_list2(X) :- print(illegal_list(X)),nl, add_internal_error('Illegal list: ', print_csv_list(X)).

print_enable_info(I) :- (translate_enable_info(I,TI) -> print(TI) ; print_for_csv(I)).

print_enable_table(R) :- print_enable_table_list(R).

print_enable_table_list([]) :- nl,nl.

print_enable_table_list([list(L)|T]) :-
    print_csv_list(L), print_enable_table_list(T).

print_for_csv([]) :- !, print('{}').

print_for_csv([H|T]) :- !, % print list without commas ,
    format('{~w',[H]), maplist(print_csv_el,T), print('}').

print_for_csv(Term) :- print(Term).

reset_enabling_analysis :-
    %retractall(disable_graph(_)),
    retractall(feasible_operation_cache(_,_)),
    retractall(cbc_enable_analysis_cache(_,_,_,_)).

simplify_for_output(no_solution_found(enumeration_warning(_,_,_,_,_)),virtual_time_out).

simplify_for_output(no_solution_found(clpfd_overflow),overflow).

simplify_for_output(time_out,time_out).

simult_enable_analysis(OpName1,OpName2,UseInvariant,TimeoutFactor,Res) :-
    b_top_level_operation(OpName1),
    b_top_level_operation(OpName2),
    %OpName2 @>OpName1,
    get_negated_guard(OpName1,PosGuard1,_NegGuard1),
    get_negated_guard(OpName2,PosGuard2,NegGuard2),
    get_conj_inv_predicate([PosGuard1,PosGuard2],UseInvariant,Pred),
    %print(checking_simultaneous(OpName1,OpName2)),nl,
    (solve_predicate_with_chr(Pred,_State,TimeoutFactor,[],RR)
    -> %print(state(_State)),nl, print(result(RR)),nl,
    ((RR = contradiction_found ; RR = no_solution_found(unfixed_deferred_sets))
    -> Res = impossible % we do not compute PosGuard1,NegGuard2 in this case: otherwise this would mean that Operation 1 can never fire !
    ; get_conj_inv_predicate([PosGuard1,NegGuard2],UseInvariant,Pred2),
    solve_predicate_with_chr(Pred2,_State2,TimeoutFactor,[],RR2),
    combine_simult_result(RR,RR2,Res))
    ; print('********* ERROR ***********'),nl,fail).

solve_predicate_with_chr(Pred,State,TimeoutFactor,Options,RR) :-
    solve_predicate(Pred,State,TimeoutFactor,['CHR','CLPFD','SMT'|Options],RR).

syntactical_independence(Reads1,Writes1,Reads2,Writes2) :-
    \+ vars_ord_intersect(Writes1,Reads2), % op1 does not modify guard/effect of op2
    \+ vars_ord_intersect(Writes2,Reads1), % op2 does not modify guard/effect of op1
    \+ vars_ord_intersect(Writes1,Writes2). % no race condition

tcltk_cbc_cfg_analysis(list([list(['Origin'|SOps])|Result])) :-
    findall(Op, b_top_level_operation(Op), Ops), sort(Ops,SOps),
    findall(list([OpName1|EnableList]),
    (b_get_sorted_op(OpName1),
    findall(Possible,cbc_quick_cfg_analysis(OpName1,_OpName2,Possible),EnableList)),
    Result),
    print_enable_table([list(['Origin'|Ops])|Result]).

tcltk_cbc_dependence_analysis(list([list(['Origin'|SOps])|Result])) :-
    %findall(Op, b_get_machine_operation(Op,_,_,_), Ops), sort(Ops,SOps),
    findall(Op, b_top_level_operation(Op), Ops), sort(Ops,SOps),
    findall(list([OpName1|EnableList]),
    (b_get_sorted_op(OpName1),
    findall(Enable,cbc_dependence_analysis(OpName1,_OpName2,Enable),EnableList)),
    Result).

tcltk_cbc_enabling_analysis(L) :-
    get_time_out_preference_with_factor(0.1,TOF),
    (TOF > 250 -> ExtraTO is TOF-250 ; ExtraTO = 0),
    tcltk_cbc_enabling_analysis(ExtraTO,L).

tcltk_cbc_enabling_analysis(ExtraTimeout,list([list(['Origin'|Ops])|Result])) :-
    findall(Op, b_top_level_operation(Op), Ops),
    %statistics(walltime,[WT1,_]),
    findall(list([OpName1|EnableList]),
    (init_or_op(OpName1),
    findall(Enable,cbc_enable_analysis(OpName1,_OpName2,Enable,ExtraTimeout),EnableList)),
    Result).

tcltk_cbc_enabling_relations_after_operation(OpName1,ExtraTimeout,
    list([list(['Event','Enable','KeepEnabled','Disable','KeepDisabled'])|Results])) :-
    findall(list([OpName2|ResOp2]),
    compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,ResOp2), Results).

tcltk_cbc_enabling_relations_for_operation(OpName2,ExtraTimeout,
    list([list(['Event','Enable','KeepEnabled','Disable','KeepDisabled'])|Results])) :-
    findall(list([OpName1|ResOp2]),
    compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,ResOp2), Results).

tcltk_cbc_simultaneous_enabling_analysis(list([list(['Origin'|SOps])|Result])) :-
    findall(Op, b_top_level_operation(Op), Ops),
    sort(Ops,SOps), % sort operations to ensure nice triangular display
    statistics(walltime,[WT1,_]),
    findall(list([OpName1|EnableList]),
    (member(OpName1,SOps),
    findall(SimulRes,tcltk_simult(OpName1,SOps,SimulRes),EnableList)),
    Result),
    statistics(walltime,[WT2,_]), Time is WT2-WT1,
    formatsilent('Runtime for simultaneous enabling analysis: ~w ms~n',[Time])
. %,print_enable_table([list(['Origin'|Ops])|Result]).

tcltk_dot_cfg_analysis(File) :-
    gen_dot_graph(File,eop_node_predicate,cfg_trans_predicate).

tcltk_simult(Op1,SOps,Res) :- member(Op2,SOps),tcltk_simult2(Op1,Op2,Res).

tcltk_simult2(Op1,Op2,Res) :-
    Op1 = Op2, % Op2 @=< Op1, % the simultaneous impossible analysis is symmetric: TO DO: do not compute/display info twice
    !,
    Res = '-'.

tcltk_simult2(Op1,Op2,TRes) :-
    simult_enable_analysis(Op1,Op2,1,fixed_time_out(150),TRes).

translate_enable_info(timeout,unknown).

translate_enable_info(time_out,unknown).

translate_enable_info(overflow,unknown).

translate_enable_info(virtual_time_out,unknown).

translate_enable_res(Rel,_,_,'impossible',red,_) :- impossible(Rel),!, fail.

translate_enable_res(guaranteed,_,_,'guaranteed',olivedrab2,solid) :- !.

translate_enable_res(Rel,X,Y,TransRel,TCol,bold) :- independent(Rel,Col),
    !,X=Y, % only show if source & dest identical
    TransRel=Rel,TCol=Col.

translate_enable_res(possible,_,_,'possible',black,solid) :- !.

translate_enable_res(keep,_,_,'keep',lightgray,solid) :- !.

translate_enable_res(possible_enable,_,_,'(enable)',black,solid) :- !.

translate_enable_res(possible_disable,_,_,'(disable)',lightblue,solid) :- !.

translate_enable_res(timeout_keep,_,_,'keep?',tomato,dashed) :- !.

translate_enable_res(timeout_possible,_,_,'possible?',tomato,dashed) :- !.

translate_enable_res(timeout_possible_disable,_,_,'(disable?)',tomato,dashed) :- !.

translate_enable_res(timeout_possible_enable,_,_,'(enable?)',tomato,dashed) :- !.

translate_enable_res(pred(Expr),_,_,String,black,dashed) :- !,
    translate_bexpression(Expr,String).

translate_enable_res(predicate(Expr),_,_,String,black,dashed) :- !,
    translate_bexpression(Expr,String).

translate_enable_res(dependent,_,_,dependent,green,solid) :- !.

translate_enable_res(race_dependent,_,_,race_dependent,green,solid) :- !.

translate_enable_res(guard_dependent,_,_,guard_dependent,olive,dashed) :- !.

translate_enable_res(action_dependent,_,_,action_dependent,green,dashed) :- !.

translate_enable_res(X,_,_,'independent',lightgray,solid) :-
    memberchk(X,[independent,syntactic_independent,syntactic_fully_independent,syntactic_unchanged]),!.

translate_enable_res(X,_,_,X,red,solid).

translate_res(cannot_enable,_,_,_,_,_) :- !, fail.

translate_res(syntactic_independent,X,Y,'independent',yellow,bold) :- !,X=Y. % only show if source & dest identical

translate_res(race_dependent,X,Y,'race_independent',lightgray,bold) :- !,X=Y. % only show if source & dest identical

translate_res(possible,_,_,'',black,solid) :- !.

translate_res(timeout_possible,_,_,'',tomato,solid) :- !.

translate_res(X,_,_,X,red,dashed).