ltl_translate

get_arg(N/Arg,Arg) :- nonvar(N),!.

get_arg(Arg,Arg).

get_ltl_sub_formulas(and(A,B),'&',[A,B]).

get_ltl_sub_formulas(or(A,B),'or',[A,B]).

get_ltl_sub_formulas(implies(A,B),'=>',[A,B]).

get_ltl_sub_formulas(equivalent(A,B),'<=>',[A,B]).

get_ltl_sub_formulas(until(A,B),'U',[A,B]).

get_ltl_sub_formulas(weakuntil(A,B),'W',[A,B]).

get_ltl_sub_formulas(release(A,B),'R',[A,B]).

get_ltl_sub_formulas(since(A,B),'S',[A,B]).

get_ltl_sub_formulas(globally(A),'G',[A]).

get_ltl_sub_formulas(finally(A),'F',[A]).

get_ltl_sub_formulas(not(A),'not',[A]).

get_ltl_sub_formulas(next(A),'X',[A]).

get_ltl_sub_formulas(yesterday(A),'Y',[A]).

get_ltl_sub_formulas(historically(A),'H',[A]).

get_ltl_sub_formulas(once(A),'O',[A]).

pp_ap(bpred(B),PP) :- !,
    translate_bexpression(B,PP1),
    ajoin(['{',PP1,'}'],PP).

pp_ap(xtl_predicate_check(P),PP) :- atom(P),!,
    ajoin(['{',P,'}'],PP).

pp_ap(enabled(TP),PP) :- !,
    pp_tp2(TP,TPP),
    ajoin(['e(',TPP,')'],PP).

pp_ap(available(TP),PP) :- !, % TO DO: check_ap currently has no rule for Av(.) / available Operator !!
    % Was introduced for David Williams.
    % Only relevant for CSP and rewritten to [tau] U (e(tau) & not [tau]) or (e(a) & not e(tau))).
    % This is done in the Prolog module with the C interface for LTL.
    pp_tp2(TP,TPP),
    ajoin(['Av(',TPP,')'],PP).

pp_ap(weak_fair(TP),PP) :- !,
    pp_tp2(TP,TPP),
    ajoin(['WF(',TPP,')'],PP).

pp_ap(strong_fair(TP),PP) :- !,
    pp_tp2(TP,TPP),
    ajoin(['SF(',TPP,')'],PP).

pp_ap(dlk(L),PP) :- !,
    maplist(pp_tp2,L,S),
    tools: ajoin_with_sep(S,',',SText),
    ajoin(['deadlock(',SText,')'],PP).

pp_ap(ctrl(L),PP) :- !,
    maplist(pp_tp2,L,S),
    tools: ajoin_with_sep(S,',',SText),
    ajoin(['controller(',SText,')'],PP).

pp_ap(det(L),PP) :- !,
    maplist(pp_tp2,L,S),
    tools: ajoin_with_sep(S,',',SText),
    ajoin(['deterministic(',SText,')'],PP).

pp_ap(Expr,PP) :-
    write_to_codes(Expr,Codes),
    atom_codes(PP,Codes).

pp_comp(eq,unchanged).

pp_comp(neq,changed).

pp_comp(lt,increasing).

pp_comp(gt,decreasing).

pp_formula(ap(AP),ap(PP)) :-
    pp_ap(AP,PP).

pp_formula(action(AP),tp(PP)) :-
    pp_tp(AP,PP).

pp_formulas([],[]).

pp_formulas([ApTp|Rest],[PP|PPrest]) :-
    (pp_formula(ApTp,PP) -> true ; PP = '???'),
    pp_formulas(Rest,PPrest).

pp_ltl(true,['true'|S],S).

pp_ltl(false,['false'|S],S).

pp_ltl(deadlock,['deadlock'|S],S).

pp_ltl(sink,['sink'|S],S).

pp_ltl(goal,['goal'|S],S).

pp_ltl(state_error,['error'|S],S).

pp_ltl(det_output,['det_output'|S],S).

pp_ltl(current,['current'|S],S).

pp_ltl(globally(F),['G ('| S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(finally(F),['F ('| S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(next(F),['X ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(yesterday(F),['Y ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(since(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' S '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(once(F),['O ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(historically(F),['H ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(until(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' U '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(weakuntil(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' W '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(release(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' R '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(implies(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' => '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(equivalent(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' <=> '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(fairnessimplication(FairAssump,Formula),['('|S],T) :- !,
    pp_ltl_fairness(FairAssump,S,[' => '| S1]),
    pp_ltl(Formula,S1,[')'|T]).

pp_ltl(or(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' or '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(and(F,G),['('|S],T) :- !,
    pp_ltl(F,S,[' & '| S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl(not(F),['not('| S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(ap(AP),[Pred|S],S) :- !, pp_ap(AP,Pred).

pp_ltl(action(A),[Action|S],S) :- !, pp_tp(A,Action).

pp_ltl(ena(F),['EX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(en(F), ['EX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(an(F), ['AX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(eg(F), ['EG ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(ef(F), ['EF ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(ag(F), ['AG ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(af(F), ['AF ('|S],T) :- !, pp_ltl(F,S,[')'|T]).

pp_ltl(eu(F,G), ['( E '|S],T) :- !,
    pp_ltl(F,S,[' U '|S1]),
    pp_ltl(G,S1,[')'|T]).

pp_ltl_fairness(strongassumptions(F),S1,T) :- !,
    (F=all ->
    S1 = ['SEF'|S], T = S
    ;
    S1 = ['('|S], pp_ltl_fairness1(F,S,[')'|T])
).

pp_ltl_fairness(weakassumptions(F),S1,T) :- !,
    (F=all ->
    S1 = ['WEF'|S], T = S
    ;
    S1 = ['('|S], pp_ltl_fairness1(F,S,[')'|T])
).

pp_ltl_fairness(and(F,G),S,T) :- !,
    pp_ltl_fairness(F,S,[' & '|S1]),
    pp_ltl_fairness(G,S1,T).

pp_ltl_fairness1(and(F,G),['('|S],T) :- !,
    pp_ltl_fairness1(F,S,[' & '|S1]),
    pp_ltl_fairness1(G,S1,[')'|T]).

pp_ltl_fairness1(or(F,G),S,T) :- !,
    pp_ltl_fairness1(F,S,[' or '|S1]),
    pp_ltl_fairness1(G,S1,T).

pp_ltl_fairness1(ap(AP),[Pred|S],S) :- !,
    pp_ap(AP,Pred).

pp_ltl_formula(Formula,Text) :-
    pp_ltl(Formula,Atoms,[]),
    ajoin(Atoms,Text).

pp_op(Id,PP) :-
    transition(_Src,Action,Id,_Dst),!,
    translate_event(Action,PP).

pp_tp(change_expr(Comparator,TE),PP) :-
    pp_comp(Comparator,PPC), !,
    translate_bexpression(TE,TPP),
    ajoin([PPC,'({',TPP,'})'],PP).

pp_tp(before_after(TE),PP) :-
    !,
    translate_bexpression(TE,TPP),
    ajoin(['BA({',TPP,'})'],PP).

pp_tp(T,PP) :-
    pp_tp2(T,PP1),
    ajoin(['[',PP1,']'],PP).

pp_tp2(btrans(event(Name)),Name) :- !.

pp_tp2(btrans(event(Name,Predicate,_)),PP) :- !,
    translate_bexpression(Predicate,PP1),
    ajoin([Name,' | ',PP1],PP).

pp_tp2(csp(tau,_Arity,[]),PP) :- !, PP = tau.

pp_tp2(csp(tick,_Arity,[]),PP) :- !, PP = tick.

pp_tp2(xtl(Op,0,[]),PP) :- !, PP = Op.

pp_tp2(xtl(Op,_Arity,PatternArgs),PP) :- !, Term =.. [Op|PatternArgs], pp_tp2(Term,PP).

pp_tp2(Action,PP) :-
    translate_action(Action,PP),!.

pp_tp2(F,AF) :-
    (translate: translate_event(F,AF) -> true; AF='???').

translate_action(bop(Name,_NumberArgs,_NumberResults,ArgPatterns,_ResPatterns),Transition) :- !,
    maplist(get_arg,ArgPatterns,ArgPatterns1),
    maplist(translate_bexpression,ArgPatterns1,PPArgPatterns),
    Op =.. [Name|PPArgPatterns],
    Transition = Op.

translate_action(csp(Channel,_Arity,Args),PP) :-
    (csp_with_bz_mode ->
    % in this mode we need to remove 'CSP:'
    translate: translate_event2(io(Args,Channel,_SPan),[_|S],[])
    ;
    translate: translate_event2(io(Args,Channel,_SPan),S,[])
    ), ajoin(S,PP).