safety_mc

add_state_at_queue_end(State,AutState,ActionId,coming_from(PrevState,PrevAutState,PrevActionId)) :-
    % format('QUEUING: (~w,~w) --~w--> ~n',[State,AutState,ActionId]),
    assertz(product(State,AutState,ActionId)),
    assertz(visited_pair_origin(State,AutState,ActionId,PrevState,PrevAutState,PrevActionId)).

add_state_at_queue_front(State,AutState,ActionId,coming_from(PrevState,PrevAutState,PrevActionId)) :-
    % format('QUEUING at FRONT: (~w,~w) --~w--> ~n',[State,AutState,ActionId]),
    asserta(product(State,AutState,ActionId)),
    assertz(visited_pair_origin(State,AutState,ActionId,PrevState,PrevAutState,PrevActionId)).

add_state_to_queue(State,AutState,ActionId,From) :-
    (aut_final_state_reached(AutState) ->
    add_state_at_queue_front(State,AutState,ActionId,From),
    debug_format(19,'** Found Accepting state ~w~n',[(State,AutState,ActionId)]),
    assertz(accepting_state(State,AutState,ActionId)) % save accepting state (for building later the counter-example)
    ; add_state_at_queue_end(State,AutState,ActionId,From)
).

already_visited(DestId,NextAutState,NextActionId) :-
    visited_pair(DestId,NextAutState,OtherActionId),
    (var(OtherActionId) -> true % we have already processed this product state without a constraint on the next action
    ; var(NextActionId) -> false % we now process the product state with unrestricted next action id: could be more behaviour
    ; NextActionId = OtherActionId).

aut_final_state_reached(AutState) :- aut_final_state(AutState),
    (AutState = 'accept_all' -> true ; aut_transition(AutState,true,AutState)).

check_ap_at_state(deadlock,StateId) :- !,
    animation_mode(MODE),
    get_b_optimisation_options(MODE,Optimizations),
    compute_state_space_transitions_if_necessary2(StateId,Optimizations),
    \+ transition(StateId,_ActionId,_ActionAsTerm,_DestId).

check_ap_at_state(AP,StateId) :-
    check_ap(AP,StateId).

check_for_aut_transition(AutState,CurId,NextAutState,ActionId) :-
    aut_transition(AutState,Label,NextAutState),
    check_transition(Label,CurId,ActionId). % check if label matches transition ActionId from B State CurId

check_transition(true,_StateId,_ActionId) :- !.

check_transition(false,_StateId,_ActionId) :- !, fail.

check_transition(ap(AP),StateId,_ActionId) :- !,
    check_ap_at_state(AP,StateId).

check_transition(tp(TP),StateId,ActionId) :- !,
    %check_enabled(TP,StateId), % not sure why this is required: it checks there is one solution; the code below will do that as well
    transition(StateId,Op,ActionId,DestId),
    check_transition_pred(TP,Op,StateId,ActionId,DestId). % ltl_propositions

check_transition(not(AF),StateId,ActionId) :- !,
    check_transition_fail(AF,StateId,ActionId).

check_transition(and(AF,AG),StateId,ActionId) :- !,
    check_transition(AF,StateId,ActionId),
    check_transition(AG,StateId,ActionId).

check_transition(or(AF,AG),StateId,ActionId) :- !,
    (check_transition(AF,StateId,ActionId) ;
    check_transition(AG,StateId,ActionId)).

check_transition(Label,_StateId,_ActionId) :-
    add_error_fail(check_transition,'Unknown Buchi automaton transition label: ', Label).

check_transition_fail(true,_StateId,_ActionId) :- !, fail.

check_transition_fail(false,_StateId,_ActionId) :- !.

check_transition_fail(ap(AP),StateId,_ActionId) :- !,
    (check_ap_at_state(AP,StateId)-> fail; true).

check_transition_fail(tp(TP),StateId,ActionId) :- !,
    transition(StateId,Op,ActionId,DestId), % we require DestId to be known
    \+ ltl_propositions:check_transition_pred(TP,Op,StateId,ActionId,DestId).

check_transition_fail(not(AF),StateId,ActionId) :- !,
    check_transition(AF,StateId,ActionId).

check_transition_fail(and(AF,AG),StateId,ActionId) :- !,
    (check_transition_fail(AF,StateId,ActionId) ;
    check_transition_fail(AG,StateId,ActionId) ).

check_transition_fail(or(AF,AG),StateId,ActionId) :- !,
    check_transition_fail(AF,StateId,ActionId),
    check_transition_fail(AG,StateId,ActionId).

check_transition_fail(Label,_StateId,_ActionId) :-
    add_error_fail(check_transition,'Unknown Buchi automaton transition label: ', Label).

compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs,Optimizations) :-
    copy_term(ActionId,OrigActionId),
    member((ActionId,_Term,DestId),ActionsAndIDs),
    % format(' Processing state transition: (B:~w,BuechiAut:~w) --~w--> B:~w~n',[CurId,AutState,ActionId,DestId]),
    compute_state_space_transitions_if_necessary2(DestId,Optimizations),
    get_aut_successor(AutState,NextAutState),
    % backtrack over candidate successor automata states first to perform visited_pair check,
    % before finding all matching B transitions (NextActionId, if any)
   
    % format(' Attempting to find compatible transitions to BA state ~w~n',[NextAutState]),
    % if NextActionId is a variable, then any transition is ok
    % now add all next actions to the queue which lead to NextAutState
    check_for_aut_transition(AutState,DestId,NextAutState,NextActionId), % NextActionId is variable if no constraint on it
    % format(' reaching: ~w * ~w (automata state via forced next action ~w)~n',[DestId,NextAutState,NextActionId]),
   
    \+ already_visited(DestId,NextAutState,NextActionId), % pair not yet processed;
    % format(' Asserting ~w~n',[visited_pair(DestId,NextAutState,NextActionId)]),
    assertz(visited_pair(DestId,NextAutState,NextActionId)), % mark as processed / to-be-processed in queue
    (aut_final_state_reached(NextAutState) ->
    add_state_to_queue(DestId,NextAutState,NextActionId,coming_from(CurId,AutState,OrigActionId))
    ;
    add_state_at_queue_end(DestId,NextAutState,NextActionId,coming_from(CurId,AutState,OrigActionId)),
    fail
).

compute_all_product_transitions(_CurId,_AutState,_ActionId,_ActionsAndIDs,_).

compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs) :-
    compute_state_space_transitions_if_necessary2(CurId,Optimizations),
    findall((ActId,ActionAsTerm,DestId),
    transition(CurId,ActionAsTerm,ActId,DestId),
    ActionsAndIDs).

compute_state_space_transitions_if_necessary2(CurId,Optimizations) :-
    (not_all_transitions_added(CurId),
    %format('Computing transitions for ~w (~w)~n',[CurId,Optimizations]),
    (retract_open_node(CurId) -> true ; add_warning(safety_mc,'Not open node: ',CurId))
    -> % if node is still not retracted from queue
    % TODO: keep track of ltllimit maximum number of new nodes to explore
    set_context_state(CurId),
    visited_expression(CurId,CurState),
    compute_transitions_opt(Optimizations,CurId,CurState),
    clear_context_state
    ; true % nothing to do
).

create_and_add_init_state((CurId,AutState,ActionId)) :-
    debug_format(5,'Creating initial state [~w:BA ~w] -- ~w -->~n',[CurId,AutState,ActionId]),
    (already_visited(CurId,AutState,ActionId) -> fail ; assertz(visited_pair(CurId,AutState,ActionId)) ),
    add_state_to_queue(CurId,AutState,ActionId,coming_from(root,root,none)).

get_aut_successor(AutState,accept_all) :- (aut_transition(AutState,_,accept_all) -> true).

get_aut_successor(AutState,NextAutState) :- % TODO: randomise and succeed only once if multiple transitions lead
    aut_transition(AutState,true,NextAutState),
    %(the idea is to execute as soon as possible transitions that do not have the label 'true')
    NextAutState \= accept_all.

get_aut_successor(AutState,NextAutState) :- % TODO: randomise and succeed only once if multiple transitions lead
    aut_transition(AutState,Label,NextAutState), Label \= true, NextAutState \= accept_all.

get_ba_successor_state(StartNode,Init,(StartNode,Next,ActionId)) :-
    aut_transition(Init,Label,Next), % Büchi Automata transition via Label
    check_transition(Label,StartNode,ActionId). % ActionId: id required to satisfy Label (if it has a transition property)

get_bf_search_result(none,Result,Len) :- !, Result = none, Len=0.

get_bf_search_result(counter_example_found,Result,Length) :- !,
    get_counter_example_from_product(Result,Length),
    debug_println(9,counter_example(Length,Result)).

get_bf_search_result(Arg,_Result,_Len) :-
    add_error_fail(run_mc_safety_property_bf, 'Unknow result: ', Arg).

get_counter_example_from_product(Result,Length) :-
    accepting_state(State,AutState,ActionId),!,
    (nonvar(ActionId) -> Trans = ActionId; Trans = none),
    debug_format(19,'Start constructing counter-example backwards from ~w:~w~n',[State,AutState]),
    %listing(accepting_state/3),nl, listing(visited_pair/3),nl, listing(visited_pair_origin/6),nl,
    get_counter_example_list(State,AutState,ActionId,[atom(State,[1],Trans)],ResList),
    Result = model(ResList,no_loop),
    length(ResList,Length).

get_counter_example_from_product(Result,0) :-
    add_error(safety_mc,'No accepting state was found (this is an internal error in the model checker).'),
    Result=[].

get_counter_example_list(State,AutState,ActionId,CurRes,Result) :-
    visited_pair_origin(State,AutState,StoredActionId,root,root,none),
    (ActionId==StoredActionId -> true ; var(StoredActionId), var(ActionId)),
    !, % we found our way back to an initial state
    Result = CurRes.

get_counter_example_list(State,AutState,ActionId,CurRes,Result) :-
    (%visited_pair(State,AutState,PrevState,PrevAutState,StoredActionId), % Note there could be several entries
    visited_pair_origin(State,AutState,StoredActionId,PrevState,PrevAutState,PrevActionId),
    (ActionId==StoredActionId -> true ; var(StoredActionId), var(ActionId)),
    debug_format(5,' [~w:BA ~w] ---counter_ex_trans:~w---> previous:[~w:BA ~w ~w]~n',[State,AutState,ActionId,PrevState,PrevAutState,PrevActionId]),
    copy_term(PrevActionId,GroundPrevActionId),
    transition(PrevState,_ActionAsTerm,GroundPrevActionId,State), % has only one solution if ActionId ground
    aut_transition(PrevAutState,_,AutState)
    -> get_counter_example_list(PrevState,PrevAutState,PrevActionId,
    [atom(PrevState,[1],GroundPrevActionId)|CurRes], Result)
    ; add_error(get_counter_example_list,'Could not find visited predecessor for: ',(State:AutState)),
    Result=CurRes
).

get_init_product(_StartNode,[],[]).

get_init_product(StartNode,[Init|Inits],Res) :-
    findall(Succ,get_ba_successor_state(StartNode,Init,Succ),L),
    append(L,Res1,Res),
    get_init_product(StartNode,Inits,Res1).

get_next_node(CurId,AutState,ActionId) :-
    pop_state_from_end(product(CurId,AutState,ActionId)).

get_next_state(ActionsAndIDs,ActionId,DstId) :-
    member((ActionId,_Term,DstId),ActionsAndIDs).

get_product_init_states([],_InitStates,_Optimizations,[]).

get_product_init_states([StartNode|Nodes],InitStates,Optimizations,Res) :-
    (ltl_safety:tps_occurring % for transition properties we need to have outgoing transitions
    -> compute_state_space_transitions_if_necessary2(StartNode,Optimizations)
    ; true),
    get_init_product(StartNode,InitStates,IStates),
    append(IStates,Res1,Res),
    get_product_init_states(Nodes,InitStates,Optimizations,Res1).

get_state_space_statistics(TS,Product) :-
    findall((X,Y),visited_pair_df(X,Y),L),
    debug_println(9,product_states(L)),
    length(L,Product),
    findall(ID,visited_expression_id(ID),IDL),
    length(IDL,TS).

initial_states_mc_safety_property(StartNodes,Optimizations,ProductInitStatesSet) :-
    findall(Init,aut_initial_state(Init),InitStates),
    get_product_init_states(StartNodes,InitStates,Optimizations,ProductInitStates),
    list_to_ord_set(ProductInitStates,ProductInitStatesSet),
    debug_println(9,init_states(ProductInitStatesSet)).

mc_safety_property((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
    assertz(visited_pair_df(CurId,AutState)),
    debug_println(19,current_history(CurId,History)),
    check_for_aut_transition(AutState,CurId,NextAutState,ActionId),
    mc_safety_property_next_state((CurId,NextAutState,ActionId),Optimizations,History,HTail,Result).

mc_safety_property_init((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
    (transition(CurId,_Op,ActionId,CurId) -> true ; assertz(visited_pair_df(CurId,AutState))),
    mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result).

mc_safety_property_next_state((CurId,AutState,ActionId),_Optimizations,History,[atom(CurId,[1],ActionId1)],Result) :-
    aut_final_state_reached(AutState),!,
    ( nonvar(ActionId) -> ActionId1=ActionId; ActionId1 = none),
    print(found_error(counter_example_found,CurId,History)),nl,
    Result = model(History,no_loop).

mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
    compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs),
    random_permutation(ActionsAndIDs,ActionsAndIDs1),
    HTail = [atom(CurId,[1],ActionId)|HTail2],
    get_next_state(ActionsAndIDs1,ActionId,DestId),
    \+ visited_pair_df(DestId,AutState),
    (ltl_safety:tps_occurring % if there is a transition property, we need outgoing transitions
    -> compute_state_space_transitions_if_necessary2(DestId,Optimizations)
    ; true),
    mc_safety_property((DestId,AutState,_NewActionId),Optimizations,History,HTail2,Result).

non_empty_automaton :-
    aut_transition(_P,_L,_Q).

open_search(Nr,RefWallTime,Optimizations,Result) :-
    get_next_node(CurId,AutState,ActionId),!,
    debug_format(5,'~nProcessing B state ~w, BA state:~w, next action:~w~n',[CurId,AutState,ActionId]),
    (aut_final_state_reached(AutState) -> % bad prefix has been found
    Result = counter_example_found,
    format('Found counter example (bad prefix) leading to state [~w: BA ~w]~n',[CurId,AutState])
    ; % continue the search
    Nr1 is Nr +1,
    (print_progress(Nr1,RefWallTime,NewRefTime)
    -> DeltaW is (NewRefTime-RefWallTime)/1000,
    get_model_check_stats(SS,TT,_,Perc,_,_),
    formatsilent('Safety model checker progress: ~w product states processed (delta = ~1f sec)~nState space statistics: ~w states checked (~1f%), ~w transitions~n',[Nr1,DeltaW,SS,Perc,TT])
    ; NewRefTime=RefWallTime),
    compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs),
    % format(' Transitions for ~w: ~w~n',[CurId,ActionsAndIDs]),
    compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs,Optimizations),
    open_search(Nr1,NewRefTime,Optimizations,Result)
).

open_search(Nr,_,_Optimizations,Res) :-
    Res = none,
    format('All relevant states visited!~nProduct states analysed: ~w~n',[Nr]). % these are product states

pop_state_from_end(Node) :-
    retract(product(State,AutState,ActionId)),!,
    Node = product(State,AutState,ActionId).

prepare_mc_safety_property :-
    retractall(product(_,_,_)),
    retractall(visited_pair(_,_,_)),
    retractall(visited_pair_origin(_,_,_, _,_,_)),
    retractall(visited_pair_df(_,_)),
    retractall(accepting_state(_,_,_)).

print_progress(Nr1,_,NewRefTime) :- Nr1 mod 10000 =:= 0, statistics(walltime,[NewRefTime,_]).

print_progress(Nr1,RefWallTime,NewRefTime) :- Nr1 mod 100 =:= 0, statistics(walltime,[NewRefTime,_]),
    NewRefTime-RefWallTime > 10000. % more than 10 secs passed

run_mc_safety_property(breadth_first,ProductInitStates,Optimizations,Result) :- !,
    cputime(T1),
    run_mc_safety_property_bf(ProductInitStates,Optimizations,IntermediateResult),
    cputime(T2), D is T2-T1,
    format('% Overall Checking Time: ~w ms~n',[D]),
    cputime(T1_CE),
    get_bf_search_result(IntermediateResult,Result,Length),
    cputime(T2_CE),
    D_CE is T2_CE-T1_CE,
    write(result(Result)),nl,
    format('% Time to get result (~w) of length ~w from breadth-first safety model checking: ~w ms~n',[IntermediateResult,Length,D_CE]).

run_mc_safety_property(random,ProductInitStates,Optimizations,Result) :- !,
    cputime(T1),
    (run_mc_safety_property_df(ProductInitStates,Optimizations,Result) ->
    cputime(T2),
    print('Counter-example has been found'),nl,
    print(counter_example(Result)),nl
    ;
    cputime(T2),
    get_state_space_statistics(TS,Product),
    print('All nodes visited. No counter-example has been found.'), nl,
    print('Number of states checked: '), print(Product), print(', where '),
    print('number of states of the transition system is: '), print(TS), nl,
    Result = none
    ),
    print('% Overall Checking Time: '), D is T2-T1, print(D), print(' ms'),nl.

run_mc_safety_property(Otherwise,_ProductInitStates,_,_Result) :-
    add_error_fail(run_mc_safety_property,'Unknown search mode: ', Otherwise).

run_mc_safety_property_bf(ProductInitStates,Optimizations,Result) :-
    maplist(create_and_add_init_state,ProductInitStates),
    Nr = 0,
    statistics(walltime,[W1,_]),
    open_search(Nr,W1,Optimizations,Result).

run_mc_safety_property_df(InitStates,Optimizations,Result) :-
    member((CurId,AutState,ActionId),InitStates),
    (trivial_automaton -> % the automaton is trivial , i.e. we have checked the formula 'false' and need to return one of the initial states as a counter-example
    %% CEPath = [atom(CurId,CurId,none)],
    Result=model([atom(CurId,[1],none)],no_loop)
    ;
    mc_safety_property_init((CurId,AutState,ActionId),Optimizations,CEPath,CEPath,Result)
).

start_mc_safety_property(SearchMode,StartNodes,Result) :-
    prepare_mc_safety_property,
    animation_mode(MODE),
    get_b_optimisation_options(MODE,Optimizations),
    %% perform_static_analyses(MODE,Optimizations),
    initial_states_mc_safety_property(StartNodes,Optimizations,ProductInitStates),
    (ProductInitStates == [], non_empty_automaton
    -> %add_warning(run_mc_safety_property,'No initial states of the product transition system have been generated.'),
    Result = none,
    print('All relevant states visited (no initial LTL states feasible)! Product states analysed: '), print(0), nl
    ;
    (\+ aut_final_state_reached(_)
    -> add_warning(run_mc_safety_property,'No accept_all state has been found. The property is possibly not a safety property.')
    ; true),
    (select((State,AutState,AId),ProductInitStates,Rest), aut_final_state_reached(AutState)
    -> Initial = [(State,AutState,AId) | Rest]
    ; Initial = ProductInitStates
    ),
    %format('Running LTL Safety MC in mode ~w : ~w~n',[SearchMode,Initial]),
    run_mc_safety_property(SearchMode,Initial,Optimizations,Result)
).

trivial_automaton :-
    aut_transition(P,L,Q),
    (P=='accept_init',(L = ap(bpred(Pred))->is_truth(Pred);fail),Q =='accept_init').