refinement_checker

accepting_state(_,From) :- node_satisfies_goal(From). % look for GF GOAL

add_all_predeterministic_transitions_fail_loop(CurState,CurClosure,CheckDIV,RootNode) :-
    specify_possible_transition(CurState,CurClosure,Action,SuccClosure,CheckDIV,RootNode),
    add_predeterministic_transitions(CurState,CurClosure,Action,SuccClosure,_SuccState),fail.

add_all_predeterministic_transitions_fail_loop(_NewRootNode,_Closure,_CheckDIV,_RootNode).

add_id_to_stack(NewNodeId) :-
    asserta(not_all_det_transitions_added(NewNodeId)).

add_predeterministic_transitions(CurState,CurClosure,Action,SuccClosure,NextState) :-
    (ord_seteq(CurClosure,SuccClosure) ->
    (\+transition(CurState,Action,_TransID,CurState) ->
    assertz(transition(CurState,Action,no_id,CurState)),
    debug_println(9,transition(CurState,Action,pred1,CurState))
    ; true % do not add any transition
    )
    ;
    (predet_node_presentation(NextState,SuccClosure) -> % state already added to state space of the pre-deterministic refinement P'
    assertz(transition(CurState,Action,no_id,NextState)),
    debug_println(9,transition(CurState,Action,pred2,NextState))
    ;
    get_predeterministic_node_id1(NextState),
    assertz(transition(CurState,Action,no_id,NextState)),
    debug_println(9,transition(CurState,Action,pred3,NextState)),
    assertz(predet_node_presentation(NextState,SuccClosure)),
    add_id_to_stack(NextState)
)
).

assert_inner_visited(From,NBA) :- assertz(inner_visited(From,NBA)).

assert_outer_visited(From,NBA) :- assertz(outer_visited(From,NBA)).

b_nba_transition(FromB,FromNBA,ActionID,ToB,ToNBA) :-
    impl_trans_id(FromB,Term1,ActionID,ToB),
    nba_trans(FromNBA,Term1,ToB,ToNBA).

check_go_step_refusal(Action,RefusedSet,NextXState,YList,NTX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel) :-
    (setof(Y2,spec_par_trans_bullet(YList,RefusedSet,Action,Y2),YS) ->
    append(TraceY,[refuse(RefusedSet),go(Action,_)],NTY),
    spec_tau_closure(YS,YTS,failures),
    not_refusals(NextXState,YTS,NTX,NTY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel)
    ;
    RefusalTraceX=NTX,
    findall(AA,(spec_stable_par_trans(YList,AA,_),AA\=tau),YListChoices),
    remove_dups(YListChoices,YEnabledList),
    get_refused_set(YEnabledList,YRefusedSet),
    append(TraceY,[refuse(YRefusedSet)],RefusalTraceY)
).

check_valid_failures_model(FailuresModel,ShortCut) :-
    (valid_failures_model(FailuresModel,S) -> ShortCut=S
    ; ShortCut='T',
    add_warning(refinement_checker,'Invalid failures model: ',FailuresModel)
).

comb_div(div,_,div).

comb_div(no_div,D,D).

comp_dest_tau_clos([],CLOS,CLOS,DIV,DIV).

comp_dest_tau_clos([Dest|T],CLOS_sofar,CLOS_RES,DIV_sofar,DIVRES) :-
    ((tau_visited(Dest,PriorList), /* we have seen the node before */
    \+ tau_closure(Dest,_,_,_)) /* its treatment is not complete; i.e., we have a loop */
    -> /* we have divergence */
    % print(tau_loop(Dest,PriorList)),nl,
    % ord_union([Dest],CLOS_sofar,CLOS_RES) % Dest already in closure
    DIV_sofar2=div,
    (PriorList=[] -> CLOS_sofar2=CLOS_sofar
    ; /* we did not add all successors of Dest yet */
    retract(tau_visited(Dest,_)),
    assertz(tau_visited(Dest,[])),
    assertz(tau_loop_back_node(Dest)),
    findall(To,tau_transition(Dest,_,To),AllDestSuccs),
    sort([Dest|AllDestSuccs],SADS), % also add Dest; it was not yet added ?? <------- TODO: check
    ord_subtract(SADS,PriorList,DestIgnored),
    % print(adding_ignored_succs(Dest,DestIgnored)),nl,
    comp_dest_tau_clos(DestIgnored,CLOS_sofar,CLOS_sofar2,div,_)
    ),
    comp_dest_tau_clos(T,CLOS_sofar2,CLOS_RES,DIV_sofar2,DIVRES)
    ; get_tau_closure2(Dest,DClos,_DStable,DIV),
    comb_div(DIV,DIV_sofar,DIV_sofar2),
    ord_union(CLOS_sofar,DClos,CLOS_sofar2), % combine states reachable via tau
    comp_dest_tau_clos(T,CLOS_sofar2,CLOS_RES,DIV_sofar2,DIVRES)).

compute_predeterministic_process(RootNode,NewRootNode,ModelStyle) :-
    generated_predeterministic_refinement(RootNode,ModelStyle,NewRootNode),
    debug_println(9,'%%%% Pre-deterministic Refinement P\' has been already generated.'),!.

compute_predeterministic_process(RootNode,NewRootNode,ModelStyle) :-
    (ModelStyle = failure_divergences -> CheckDIV=true; CheckDIV=false),
    get_tau_loop_closure1(RootNode,Closure,false),
    get_predeterministic_node_id1(NewRootNode),
    assertz(predet_node_presentation(NewRootNode,Closure)),
    debug_println(9,tau_closure(NewRootNode,Closure)),
    add_id_to_stack(NewRootNode),
    generate_predeterministic_process_state_space(NewRootNode,CheckDIV),
    assertz(generated_predeterministic_refinement(RootNode,ModelStyle,NewRootNode)).

compute_tau_closure(State,Closure,Stable,DIV) :-
    (tau_priority_transition(State,Span,_)
    -> Prio = prio, findall(To,tau_priority_transition(State,Span,To),Dest), sort(Dest,SDest),
    assertz(tau_visited(State,SDest)) % remember that we did not inspect all tau successors, only Dest
    ; Prio = all, findall(To,tau_transition(State,_,To),Dest),
    assertz(tau_visited(State,[]))
    ),
    %print(visiting(State,Dest,Prio)),nl,
    (Dest=[]
    -> /* stable state */
    DivOccurred = no_div, TauClosure=[State],
    DStable = stable
    ; /* unstable state */
    sort(Dest,SDest),
    comp_dest_tau_clos(SDest,[],DestTauClosure,no_div,DivOccurred),
    (((DivOccurred=no_div ; \+ tau_loop_back_node(State)),
    Prio=prio)
    -> DStable = unstable_prio(SDest), % it is safe to only treat the priority tau transitions in this node
    TauClosure = DestTauClosure % also: we do not need to add this node to the tau-closure
    ; DStable = unstable,
    ord_union([State],DestTauClosure,TauClosure) % also add node itself
    )
    ),
    assertz(tau_closure(State,TauClosure,DStable,DivOccurred)),
    Closure=TauClosure, DIV=DivOccurred, Stable=DStable.

compute_tau_scc(State,RootState,LoopVisited,SCC,SCCRes,Test) :-
    \+memberchk(State,LoopVisited),
    \+memberchk(State,SCC),
    impl_trans_test(Test,State,tau,Succ),
    (Succ=RootState ->
    SCCRes=[State|SCC]
    ;
    compute_tau_scc(Succ,RootState,LoopVisited,[State|SCC],SCCRes,Test)
).

compute_tau_scc(RootState,RootState,_LoopVisited,_SCC,[RootState],_Test).

convert_to_csp_event(Event,CSPEvent) :- split_atom(Event, ['(',',',')'], DotEls),ajoin_with_sep(DotEls,'.',CSPEvent).

cycle_check(From,NBA,[],From,NBA) :- !. % Loop found

cycle_check(From,NBA,_,_,_) :- inner_visited(From,NBA),!,fail. % already explored

cycle_check(From,NBA,[ActionID|TLoop],TargetB,TargetNBA) :- assert_inner_visited(From,NBA),
    % format('Looking for cycle from ~w to target ~w : ~w~n',[From,TargetB,TargetNBA]),
    b_nba_transition(From,NBA,ActionID,ToB,ToNBA),
    cycle_check(ToB,ToNBA,TLoop,TargetB,TargetNBA).

deadlock_check(X,ModelStyle,Trace) :- DLK=true,
    (ModelStyle=failure_divergences -> DIV=true ;
    ModelStyle=trace -> add_error(deadlock_check,'Trace model cannot be used for deadlock checking'), DIV=false
    ; DIV=false),
    dfs_check(X,Trace,DLK,DIV).

det_check(X,TraceX,TraceY,YEnabledList,ModelStyle) :-
    reset_all_dynamic_state_predicates_for_determinism_check,
    cputime(T1),
    assertz(cur_det_id(X)),
    % computing the pre-deterministic refinement P' of P
    compute_predeterministic_process(X,PredRootId,ModelStyle),
    cputime(T2),
    %tcltk_interface: add_new_visited_expression(PredRootId,_Hash,[],root,off),
    spec_tau_closure([PredRootId],InitialsRootId,failures),
    ( ModelStyle=failure_divergences,determinism_check_div_found(PredRootId) ->
    dfs_search(PredRootId,false,true,TraceX),cputime(T3),print_state_from_id(X),
    print(' reaches a divergence.'),nl,
    print(TraceX),nl,TraceY=TraceX
    % after computing P' we check wheter P' is refinement of P: P' [F= P
    % if P' [F= P is true we proved that P is deterministic, otherwise P is not deterministic
    ;not_refines(X,InitialsRootId,TraceX,TraceY,YEnabledList,ModelStyle) ->
    cputime(T3),print_state_from_id(X), print(' reaches a '), print('non deterministic choice'),nl,
    print(TraceX),nl
    ; cputime(T3),print_state_from_id(X),print(' is '),print('deterministic'),nl,TraceX=no_counter_example
    ),
    printsilent('% Generating P\' Time : '), D1 is T2-T1, printsilent(D1), printsilent(' ms'),nls,
    printsilent('% Checking P\' [F= P Time: '), D2 is T3-T2, printsilent(D2), printsilent(' ms'),nls,
    printsilent('% Overall Checking Time: '), D is T3-T1, printsilent(D), printsilent(' ms'),nls.

deterministic_check(X,ModelStyle,ResTrace) :-
    det_check(X,TraceX,TraceY,YEnabledList,ModelStyle),
    (TraceX==no_counter_example
    -> ResTrace=no_counter_example %,print_message('No refinement counter example found') used to be all return value
    ; inst_list(TraceX,ResTrace0),
    inst_list(TraceY,ResTrace1), /* convert pending free var into [] + go */
    tcltk_execute_string_trace(X,TraceX),
    append(ResTrace0,[' At_last_step_specification_can_do_one_of:'|YEnabledList],ResTraceX),
    append(ResTraceX,[' Trace_of_the_left_specification:'|ResTrace1],ResTrace)
).

dfs_check(X,ResTrace,DLK,DIV) :-
    retractall(dvisited(_)), retractall(tau_closure(_,_,_,_)),retractall(dincomplete),
    cputime(T1),
    (dfs_search(X,DLK,DIV,Trace1) ->
    cputime(T2),print_state_from_id(X), print(' reaches a '), printDD(DLK,DIV),nl,
    printsilent(Trace1),nls,
    inst_list(Trace1,ResTrace),
    tcltk_execute_string_trace(X,Trace1)
    ; dincomplete -> cputime(T2),print('No '),printDD(DLK,DIV), print('found so far for :'),
    print_state_from_id(X),nl, ResTrace=none_so_far
    ; cputime(T2),print_state_from_id(X), print(' is '),printDD(DLK,DIV), print('free'),nl,ResTrace=no_counter_example
    ),
    (silent_mode(on) -> true ; print('% Checking Time: '), D is T2-T1, print(D), print(' ms'),nl).

dfs_search(X,_,_DIV,_) :- dvisited(X),!, %print(already_visited(X)),nl,
    % (DIV\=true, TO DO: check that we have not ignored tau or visible transitions in this loop)
    fail.

dfs_search(X,DLK,_,[deadlocks]) :- DLK=true,\+ impl_trans_term(X,_,_),!, % will compute transitions if necessary
    (not_all_transitions_added(X) -> (dincomplete -> assertz(dincomplete),fail) ; true).

dfs_search(X,DLK,DIV,Result) :-
    get_tau_closure(X,Closure,Stable,Diverges),
    assertz(dvisited(X)),
    (DIV=true, Diverges=div
    -> Result = [diverges], debug_println(19,diverges(X,Closure))
    ; Stable=unstable_prio(Dest) -> /* only perform the first priority tau transitions */
    Result=[go(tau,Y)|R2],
    member(Y,Dest), dfs_search(Y,DLK,DIV,R2)
    ; % Stable=[X] ->
    Result=[go(A,Y)|R2], impl_trans(X,A,Y), dfs_search(Y,DLK,DIV,R2)
% ; Result=[go(tau,Y)|R2], member(Y,Stable), dfs_search(Y,DLK,DIV,R2)
).

divergence_check(X,Trace) :- DLK=false,DIV=true,dfs_check(X,Trace,DLK,DIV).

do_one_trace_step_ahead(X,YList,TraceX,TraceY,YEnabledList,FailuresModel) :-
    TraceX = [go(A,X2)|TX],
    impl_trans(X,A,X2),
    (A = tau
    -> not_refines(X2,YList,TX,TraceY,YEnabledList,FailuresModel)
    ; (setof(Y2,spec_par_trans(YList,A,Y2),YS)
    -> TraceY = [go(A,_)|TY],
    spec_tau_closure(YS,YTS,FailuresModel), % diamond compression of the LTS of the Spec process
    not_refines(X2,YTS,TX,TY,YEnabledList,FailuresModel)
    ; findall(AA,(spec_par_trans(YList,AA,_),AA\=tau),YListChoices), /* no transition: refinement false */
    remove_dups(YListChoices,YEnabledList) % do we need to remove duplicated enabled actions here?
)
).

execute_string_trace_to_node([]) :- !.

execute_string_trace_to_node([spec_cannot_diverge|T]) :- !, execute_string_trace_to_node(T).

execute_string_trace_to_node([deadlocks|T]) :- !, execute_string_trace_to_node(T).

execute_string_trace_to_node([diverges|T]) :-
    current_state_id(CurID),
    find_tau_trace_to(CurID,divergence,NewTrace,T),!,
    execute_string_trace_to_node(NewTrace).

execute_string_trace_to_node([not_enabled(_)|T]) :- !, execute_string_trace_to_node(T).

execute_string_trace_to_node([cannot_refuse_compl(_)|T]) :- !, execute_string_trace_to_node(T).

execute_string_trace_to_node([cannot_refuse(_)|T]) :- !, execute_string_trace_to_node(T).

execute_string_trace_to_node([refuse(_)|T]) :- !, execute_string_trace_to_node(T).

execute_string_trace_to_node([go('$initialise_machine',ID)|T]) :-
    current_state_id(CurID),
    transition(CurID,Action,ID),
    functor(Action,'$initialise_machine',_),!,
    tcltk_interface:tcltk_perform_action(Action,ID),
    execute_string_trace_to_node(T).

execute_string_trace_to_node([go('$initialise_machine',ID)|T]) :-
    /* special case for CurID=root, as setup_constants get merged
    into initialise_machine by refinement checker */
    current_state_id(CurID), CurID=root,
    transition(CurID,Action1,ID1),
    functor(Action1,'$setup_constants',_),
    transition(ID1,Action2,ID),
    functor(Action2,'$initialise_machine',_),!,
    tcltk_interface:tcltk_perform_action(Action1,ID1),
    tcltk_interface:tcltk_perform_action(Action2,ID),
    execute_string_trace_to_node(T).

execute_string_trace_to_node([go('$initialise_machine',ID)|T]) :-
    current_state_id(root),
    transition(root,start_cspm_MAIN,ID),!,
    tcltk_interface:tcltk_perform_action(start_cspm_MAIN,ID),
    execute_string_trace_to_node(T).

execute_string_trace_to_node([go('$setup_constants',ID)|T]) :-
    current_state_id(CurID),
    transition(CurID,Action,ID),
    functor(Action,'$setup_constants',_),!,
    tcltk_interface:tcltk_perform_action(Action,ID),
    execute_string_trace_to_node(T).

execute_string_trace_to_node([go(tau,DestID)|T]) :- % could now be multiple taus ! adapt
    current_state_id(CurID),
    find_tau_trace_to(CurID,DestID,NewTrace,T),!,
    execute_string_trace_to_node(NewTrace).

execute_string_trace_to_node([go(tau_direct,ID)|T]) :-
    current_state_id(CurID),
    tau_transition(CurID,Action,ID),!,
    tcltk_interface:tcltk_perform_action(Action,ID),
    execute_string_trace_to_node(T).

execute_string_trace_to_node([go(Action,ID)|T]) :- /* <---- Node ID's have to be added to avoid problems !! */
    current_state_id(CurID),
    transition(CurID,Ev,TransitionId,ID),
    translate_event(Ev,Action),
    tcltk_interface:tcltk_perform_action(CurID,Action,TransitionId,ID),!,
    execute_string_trace_to_node(T).

execute_string_trace_to_node([go(Action,ID)|_T]) :- silent_mode(off),
    current_state_id(CurID),
    format('Could not replay event ~w (reaching state id ~w) in state ~w~n',[Action,ID,CurID]),
    debug_mode(on),
    current_expression(CurID,State),
    print(current_expression(CurID,State)),nl,
    fail.

find_failure_abstraction([AbsState|_T],AllXActions) :-
    spec_stable(AbsState),
    spec_all_possible_actions(AbsState,AllAbsActions),
    % note: we can use ord_subset as setof returns sorted lists
    ord_subset(AllAbsActions,AllXActions),!.% we have found an abstract state whose failures is a superset of X's failures

find_failure_abstraction([_|T],AllXActions) :-
    find_failure_abstraction(T,AllXActions).

find_tau_trace_to(CurID,DestID,Trace,TraceTail) :- retractall(tau_trace_visited(_)),
    find_tau_trace_to_aux(CurID,DestID,Trace,TraceTail).

find_tau_trace_to_aux(CurID,DestID,T,Tail) :-
    tau_trace_visited(CurID),!,DestID=divergence,T=Tail.

find_tau_trace_to_aux(CurID,ID,T,Tail) :- ID=CurID,!,T=Tail.

find_tau_trace_to_aux(CurID,ID,[go(tau_direct,ID2)|T],Tail) :- assertz(tau_trace_visited(CurID)),
    tau_transition(CurID,_,ID2),
    find_tau_trace_to_aux(ID2,ID,T,Tail).

generate_predeterministic_process_state_space(RootNode,CheckDIV) :-
    % in case we found div state and we check for divergence as well then
    % do not explore the pre-deterministic state space any more.
    (CheckDIV=true,determinism_check_div_found(RootNode) -> fail; true),
    % otherwise explore the pre-deterministic state space until stack is empty
    pop_id_from_stack(NodeId),!,
    predet_node_presentation(NodeId,Closure), % tau loop closure already explored
    add_all_predeterministic_transitions_fail_loop(NodeId,Closure,CheckDIV,RootNode),
    debug_println(9,tau_closure(NodeId,Closure)),
    generate_predeterministic_process_state_space(RootNode,CheckDIV).

generate_predeterministic_process_state_space(_RootNode,_CheckDIV).

get_max_tau_loop_closure([],_LV,Closure,Closure,_Test).

get_max_tau_loop_closure(Waiting,LoopVisited,Closure_so_far,MaxClosure,Test) :-
    Waiting=[State|Rest],
    (\+member(State,LoopVisited) ->
    get_tau_loop_closure(State,Closure,LoopVisited,Test),
    ord_add_element(LoopVisited, State, LoopVisited1),
    ord_union(Closure_so_far,Closure,Closure1),
    ord_intersection(LoopVisited1,Closure1,Visited,NewToClosure),
    ord_union(NewToClosure,Rest,Waiting2),
    ord_intersection(Visited,Waiting2,_Inter,Waiting1)
    ;
    Waiting1=Rest,LoopVisited1=LoopVisited,Closure1=Closure_so_far
    ),
    get_max_tau_loop_closure(Waiting1,LoopVisited1,Closure1,MaxClosure,Test).

get_predeterministic_node_id1(NewId) :-
    cur_det_id(ID),
    ID1 is ID + 1,
    gensym('det',NewId),
    retract(cur_det_id(ID)),
    assertz(cur_det_id(ID1)).

get_reduced_refused_set(_,RefusedSet) :- animation_mode(b),!,
    RefusedSet = ['$UNKNOWN']. % TODO: get all operations at list and build complement ??

get_reduced_refused_set(AllXActions,ReducedRefuseSet) :-
    get_refused_set3(AllXActions,Closure,RefusedSet),
    reduce_channel_set(RefusedSet,Closure,ReducedRefuseSet).

get_refused_set(_,RefusedSet) :- animation_mode(b),!,
    RefusedSet = ['$UNKNOWN'].

get_refused_set(AllXActions,RefusedSet) :-
    get_refused_set3(AllXActions,_,RefusedSet).

get_refused_set3(AllXActions,R,RefusedSet) :-
    evaluate_argument('Events',R),
    expand_symbolic_set(R,R1,_C),
    (csp_with_bz_mode ->
    l_translate_csp_b_event(AllXActions,AllXActionsNew),
    l_translate_csp_b_event(R1,R2)
    ; AllXActionsNew=AllXActions,
    R2=R1
    ),
    return_csp_closure_value(R2,AllPossibleEvents),
    list_to_ord_set(AllPossibleEvents,AllEventsSet),
    list_to_ord_set(AllXActionsNew,AllXActionsSet),
    ord_subtract(AllEventsSet,AllXActionsSet,RefusedSet).

get_tau_closure(State,Closure,Stable,DIV) :- tau_closure(State,C,S,D),!,Closure=C, Stable=S,DIV=D.

get_tau_closure(State,Closure,Stable,DIV) :- retractall(tau_visited(_,_)),
    compute_tau_closure(State,Closure,Stable,DIV).

get_tau_closure2(State,Closure,Stable,DIV) :- tau_closure(State,C,S,D),!,Closure=C, Stable=S,DIV=D.

get_tau_closure2(State,Closure,Stable,DIV) :- compute_tau_closure(State,Closure,Stable,DIV).

get_tau_loop_closure(State,Closure,LoopVisited,Test) :-
    setof(SCC,compute_tau_scc(State,State,LoopVisited,[],SCC,Test),SCCs),
    append(SCCs,Closure1),
    list_to_ord_set(Closure1,Closure).

get_tau_loop_closure1(State,Closure,Test) :-
    get_max_tau_loop_closure([State],[],[],Closure,Test).

get_visible_transition(State,Closure,Action,SuccNode) :-
    %random_select(Node,Closure,_Rest),
    random_permutation(Closure,Closure1),!,
    member(Node,Closure1),
    impl_trans(Node,Action,SuccNode),
    Action\=tau,
    % adding only one visible transition to the pre-deterministic state
    \+transition(State,Action,_TransID,_CurState).

impl_all_possible_actions(State,ActionList) :-
    (setof(A,NState^impl_trans(State,A,NState),ActionList) -> true ; ActionList=[]).

impl_diverges(State) :- get_tau_closure(State,_,_,div).

impl_non_tau_trans(X,A,X2) :-
    impl_trans(X,A,X2),
    A\=tau.

impl_stable(State) :-
    get_tau_closure(State,_,stable,_).

impl_tau_transition_from_closure(Closure,SuccNode) :-
    %random_select(Node,Closure,_Rest), % random_select inserts a cut after unifying Node
    random_permutation(Closure,Closure1),!,
    member(Node,Closure1),
    impl_trans(Node,tau,SuccNode),
    \+memberchk(SuccNode,Closure).

impl_trans(From,Label,To) :- /* need to improve efficiency of that : */
    impl_trans_term(From,Action1,To1),
    (functor(Action1,'$setup_constants',_)
    -> impl_trans(To1,Label,To)
    ; ref_generate_label(Action1,Label), To=To1 % for in-situ refinement we do not need the overhead of this !
).

impl_trans_cspb(From,Label,To) :-
    impl_trans(From,X,To),translate_csp_b_event(X,X1),
    % print(translated_event(X1)),nl,
    (var(Label) -> Label=X
    ; translate_csp_b_event(Label,Label1),X1==Label1).

impl_trans_test(IsTestCase,From,Label,To) :-
    (IsTestCase=true -> test_transition(From,Label,To) ; impl_trans(From,Label,To)).

in_situ_model_check(SpecNodeID,ResTrace,Type,ModelStyle,MaxNrOfNewNodes) :-
    set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes),
    interruptable_perform_mc(Type,ModelStyle,SpecNodeID,ResTrace).

in_situ_ref_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes) :-
    % TO DO: redirect spec_trans,... to impl_trans ....
    % retractall(spec_trans(_,_,_)),
    % assertz((spec_trans(From,Label,To) :- impl_trans(From,Label,To))),
    interruptable_refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes).

initial_nba_state(1).

inst_list([],R) :- !,R=[].

inst_list([go(tau_direct,_ID)|T],['GO:',tau|IT]) :- !, inst_list(T,IT). % NOTE : can be multiple taus now

inst_list([go(Op,_ID)|T],['GO:',Op|IT]) :- csp_mode,!, inst_list(T,IT).

inst_list([go(Op,_ID)|T],[Op|IT]) :- !, inst_list(T,IT).

inst_list([spec_cannot_diverge|T],['DIVERGES'|IT]) :- !, inst_list(T,IT).

inst_list([diverges|T],['DIVERGES'|IT]) :- !, inst_list(T,IT).

inst_list([deadlocks|T],['DEADLOCKS'|IT]) :- !, inst_list(T,IT).

inst_list([not_enabled(Op)|T],['NOT_ENABLED:',Op|IT]) :- !,inst_list(T,IT).

inst_list([determ(Op1,_ID1,Op2,_ID2)|T],['DETERMINISM_BY_EVENT:',Op1,Op2|IT]) :- !,inst_list(T,IT).

inst_list([cannot_refuse_compl(Ops)|T],Res) :-
    append(['CANNOT_REFUSE_COMPL:'|Ops],IT,Res),
    inst_list(T,IT).

inst_list([cannot_refuse(Ops)|T],Res) :-
    append(['CANNOT_REFUSE:'|Ops],IT,Res),
    inst_list(T,IT).

inst_list([refuse('Sigma')|T],Res) :-
    append(['REFUSED_SET:','Sigma'],IT,Res),
    inst_list(T,IT).

inst_list([refuse(bullet)|T],Res) :-
    append(['REFUSED_SET:',bullet],IT,Res),
    inst_list(T,IT).

inst_list([refuse(Ops)|T],Res) :-
    append(['REFUSED_SET:'|Ops],IT,Res),
    inst_list(T,IT).

interruptable_perform_mc(Type,ModelStyle,SpecNodeID,ResTrace) :-
    evaluate_argument('Events',R),
    (is_not_infinite_type(R) -> true; assertz(haskell_csp:ignore_infinite_datatypes)),
    user_interruptable_call_det(catch_interrupt_assertion_call(
    refinement_checker: perform_mc(Type,ModelStyle,SpecNodeID,ResTrace)),InterruptResult),
    (InterruptResult=interrupted -> ResTrace=[interrupted], print('Assertion check was interrupted by user!!!'),nl
    ; printsilent('Assertion check completed.'),nls),
    retractall(haskell_csp:ignore_infinite_datatypes).

interruptable_refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes) :-
    user_interruptable_call_det(catch_interrupt_assertion_call(refinement_checker: refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes)),InterruptResult),
    (InterruptResult=interrupted -> ResTrace=[interrupted], print("Refinement check was interrupted by user!!!"),nl
    ;(real_error_occurred ->
    print_error('% *** Errors occurred while refinement checking ! ***'),nl,nl,fail
    ; printsilent('Refinement check completed.'),nls
)
).

l_translate_csp_b_event([],[]).

l_translate_csp_b_event([Event|T],[TEvent|R]) :- translate_csp_b_event(Event,TEvent),l_translate_csp_b_event(T,R).

nba_trans(1,_,_,1). % :- print(A),nl.

nested_dfs_cycle_check(Prefix,State,Loop) :-
    reset_nfs,
    start_ms_timer(T1),
    initial_nba_state(NBAInit),
    (reachable_cycle(root,NBAInit,Prefix,State,Loop)
    ->
    stop_ms_timer_with_msg(T1,'Nested-DFS found cycle'),
    print_state_from_id(State), print(' satisfies GOAL and can be executed infinitely often '),nl,
    printsilent('Path to state: '),printsilent(Prefix),nls,
    printsilent('Loop: '),printsilent(Loop),nls,
    (minimize_lasso(Prefix,Loop,NP,NL), append(NP,NL,Trace),
    set_counterexample_by_transition_ids(Trace)
    -> true ; add_error(nested_dfs_cycle_check,'Could not set counter example:',Prefix))
    ;
    stop_ms_timer_with_msg(T1,'Nested-DFS found no cycle'),
    format('No infinite loop with state statisfying GOAL found~n',[]),fail
).

not_failure_refines(singleton_failures,X,YList,[not_enabled(A)|_T]) :- % Singleton Failures
    spec_trans_all(YList,A),
    \+(impl_trans(X,A,_)), /* TO DO: handle tau for CSP */
    print_message(cannot_do(A)).

not_failure_refines(failures,X,YList,[cannot_refuse_compl(AllXActions),cannot_refuse(ReducedRefuseSet)|_T]) :-
    % CSP Failures
    impl_stable(X), % only need to check if X is stable
    impl_all_possible_actions(X,AllXActions),
    \+ find_failure_abstraction(YList,AllXActions), % if satisfied => an X action can be refused at the current state of Y
    % note: we can use ord_subset since setof returns sorted lists
    get_reduced_refused_set(AllXActions,ReducedRefuseSet),
    debug_println(19,cannot_refuse_compl(AllXActions)),
    debug_println(19,cannot_refuse(ReducedRefuseSet)).

not_failure_refines(failure_divergences,X,YList,T) :-
    (not_failure_refines(failures,X,YList,T)
    -> true /* not we have already checked for divergence in YList in not_refines */
    ; impl_diverges(X), T=[spec_cannot_diverge|_T]).

not_refines(X,Y,Tr,_,_YEnabled,_) :- % print_message(nr(X,Y,Tr)),
    % the configuration is already in the memo table: do not look for a counter-example here
    not_refines_table(X,Y,Tr),!,fail.

not_refines(X,YList,TraceX,_,_,_) :-
    assertz(not_refines_table(X,YList,TraceX)), % add to memo table
    YList=[X|_],csp_mode,!,fail. % simple check if X appears in the list; if so we will never find a counter example; we could do a full member check (but not sure about performance)

not_refines(_X,YList,_TraceX,_TraceY,_YEnabled,_) :-
    \+(spec_completely_explored),
    spec_list_contains_unexplored_node(YList),!, %YEnabled=['$unknown'],
    fail.

not_refines(X,YList,TraceX,_TraceY,YEnabledList,FailuresModel) :- /* use failure refinement */
    not_failure_refines(FailuresModel,X,YList,TraceX),
    findall(AA,spec_par_trans(YList,AA,_),YEnabledList).

not_refines(X,YList,TraceX,TraceY,YEnabledList,FailuresModel) :-
    get_tau_closure(X,_Closure,Stable,_Diverges),
    Stable=unstable_prio(Dest),!, % only perform tau priority action
    TraceX = [go(tau,X2)|TX], member(X2,Dest),
    not_refines(X2,YList,TX,TraceY,YEnabledList,FailuresModel).

not_refines(X,YList,TraceX,TraceY,YEnabledList,FailuresModel) :-
    do_one_trace_step_ahead(X,YList,TraceX,TraceY,YEnabledList,FailuresModel).