ctl

combine_result(false,false,R) :- !,R=false.

combine_result(incomplete,_,R) :- !,R=incomplete.

combine_result(_,incomplete,R) :- !,R=incomplete.

combine_result(_,_,computing).

convert_ctl_trace(Proc,Ctl,Mode,UseTransitionIDs,Trace,CE) :-
    expand_trace(Trace,Result),
    %% convert_ctl_trace1(ETrace,Result),
    (ctl_counter_examples_cache(Proc,Ctl,Mode,_) -> true; assertz(ctl_counter_examples_cache(Proc,Ctl,Mode,Result))),
    (UseTransitionIDs = true -> get_event_trace_transitions(Mode,Result,EventTrace)
    ; get_event_trace(Result,EventTrace)),
    CE=ce(EventTrace).

ctl_model_check(Formula,MaxNodes,Mode,Res) :-
    (temporal_parser(Formula,ctl,Ctl) -> true ; add_error(ctl,'CTL Parser failed: ',Formula),fail),
    set_max_nr_of_new_impl_trans_nodes(MaxNodes),
    select_ctl_mode(Mode,Ctl,Startnodes,Ctl2),
    ctl_model_check2(Ctl2,Mode,Startnodes,Res).

ctl_model_check2(Formula,Mode,InitStates,Res) :-
    reset_ctl,
    debug_println(4,ctl_preprocessing),
    ltl: preprocess_formula(Formula,PFormula),
    debug:debug_println(5,starting_ctl_model_check(PFormula,Mode,InitStates)),
    ( printtime(ctl_sat_for_all(PFormula,InitStates,Trace,Res)),
    debug_format(9,'CTL internal trace: ~w~n',[Trace]),
    Trace = [Initstate|_] ->
    ( Mode=init -> ltl: set_trace_to_init(Initstate) % we need to go to the initialised state
    % before the counterexample itself is shown
    ; Mode = specific_node(NodeID) -> ltl: set_trace_to_init(NodeID)
    ; true),
    expand_trace(Trace,ETrace), %debug_println(4,expanded(ETrace)),
    print_trace(Res,ETrace),
    ltl: executetrace(ETrace),
    (debug_mode(off)
    -> reset_ctl
    ; reset_ctl_with_stats
    )
    %,(formula_registry(F,Id),format('Formula ~w = ~w~n',[Id,F]),fail ; true)
    %, nl, findall(T,sat_eu_table(_,_,_,T,_),Ts), lists:max_member(Mx,Ts), print(max_trace_length(Mx)),nl
    %, (sat_eu_table(E,Fid,Gid,T2,R), print(sat_eu_table(E,Fid,Gid,T2,R)),nl,fail ; true)
    ;
    add_internal_error('CTL model check failed: ',PFormula),
    print_size_of_table(ctl: sat_eu_table/5),fail
).

ctl_model_check_with_ast(Proc,Ctl,MaxNodes,Mode,Res,CE) :-
    set_max_nr_of_new_impl_trans_nodes(MaxNodes),
    select_ctl_mode(Mode,Ctl,Startnodes,Ctl2),
    interruptable_ctl_model_check_with_ce3(Proc,Ctl2,Mode,Startnodes,Res,CE).

ctl_model_check_with_ce(Proc,Formula,MaxNodes,Mode,Res,CE) :-
    (temporal_parser(Formula,ctl,Ctl) -> true ; add_error_fail(ctl,'CTL Parser failed: ',Formula)),
    set_max_nr_of_new_impl_trans_nodes(MaxNodes),
    select_ctl_mode(Mode,Ctl,Startnodes,Ctl2),
    interruptable_ctl_model_check_with_ce2(Proc,Ctl2,Mode,Startnodes,Res,CE).

ctl_model_check_with_ce2(Proc,Formula,Mode,InitStates,Res,CE) :-
    reset_ctl,
    ltl: preprocess_formula(Formula,PFormula),
    ( printtime(ctl_sat_for_all(PFormula,InitStates,Trace,Res)) ->
    ( Res = true -> CE=none, printsilent('Witness found: '),nls
    ; Res = false -> print('CTL counterexample found: '),nl, convert_ctl_trace(Proc,PFormula,Mode,false,Trace,CE)
    ; CE=unexpected_result, print('Could not decide property: '), print(Res), print(': '),nl),
    (debug_mode(on) -> print(Trace),nl ; true),
    (silent_mode(on) -> reset_ctl
    ; reset_ctl_with_stats
    )
    ;
    add_internal_error('CTL model check failed: ',PFormula),
    print_size_of_table(ctl: sat_eu_table/5),fail
    ),nl.

ctl_model_check_with_ce3(Proc,Formula,Mode,InitStates,Res,CE) :-
    reset_ctl,
    ltl: preprocess_formula(Formula,PFormula),
    ( printtime(ctl_sat_for_all(PFormula,InitStates,Trace,Res)) ->
    ( Res = true -> CE=none, printsilent('Witness found: '),nls
    ; Res = false -> format('CTL counterexample found (~w)~n',[Mode]),
    convert_ctl_trace(Proc,PFormula,Mode,true,Trace,CE)
    ; CE=unexpected_result, print('Could not decide property: '), print(Res), print(': '),nl),
    (debug_mode(on) -> print(Trace),nl ; true),
    %expand_trace(Trace,ETrace), print(expanded(ETrace)),nl,
    (silent_mode(on) -> reset_ctl
    ; reset_ctl_with_stats
    )
    ;
    add_internal_error('CTL model check failed: ',PFormula),
    print_size_of_table(ctl: sat_eu_table/5),fail
    ),nl.

ctl_sat_for_all(Formula,States,Trace,Res) :-
    length(States,Len),
    (Len>1 -> formatsilent('Checking CTL formula for ~w initial states~n',[Len]) ; true),
    % one can also use Mode=specific_node(NodeID), but then Len=1
    ctl_sat_for_all2(States,Formula,[],unknown,Trace1,Res1),
    (Res1 = unknown -> Res=true, Trace=[] ; Res=Res1, Trace=Trace1).

ctl_sat_for_all2([],_Formula,Trace,Res,Trace,Res).

ctl_sat_for_all2([State|Srest],Formula,PrevTrace,PrevRes,Trace,Res) :-
    sat(Formula,State,Trace1,Res1),
    debug_format(19,'CTL result for state ~w: ~w~n',[State,Res1]),
    NewTrace = [State|Trace1],
    ( Res1=false ->
    % Counter-example found, use it and stop
    Res=false, Trace=NewTrace
    ; Res1=incomplete ->
    Res=incomplete, Trace=NewTrace
    ; PrevRes=unknown ->
    % First witness found, store and continue
    ctl_sat_for_all2(Srest,Formula,NewTrace,true,Trace,Res)
    ;
    % Another witness found, ignore it and use the old
    ctl_sat_for_all2(Srest,Formula,PrevTrace,true,Trace,Res)).

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

expand_trace([H|T],[H|ET]) :- !, expand_trace(T,ET).

expand_trace(eu(Fid,Gid,Next),[Next|ET]) :- !,
    sat_eu_table(Next,Fid,Gid,T,_),
    expand_trace(T,ET).

expand_trace(T,R) :- add_internal_error('Unknown trace: ',expand_trace(T,R)), T=R.

formula_to_id(Formula,Id) :- formula_registry(Formula,R),!,R=Id.

formula_to_id(Formula,Id) :- retract(next_id(R)),
    R1 is R+1, assertz(next_id(R1)),
    assertz(formula_registry(Formula,R)),
    Id = R.

get_event_trace(Trace,ETrace) :-
    get_event_trace1(Trace,Res),
    tools: ajoin_with_sep(Res,' -> ',ETrace).

get_event_trace1([],['']).

get_event_trace1([_NodeID],['']).

get_event_trace1([Src,Dest|Rest], [Event|Res]) :-
    transition(Src,Op,_OpId,Dest),
    translate_event(Op,Event),
    get_event_trace1([Dest|Rest],Res).

get_event_trace_transitions(init,[StartNode|T],CE) :-
    (transition(root,_,_,StartNode) ->
    get_event_trace_transitions2([root,StartNode|T],CE)
    ; transition(root,_,_,N1), transition(N1,_,_,StartNode) -> % setup constants first
    get_event_trace_transitions2([root,N1,StartNode|T],CE)
    ;
    get_event_trace_transitions2([root,StartNode|T],CE)).

get_event_trace_transitions(specific_node(Start),Trace,CE) :- % do we need a trace from root to Start ?
    get_event_trace_transitions2([Start|Trace],CE).

get_event_trace_transitions2([], Res) :- !, Res=[].

get_event_trace_transitions2([_NodeID],Res) :- !, Res=[].

get_event_trace_transitions2([Src,Dest|Rest], [transition(OpId,OpName,Src,Dest)|Res]) :-
    transition(Src,Op,OpId,Dest),!,
    get_operation_name(Op,OpName),
    get_event_trace_transitions2([Dest|Rest],Res).

get_event_trace_transitions2([Src,Dest|_],[]) :-
    add_error(ctl_model_check,'Cannot replay counter example, no transition for:',(Src,Dest)).

interruptable_ctl_model_check_with_ce2(Proc,Formula,Mode,InitStates,Res,CE) :-
    user_interruptable_call_det(catch_interrupt_assertion_call(ctl: ctl_model_check_with_ce2(Proc,Formula,Mode,InitStates,Res,CE)),InterruptResult),
    (InterruptResult=interrupted ->
    Res=interrupted
    ; real_error_occurred ->
    print_error('% *** Errors occurred while CTL model checking ! ***'),nl,nl,fail
    ; formatsilent('CTL assertion check completed.~n',[])
).

interruptable_ctl_model_check_with_ce3(Proc,Formula,Mode,InitStates,Res,CE) :-
    user_interruptable_call_det(catch_interrupt_assertion_call(ctl: ctl_model_check_with_ce3(Proc,Formula,Mode,InitStates,Res,CE)),InterruptResult),
    (InterruptResult=interrupted ->
    Res=interrupted
    ; real_error_occurred ->
    print_error('% *** Errors occurred while CTL model checking ! ***'),nl,nl,fail
    ; formatsilent('CTL assertion check completed.~n',[])
).

mark_all_computing_nodes_as_false(Fid,Gid,Computing) :-
    avl_member(E,Computing),
    assertz(sat_eu_table(E,Fid,Gid,[],false)),
    fail.

mark_all_computing_nodes_as_false(_F,_G,_Computing).

negate_result(true,false).

negate_result(false,true).

negate_result(incomplete,incomplete).

next_id(0).

parse_and_pp_ctl_formula(FormulaAsAtom,Text) :-
    temporal_parser(FormulaAsAtom,ctl,Ctl),
    ( ltl: pp_ltl_formula(Ctl,Text)
    -> true
    ; add_error_fail(ctl, 'Failed to pretty print CTL formula: ', Ctl)
).

print_trace(_,_) :- silent_mode(on),!.

print_trace(Res,Trace) :-
    (length(Trace,Len) -> true ; Len=0),
    ( Res = true -> format('CTL Witness of length ~w found~n',[Len])
    ; Res = false -> format('CTL counterexample of length ~w found~n',[Len])
    ; format('Could not decide CTL property, checking result: ~w~n',[Res])
    ),
    (debug_mode(on) -> format('Trace: ~w~n',[Trace]) ; true).

printtime(C) :-
    statistics(runtime,[Start|_]), statistics(walltime,[StartW|_]),
    (call(C) -> Res=ok ; Res=failure),
    statistics(runtime,[End|_]), statistics(walltime,[EndW|_]),
    T is End - Start, TW is EndW - StartW,
    formatsilent('CTL check took ~3d seconds walltime (~3d seconds runtime) ~n', [TW,T]),
    Res=ok.

reset_ctl :-
    retractall(sat_eg_table(_,_,_)),
    retractall(sat_eu_table(_,_,_,_,_)),
    retractall(formula_registry(_,_)),
    retractall(next_id(_)),
    assertz(next_id(0)).

reset_ctl_ce_cache :-
    retractall(ctl_counter_examples_cache(_,_,_,_)).

reset_ctl_with_stats :-
    print_size_of_table(ctl: sat_eg_table/3),
    print_size_of_table(ctl: sat_eu_table/5),
    print_size_of_table(ctl: formula_registry/2),
    retract_with_statistics(ctl,[sat_eg_table(_,_,_),sat_eu_table(_,_,_,_,_)]).

sat(true,_E,T,R) :- !, T=[], R=true.

sat(false,_E,T,R) :- !, T=[], R=false.

sat(not(F),E,T,Res) :- !, sat(F,E,T,Res1), negate_result(Res1,Res).

sat(ap(P),E,[],Res) :- !, (check_ap(P,E) -> Res=true ; Res=false). /* elementary atomic proposition */

sat(action(OpSpec),E,T,Res) :- !, /* transition proposition */
    (trans(E,E2,Act),
    check_transition(OpSpec,Act,E,E2)
    -> Res=true, T=[E2]
    ; Res=false, T=[]).

sat(and(F,G),E,T,Res) :- !,
    sat(F,E,T1,Res1),
    (Res1=false -> Res=false,T=T1
    ; sat(G,E,T,Res)).

sat(or(F,G),E,T,Res) :- !,
    sat(F,E,T1,Res1),
    (Res1=true -> Res=true,T=T1
    ; sat(G,E,T,Res)
).

sat(implies(A,B),E,T,Res) :- !, sat( or(not(A),B),E,T,Res).

sat(equivalent(A,B),E,T,Res) :- !, sat( and(implies(A,B),implies(B,A)),E,T,Res).

sat(an(F),E,T,Res) :- !, sat(not(en(not(F))),E,T,Res).

sat(en(F),E,T,Res) :- !, /* exists next */
    (trans(E,E2,_),
    sat(F,E2,T2,true)
    -> Res=true, T=[E2|T2]
    ; Res=false, T=[]).

sat(action(OpSpec,F),E,T,Res) :- !,
    /* exists next with predicate on transition; ena renamed to action by preprocess_formula2 */
    (trans(E,E2,Act),
    check_transition(OpSpec,Act,E,E2),sat(F,E2,T2,true)
    -> Res=true, T=[E2|T2]
    ; Res=false, T=[]).

sat(eu(F,G),E,T,Res) :- !, /* exists until */
    sat_eu(E,F,G,T,Res).

sat(ef(F),E,T,Res) :- !, /* exists future */
    sat(eu(true,F),E,T,Res).

sat(ag(F),E,T,Res) :- !, sat(not(ef(not(F))),E,T,Res).

sat(af(F),E,T,Res) :- !, sat(not(eg(not(F))),E,T,Res).

sat(eg(F),E,T,Res) :- !, sat_eg(E,F,T,Res).

sat(X,State,T,R) :- add_internal_error('Uncovered CTL Formula: ',sat(X,State,T,R)),fail.

sat_eg(E,F,[],R) :-
    sat_eg_table(E,F,Res),!,
    R=Res. % loop found

sat_eg(E,F,[],R) :- sat(F,E,_T,false),!,
    assertz(sat_eg_table(E,F,false)),
    R=false.

sat_eg(E,F,[E2|T],R) :- %print(true(E,F)),nl,
    assertz(sat_eg_table(E,F,true)),
    trans(E,E2,_Act),
    (\+ (trans(E,E3,_), E2 \= E3) % deterministic transition: extend counter example; no need to backtrack
    -> %!, % this cut causes to recognise already visited states as the begining of a loop
    % since it skips the retracting-clause of sat_eg
    sat_eg(E2,F,T,R)
    ; sat_eg(E2,F,T,true),!,R=true
).

sat_eg(E,F,T,R) :- retract(sat_eg_table(E,F,_)),assertz(sat_eg_table(E,F,false)),
    T=[],R=false.

sat_eu(E,F,G,T,R) :- formula_to_id(F,Fid), formula_to_id(G,Gid),
    sat_eu1(E,F,Fid,G,Gid,T,R).

sat_eu1(E,F,Fid,G,Gid,T,R) :-
    empty_avl(Computing), %print(start_eu(E,F,G,T,R)),nl,
    sat_eu2(E,F,Fid,G,Gid,Computing,OutComputing,T,Res), % print(res(Res)),nl,
    ( Res = computing ->
    % we found only false and computing (i.e. cycles) nodes,
    % there is no true node to encounter
    assertz(sat_eu_table(E,Fid,Gid,[],false)),
    % we know that all visited nodes must be false, too
    mark_all_computing_nodes_as_false(Fid,Gid,OutComputing),
    R=false
    ;
    R = Res).

sat_eu2(E,_F,_,_G,_,InComputing,OutComputing,T,R) :-
    % the node has already been checked, Result is "computing"
    avl_fetch(E,InComputing),!,R=computing,T=[],OutComputing = InComputing.

sat_eu2(E,_F,Fid,_G,Gid,InComputing,OutComputing,T,R) :-
    % the value for this node has already been computed
    sat_eu_table(E,Fid,Gid,TT,Res),!, %print(sat_eu_table(E,F,G,TT,Res)),nl,
    R=Res,T=TT,OutComputing=InComputing.

sat_eu2(E,_F,Fid,G,Gid,InComputing,OutComputing,T,Res) :- % print(sat_eu_eval(E,F,G)),nl,
    % the goal is true in this node
    Res=true,
    /* exists until */
    sat(G,E,T,true),!,
    % print(set_eu_g_true(G,T)),nl,
    assertz(sat_eu_table(E,Fid,Gid,T,true)),
    %% assertz(sat_eu_table(E,Fid,Gid,[],true)),
    InComputing = OutComputing.

sat_eu2(E,F,Fid,G,Gid,InComputing,OutComputing,T,Res) :- /* exists until */
    % the goal is not true
    % sat(not(G),E,_), /* added to avoid extra answers */
    sat(F,E,T1,Res1),
    % print(sat_eu_loop(E,F,T1,Res1)),nl,
    (
    Res1=true ->
    avl_store(E,InComputing,true,Computing),
    sat_eu_step(E,F,Fid,G,Gid,Computing,OutComputing,T2,Res2),
    ( Res2 = true ->
    % we found a node with the goal, mark this as true
    assertz(sat_eu_table(E,Fid,Gid,T2,true)), %% < ------------- T2
    Res=true, T=T2
    ; Res2 = computing ->
    Res=computing, T=[]
    ;
    % we found only false or incomplete nodes, mark this as false / incomplete
    assertz(sat_eu_table(E,Fid,Gid,[],Res2)),
    Res=Res2, T=[]
    )
    ; /* Res1 = false or incomplete */
    % if F is false the result is false anyhow - we do not have to look into the future
    assertz(sat_eu_table(E,Fid,Gid,[],Res1)),
    Res=Res1, T=T1, OutComputing=InComputing
).

sat_eu_step(E,F,Fid,G,Gid,InComputing,OutComputing,T,R) :-
    findall(N,trans(E,N,_),Nexts), % Nexts can be [] when max_nr_of_new_nodes reached; TO DO: catch error occuring in decrease_max_nr_of_new_nodes and set Result to incomplete
    (Nexts = [], not_all_transitions_added(E) -> InResult=incomplete ; InResult = false),
    sat_eu_step2(Nexts,F,Fid,G,Gid,InComputing,OutComputing,T,InResult,R).

sat_eu_step2([],_F,_,_G,_,InComputing,OutComputing,T,In,Out) :- !,In=Out,T=[],InComputing=OutComputing.

sat_eu_step2([Next|Nrest],F,Fid,G,Gid,InComputing,OutComputing,T,In,R) :-
    sat_eu2(Next,F,Fid,G,Gid,InComputing,Computing,_T2,Res),
    ( Res=true -> R=true, T=eu(Fid,Gid,Next), % --> we now store link to next node and not full trace: T=[Next|T2],
    OutComputing=Computing
    ;
    combine_result(In,Res,New),
    sat_eu_step2(Nrest,F,Fid,G,Gid,Computing,OutComputing,T,New,R)).

select_ctl_mode(starthere,Ctl,[Startnode],Ctl) :-
    !, current_state_id(Startnode),
    debug_format(19,'Checking CTL formula from current state: ~w~n',[Startnode]).

select_ctl_mode(init,Ctl,Startnodes,Ctl) :-
    !, find_initialised_states(Startnodes),
    debug_format(19,'Checking CTL formula from all initial states: ~w~n',[Startnodes]).

select_ctl_mode(specific_node(Startnode),Ctl,[Startnode],Ctl) :-
    !,
    debug_format(19,'Checking CTL formula from specific state: ~w~n',[Startnode]).

select_ctl_mode(Mode,Ctl,[],Ctl) :-
    add_error(ltl,'Internal error: Unexpected mode', Mode),
    fail.

tcltk_play_ctl_counterexample(Proc,Ctl) :-
    ctl_counter_examples_cache(Proc,Ctl,Mode,ETrace),
    ETrace = [Initstate|_],
    ( Mode=init -> ltl: set_trace_to_init(Initstate)
    ; Mode = specific_node(NodeID) -> ltl: set_trace_to_init(NodeID)
    ; true),
    ltl: executetrace(ETrace).

tcltk_play_ctl_counterexample(Proc,Ctl) :-
    add_error_fail(ctl_counter_example, 'Internal error: No counterexample has been asserted for the following configuration: ',(Proc,Ctl)).