ltl_fairness

check_scc_ce(LtlFormula,SCC) :-
    Max = 10000, Mode = init,
    (temporal_parser(LtlFormula,ltl,Ltl) -> true ; add_error_fail(ltl,'LTL Parser failed: ',LtlFormula)),
    ltl_model_check_ast(Ltl,Max,Mode,_,Status), % TO DO: why do we call this internal predicate ??
    clean_scc(Status,Result),
    atom_codes(SCC,Codes),
    read_from_codes(Codes,SCCTerm),
    (match_ce_result(SCCTerm,Result) ->
    true
    ;
    print(result_was(Result)),nl,
    add_error(ltl_scc_check,'No one of the SCCs could be reproduced as counter example: ',SCC)
).

clean_scc(model(Trace,Entry),Result) :-
    maplist(get_nodeid,Trace,CleanedTrace),
    Result = model(CleanedTrace,Entry).

cltl_get_enabled_actions_callback(StateIds,ActionsSet) :-
    % is it possible to get an empty list?
    findall(Action,(member(StateId,StateIds),get_enabled_action(StateId,Action)),Actions),
    list_to_ord_set(Actions,ActionsSet),
    debug_println(9,enabled_actions(StateIds,ActionsSet)).

cltl_get_transition_ids_callback(Arg,StateIds,LTransIds) :-
    (var(Arg) ->
    add_internal_error('Action argument is a variable!',cltl_get_transition_ids_callback(Arg,StateIds,LTransIds))
    ; var(StateIds) ->
    % if StateIds is a variable it can cause endless loop (memory use increases rapidly)
    add_internal_error('Unexpected argument for state ids. Expected a list of state ids, but got a variable!',cltl_get_transition_ids_callback(Arg,StateIds,LTransIds))
    ;
    get_transition_ids(Arg,StateIds,LTransIds),
    length(StateIds,NStates),length(LTransIds,NTransitions),
    debug_println(9,get_transition_ids(fainress_argument(Arg),state_ids(NStates,StateIds),transition_ids(NTransitions,LTransIds)))
).

create_action_argument(A,Action) :-
    animation_mode(Mode),
    (Mode == cspm ->
    get_tp_specification_for_csp(A,Action)
    ; Mode == b ->
    get_tp_specification_for_b(A,Action)
    ; Mode == csp_and_b ->
    get_tp_specification_for_csp_and_b(A,Action)
    ; Mode == xtl -> %TO DO: review wether ok
    create_xtl_action_argument(A,Action)
    ; % TODO: implement general fairness check support also for the other formalisms
    animation_mode(Mode),
    add_error(ltl_wrap_action,'Fairness not supported for ',action(A,Mode))
).

create_xtl_action_argument(Op,xtl(OpName,Arity,Args)) :-
    functor(Op,OpName,Arity), Op =.. [_|Args].

ev_fairness_id(Spec,StateId,Op) :-
    check_transition(Spec,Op,StateId,_DstId).

ev_fairness_id(Spec,StateId,TransId,Op) :-
    transition(StateId,Op,TransId,DstId),
    check_transition(Spec,Op,StateId,DstId).

ex2disj(or(A,B),or(AR,BR)) :- !,
    ex2disj(A,AR),
    ex2disj(B,BR).

ex2disj(and(A,B),R) :- !,
    ex2disj(A,AR),
    ex2disj(B,BR),
    join(AR,BR,R).

ex2disj(ap(X),ap(X)) :- !.

fairness_check_on(all,_StrongFairnessAssumption).

fairness_check_on([_|_],_StrongFairnessAssumption).

fairness_check_on(_WeakFairnessAssumption,all).

fairness_check_on(_WeakFairnessAssumption,[_|_]).

get_and_args(ap(strong_fair(A)),[R]) :- !, preprocess_tp(A,R).

get_and_args(ap(weak_fair(A)),[R]) :- !, preprocess_tp(A,R).

get_and_args(and(A,B),Res) :- !,
    get_and_args(A,R1),
    get_and_args(B,R2),
    append(R1,R2,Res).

get_enabled_action(StateId,Action):-
    transition(StateId,A,_AId,_DstId),
    create_action_argument(A,Action).

get_fairness_assumption_actions(F,Res) :-
    (F=all ->
    Res = all
    ;
    normalise_to_dnf(F,DNF),
    (debug:debug_mode(on) ->
    ltl_translate: pp_ltl_formula(DNF,Text),
    print('Disjunctive Normal Form for Fairness Forlmula: '),
    print(Text),nl
    ; true),
    get_or_args(DNF,R),
    list_to_ord_set(R,Res)
).

get_fairness_specification(loop(ReEntry),StateTransitions,Assumption) :- !,
    append_length(Loop,StateTransitions,ReEntry),
    maplist(get_specifications,Loop,ListsofSpecs),
    append(ListsofSpecs,Specs),
    list_to_ord_set(Specs,OrdSet),
    Assumption = [OrdSet].

get_fairness_specification(_,_,[[]]).

get_nodeid(atom(StateId,_Evaluation,_AtomId),StateId).

get_nodeid(El,StateId) :- add_internal_error('Unrecognised trace element: ', get_nodeid(El,StateId)).

get_or_args(ap(strong_fair(A)),[[R]]) :- !,
    preprocess_tp(A,R).

get_or_args(ap(weak_fair(A)),[[R]]) :- !,
    preprocess_tp(A,R).

get_or_args(and(A,B),Args) :- !,
    get_and_args(and(A,B),Res),
    list_to_ord_set(Res,Res1),
    Args = [Res1].

get_or_args(or(A,B),Res) :- !,
    get_or_args(A,R1),
    get_or_args(B,R2),
    append(R1,R2,Res).

get_specifications(strans(StateId,_),Specs) :-
    findall(Spec,
    (transition(StateId,Transition,_TransId,_DstId),get_tp_specification(Transition,Spec)),
    Specs).

get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs) :-
    (FairnessFormula = and(strongassumptions(SAssumptions),weakassumptions(WAssumptions))
    -> get_fairness_assumption_actions(SAssumptions,StrongFairnessArgs),
    get_fairness_assumption_actions(WAssumptions,WeakFairnessArgs)
    ; FairnessFormula = and(weakassumptions(WAssumptions),strongassumptions(SAssumptions))
    -> get_fairness_assumption_actions(SAssumptions,StrongFairnessArgs),
    get_fairness_assumption_actions(WAssumptions,WeakFairnessArgs)
    ; FairnessFormula = weakassumptions(F)
    -> StrongFairnessArgs =[], get_fairness_assumption_actions(F,WeakFairnessArgs)
    ; FairnessFormula = strongassumptions(F)
    -> WeakFairnessArgs = [], get_fairness_assumption_actions(F,StrongFairnessArgs)
    ;
    add_internal_error('Unrecognised fairness assumption: ', get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs))
).

get_tp_specification(Transition,Spec) :- animation_mode(Mode),
    get_tp_specification(Mode,Transition,Spec).

get_tp_specification(b,Transition,Spec) :- !,
    get_tp_specification_for_b(Transition,Spec).

get_tp_specification(csp_and_b,Transition,Spec) :- !,
    get_tp_specification_for_csp_and_b(Transition,Spec).

get_tp_specification(cspm,Transition,Spec) :- !,
    get_tp_specification_for_csp(Transition,Spec).

get_tp_specification(xtl, Transition,Spec) :- !, % TO DO: review wether ok
    create_xtl_action_argument(Transition,Spec).

get_tp_specification(Mode,Transition,_Spec) :-
    add_error_fail(ltl_verification, 'Fairness not implemented for formalism yet ',Mode:Transition).

get_tp_specification_for_b('-->'(Op,ReturnValues),Spec) :- !,
    Op =.. [OpName|Args],
    length(Args,NumberArgs),
    length(ReturnValues,NumberResults),
    Spec=bop(OpName,NumberArgs,NumberResults,Args,ReturnValues).

get_tp_specification_for_b(Transition,Spec) :-
    Transition =.. [OpName|Args],
    length(Args,NumberArgs),
    Spec=bop(OpName,NumberArgs,0,Args,[]).

get_tp_specification_for_csp(tick(_),Res) :- !, Res = csp(tick,0,[]).

get_tp_specification_for_csp(tau(_),Res) :- !, Res=csp(tau,0,[]).

get_tp_specification_for_csp(io(Vals,Channel,_Span),Res) :- !,
    length(Vals,N),
    Res = csp(Channel,N,Vals).

get_tp_specification_for_csp(A,Action) :-
    add_internal_error('Unknown CSP event: ',get_tp_specification_for_csp(A,Action)),
    Action=csp(unknown(A),0,[]).

get_tp_specification_for_csp_and_b(A,Action) :-
    % plain CSP event
    functor(A,F,_),
    member(F,[tau,io]),!,
    get_tp_specification_for_csp(A,Action).

get_tp_specification_for_csp_and_b(A,Action) :-
    get_tp_specification_for_b(A,Action).

get_transition_id(Arg,NodeId,TransId,DstId) :-
    transition(NodeId,Op,TransId,DstId),
    match_transition_with_argument(Arg,Op,NodeId,DstId).

get_transition_ids(Arg,StateIds,LTransIds) :-
    findall(TransId,(member(NodeId,StateIds),match_transition(NodeId,Arg,TransId)),LTransIds).

initialise_fairness_assumptions(Ltl,WeakFairnessArgs,StrongFairnessArgs,LtlFormula) :-
    (Ltl = fairnessimplication(FairnessFormula,LtlFormula) ->
    get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs),
    debug_println(9,get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs))
    ;
    WeakFairnessArgs = [], StrongFairnessArgs = [], LtlFormula = Ltl).

join(or(A,B),C,or(AC,BC)) :- !,
    join(A,C,AC),
    join(B,C,BC).

join(C,or(A,B),or(AC,BC)) :-
    C\=or(_,_),!,
    join(C,A,AC),
    join(C,B,BC).

join(A,B,and(A,B)) :-
    A\=or(_,_),B\=or(_,_),!.

match_ce_result([],_) :- !,fail.

match_ce_result([H|T],Result) :-
    (H = Result -> true; match_ce_result(T,Result)).

match_transition(NodeId,Arg,TransId) :-
    %% print(match_transition(NodeId,Arg,TransId)),nl,
    transition(NodeId,OpName,TransId,Dst),
    match_transition_with_argument(Arg,OpName,NodeId,Dst).

match_transition_with_argument(bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),Transition,_NodeId,_Dst) :- !,
    functor(Op,Name,NumberArgs),
    ( NumberResults == 0 ->
    Transition = Op
    ;
    Transition = '-->'(Op,ReturnValues),
    length(ReturnValues,NumberResults),
    (ReturnValues=ResPatterns -> true
    ; ltl_propositions: check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues))
    ),
    (Op =.. [_Name|ArgPatterns]; ltl_propositions: check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op)).

match_transition_with_argument(Op,Transition,NodeId,DstId) :-
    check_transition(Op,Transition,NodeId,DstId).

normalise_to_dnf(F,DNF) :-
    ex2disj(F,DNF).