ltl_safety

assert_aut_final_state(StateDescription) :-
    debug_println(9,asserting_finitestate(StateDescription)),
    assertz(aut_final_state(StateDescription)).

assert_aut_initial_state(StateDescription) :-
    debug_println(9,asserting_initialstate(StateDescription)),
    assertz(aut_initial_state(StateDescription)).

assert_aut_transition(Src,Atom,Dst) :-
    atom_codes(Atom,Codes),
    read_term_from_codes_exception(Codes,PrepRep,[]),
    redefine_transition_label(PrepRep,Label),
    debug_println(9,asserting_transition(aut_transition(Src,Label,Dst))),
    assertz(aut_transition(Src,Label,Dst)).

aut_state(S) :- aut_initial_state(S).

aut_state(S) :- aut_final_state(S).

basic_ap(ap(_)).

basic_ap(true).

basic_ap(false).

clear_automaton_facts :-
    retractall(aut_transition(_,_,_)),
    retractall(aut_initial_state(_)),
    retractall(aut_final_state(_)).

create_atomic_b_predicate(BPred,Res) :-
    Res = ap(bpred(BPred)).

debug_print_ba_automaton :-
    %listing(aut_initial_state/1), listing(aut_final_state/1), listing(aut_transition/3),
    (debug_mode(on)
    -> print_transitions_fail_loop
    ; true).

direct_encode_ltl_as_ba(not(false),GenAutomata) :- encode_not_globally(false,GenAutomata).

direct_encode_ltl_as_ba(not(globally(F)),GenAutomata) :- encode_not_globally(F,GenAutomata).

encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult) :-
    GenAutomata=true,direct_encode_ltl_as_ba(Ltl,GenAutomata),!,
    (ltl_formula_uses_tps(Ltl)
    -> debug_format(19,'LTL (safety) formula uses transition informations~n',[]),
    assertz(tps_occurring) % influences the way the safety mc needs to run
    ; true),
    debug_format(19,'Encoding LTL formula directly without ltl2ba~n',[]),
    Ltl1=Ltl, ExitResult=ok.

encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult) :-
    clear_automaton_facts,
    %format('LTL formula: ~w~n',[Ltl]),
    translate_to_ltl2ba_syntax(Ltl,Ltl1), % this has a side-effect of asserting tps_occurring, ... !!!!
    safe_ltl2ba_init,
    (debug_mode(on) -> Verbose = true; Verbose = false),
    c_call_ltl2ba(Ltl1,ltl_safety:assert_aut_initial_state,
    ltl_safety:assert_aut_final_state,
    ltl_safety:assert_aut_transition,Verbose,ExitResult).

encode_not_globally(implies(AP,next(NextAP)),GenAutomata) :- % formulas like G([Loop] => XX{x=0})
    translate_ap(AP,TAP),
    negate_ap(AP,NegTAP),
    negate_ap(NextAP,NegAP),
    (GenAutomata=false -> true
    ; clear_automaton_facts,
    assertz(aut_initial_state('T0_init')),
    %assertz(aut_final_state(accept_S12)), % ?? useful
    assertz(aut_final_state(accept_all)),
    assertz(aut_transition('T0_init', TAP, accept_S12)),
    assertz(aut_transition('T0_init', NegTAP, 'T0_init')),
    assertz(aut_transition('accept_S12', NegAP, accept_all)),
    assertz(aut_transition('accept_S12', NegTAP, 'T0_init')),
    assertz(aut_transition('accept_S12', TAP, accept_S12))
).

encode_not_globally(AP,GenAutomata) :- % special translation for checking LTL formula G{Pred}
    negate_ap(AP,NegAP),
    (GenAutomata=false -> true
    ; clear_automaton_facts,
    assertz(aut_initial_state('T0_init')),
    assertz(aut_final_state(accept_all)),
    assertz(aut_transition('T0_init', NegAP, accept_all)),
    assertz(aut_transition('T0_init', true, 'T0_init'))
).

get_platform_specifix_ltl2ba_library(darwin,'ltl2ba.bundle'):- !.

get_platform_specifix_ltl2ba_library(linux,'ltl2ba.so') :- !.

get_platform_specifix_ltl2ba_library(windows,'ltl2ba.dll') :- !.

get_platform_specifix_ltl2ba_library(Unknown,_) :-
    add_error_fail(translating_ltl2ba,'Unknown platform: ', Unknown).

is_atomic_proposition(F) :-
    F =.. [Functor|_Args],
    memberchk(Functor,[true,false,ap,action]).

is_ltl2ba_tool_installed :- is_ltl2ba_tool_installed(message).

is_ltl2ba_tool_installed(GenerateMsg) :-
    host_platform(Platform),
    get_platform_specifix_ltl2ba_library(Platform,File),
    absolute_file_name(prob_lib(File),LTL2BALibrary),
    (file_exists(LTL2BALibrary) ->
    debug_println(9,'LTL2BA is installed.'),
    safe_ltl2ba_init
    ; GenerateMsg==message ->
    add_message(translating_ltl2ba,
    'ltl2ba library could not be found in lib/ directory of ProB, install ltl2ba for faster model checking (see Help menu in ProB Tcl/Tk): ',LTL2BALibrary),
    fail
).

is_safety_property(not(F),NF) :-
    normalize_to_release_pnf(F,NF),
    F \= true, % not(true) corresponds to G true which is also a liveness property and
    % will lead to a warning later that there is no accept_all state
    is_syntactically_safe(NF).

is_syntactically_safe(deadlock) :- !.

is_syntactically_safe(false) :- !.

is_syntactically_safe(true) :- !.

is_syntactically_safe(ap(F)) :- F \= available(_), !. % Gavin Lowe's available operator is only treated in ltlc.pl

is_syntactically_safe(action(_)) :- !.

is_syntactically_safe(and(F,G)) :- !,
    is_syntactically_safe(F),
    is_syntactically_safe(G).

is_syntactically_safe(or(F,G)) :- !,
    is_syntactically_safe(F),
    is_syntactically_safe(G).

is_syntactically_safe(next(F)) :- !,
    is_syntactically_safe(F).

is_syntactically_safe(weakuntil(F,G)) :- !,
    is_syntactically_safe(F),
    is_syntactically_safe(G).

is_syntactically_safe(release(F,G)) :- !,
    is_syntactically_safe(F),
    is_syntactically_safe(G).

is_syntactically_safe(not(F)) :- !,
    is_atomic_proposition(F).

ltl_formula_uses_tps(globally(A)) :- !, ltl_formula_uses_tps(A).

ltl_formula_uses_tps(finally(A)) :- !, ltl_formula_uses_tps(A).

ltl_formula_uses_tps(next(A)) :- !, ltl_formula_uses_tps(A).

ltl_formula_uses_tps(until(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).

ltl_formula_uses_tps(weakuntil(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).

ltl_formula_uses_tps(release(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).

ltl_formula_uses_tps(action(_)) :- !.

ltl_formula_uses_tps(AP) :- basic_ap(AP),!, fail.

ltl_formula_uses_tps(not(AP)) :- !, ltl_formula_uses_tps(AP).

ltl_formula_uses_tps(and(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).

ltl_formula_uses_tps(or(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).

ltl_formula_uses_tps(implies(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).

ltl_formula_uses_tps(equivalent(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).

ltl_formula_uses_tps(A) :- add_internal_error('Unknown LTL property:',ltl_formula_uses_tps(A)).

ltl_mc_safety_property(Ltl,StartNodes,Result) :-
    encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult),
    debug_print_ba_automaton,
    !,
    (ExitResult = ok ->
    SMode = breadth_first, % can also be random
    start_mc_safety_property(SMode,StartNodes,Result) % uses aut_transition/3, aut_final_state/1, aut_initial_state/1 from this module
    ; ExitResult = error ->
    add_error_fail(translating_ltl2ba,'An error appeared while translating LTL to BA for the following formula: ',Ltl1)
    ;
    add_error_fail(translating_ltl2ba,'Unexpected error occurred while translating LTL to BA for the following formula: ',Ltl1)
).

ltl_mc_safety_property(_Ltl,_StarNodes,_Result) :-
    add_error_fail(translating_ltl2ba,'Please ensure that ltl2ba is installed (see Help menu in ProB Tcl/Tk)','').

negate_ap(implies(A,B),and(TA,NB)) :- translate_ap(A,TA), negate_ap(B,NB).

negate_ap(equivalent(A,B),equivalent(TA,NB)) :- translate_ap(A,TA), negate_ap(B,NB).

negate_ap(or(A,B),and(NA,NB)) :- negate_ap(A,NA), negate_ap(B,NB).

negate_ap(and(A,B),or(NA,NB)) :- negate_ap(A,NA), negate_ap(B,NB).

negate_ap(ap(Pred),not(ap(Pred))).

negate_ap(action(BOP),not(tp(BOP))).

negate_ap(not(AP),TAP) :- translate_ap(AP,TAP).

negate_ap(false,true).

normalize_to_release_pnf(deadlock,deadlock) :- !.

normalize_to_release_pnf(false,false) :- !.

normalize_to_release_pnf(true,true) :- !.

normalize_to_release_pnf(ap(P),ap(P)) :- !.

normalize_to_release_pnf(action(P),action(P)) :- !.

normalize_to_release_pnf(and(F,G),and(NF,NG)) :- !,
    normalize_to_release_pnf(F,NF),
    normalize_to_release_pnf(G,NG).

normalize_to_release_pnf(or(F,G),or(NF,NG)) :- !,
    normalize_to_release_pnf(F,NF),
    normalize_to_release_pnf(G,NG).

normalize_to_release_pnf(implies(F,G),NImplies) :- !,
    normalize_to_release_pnf(or(not(F),G),NImplies).

normalize_to_release_pnf(next(F),next(NF)) :- !,
    normalize_to_release_pnf(F,NF).

normalize_to_release_pnf(globally(F),release(false,NF)) :- !,
    normalize_to_release_pnf(F,NF).

normalize_to_release_pnf(finally(F),until(true,NF)) :- !,
    normalize_to_release_pnf(F,NF).

normalize_to_release_pnf(weakuntil(F,G),weakuntil(NF,NG)) :- !,
    normalize_to_release_pnf(F,NF),
    normalize_to_release_pnf(G,NG).

normalize_to_release_pnf(release(F,G),release(NF,NG)) :- !,
    normalize_to_release_pnf(F,NF),
    normalize_to_release_pnf(G,NG).

normalize_to_release_pnf(until(F,G),until(NF,NG)) :- !,
    normalize_to_release_pnf(F,NF),
    normalize_to_release_pnf(G,NG).

normalize_to_release_pnf(not(true),false) :- !.

normalize_to_release_pnf(not(false),true) :- !.

normalize_to_release_pnf(not(and(F,G)),NOr) :- !,
    normalize_to_release_pnf(or(not(F),not(G)),NOr).

normalize_to_release_pnf(not(or(F,G)),NAnd) :- !,
    normalize_to_release_pnf(and(not(F),not(G)),NAnd).

normalize_to_release_pnf(not(next(F)),NNext) :- !,
    normalize_to_release_pnf(next(not(F)),NNext).

normalize_to_release_pnf(not(finally(F)),NGlobally) :- !,
    normalize_to_release_pnf(release(false,not(F)),NGlobally).

normalize_to_release_pnf(not(globally(F)),NUntil) :- !,
    normalize_to_release_pnf(until(true,not(F)),NUntil).

normalize_to_release_pnf(not(until(F,G)),NRelease) :- !,
    normalize_to_release_pnf(release(not(F),not(G)),NRelease).

normalize_to_release_pnf(not(F),NF) :- !,
    (F = not(F1) ->
    normalize_to_release_pnf(F1,NF)
    ; normalize_to_release_pnf(F,NF1),
    NF=not(NF1)).

pp_ba_label(true,['true'|S],S) :- !.

pp_ba_label(false,['false'|S],S) :- !.

pp_ba_label(ap(AP),[Atom|S],S) :- !,
    pp_ap(AP,Atom).

pp_ba_label(tp(TP),[Atom|S],S) :- !,
    pp_tp(TP,Atom).

pp_ba_label(not(Pred),['! ('|S],T) :- !,
    pp_ba_label(Pred,S,[')'|T]).

pp_ba_label(and(Pred1,Pred2),['('|S],T) :- !,
    pp_ba_label(Pred1,S,[' && '| S1]),
    pp_ba_label(Pred2,S1,[')'|T]).

pp_ba_label(or(Pred1,Pred2),['('|S],T) :- !,
    pp_ba_label(Pred1,S,[' || '| S1]),
    pp_ba_label(Pred2,S1,[')'|T]).

pp_ba_label(Otherwise,['???'|S],S) :-
    add_error(printing_ba_label_for_ltl2ba,'Non-expected label: ',Otherwise).

pp_formula_to_ltl2ba_syntax(Formula,Res) :-
    pp_to_ltl2ba_syntax(Formula,Atoms,[]),
    ajoin(Atoms,Res).

pp_to_ltl2ba_syntax(true,['true'|S],S) :- !.

pp_to_ltl2ba_syntax(false,['false'|S],S) :- !.

pp_to_ltl2ba_syntax(deadlock,['deadlock'|S],S) :- !.

pp_to_ltl2ba_syntax(ap(X),[AP|S],S) :- !,
    term_hash(X,Hash),
    ajoin(['ap',Hash],AP),
    (\+ap_representation(AP,_) -> assertz(ap_representation(AP,X)); true).

pp_to_ltl2ba_syntax(action(X),[TP|S],S) :- !,
    assertz(tps_occurring),
    term_hash(X,Hash),
    ajoin(['tp',Hash],TP),
    (\+tp_representation(TP,_) -> assertz(tp_representation(TP,X)); true).

pp_to_ltl2ba_syntax(not(X),['! '|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,T).

pp_to_ltl2ba_syntax(and(X,Y),['('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[' && '|S1]),
    pp_to_ltl2ba_syntax(Y,S1,[')'|T]).

pp_to_ltl2ba_syntax(or(X,Y),['('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[' || '|S1]),
    pp_to_ltl2ba_syntax(Y,S1,[')'|T]).

pp_to_ltl2ba_syntax(implies(X,Y),['('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[' -> '|S1]),
    pp_to_ltl2ba_syntax(Y,S1,[')'|T]).

pp_to_ltl2ba_syntax(equivalent(X,Y),['('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[' <-> '|S1]),
    pp_to_ltl2ba_syntax(Y,S1,[')'|T]).

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

pp_to_ltl2ba_syntax(globally(X),['[] ('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[')'|T]).

pp_to_ltl2ba_syntax(finally(X),['<> ('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[')'|T]).

pp_to_ltl2ba_syntax(until(X,Y),['('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[' U '|S1]),
    pp_to_ltl2ba_syntax(Y,S1,[')'|T]).

pp_to_ltl2ba_syntax(release(X,Y),['('|S],T) :- !,
    pp_to_ltl2ba_syntax(X,S,[' V '|S1]),
    pp_to_ltl2ba_syntax(Y,S1,[')'|T]).

pp_to_ltl2ba_syntax(weakuntil(X,Y),S,T) :- !,
    pp_to_ltl2ba_syntax(release(or(not(X),Y),or(X,Y)),S,T).

print_label(Label) :-
    print(' --('),print(Label),print(')--> ').

print_transitions_fail_loop :-
    aut_transition(Src,Label,Dst),
    print('Transition: '),print(Src),
    translate_and_print_label(Label),
    print(Dst),nl,fail.

print_transitions_fail_loop.

read_term_from_codes_exception(Codes,PrepRep,Options) :-
    (read_term_from_codes(Codes,PrepRep,Options)
    -> true
    ; atom_codes(Atom,Codes),
    add_error(translating_ltl3ba_callback, 'Unexpected atom representation (does atom ends with fullstop?): ', Atom)
).

redefine_transition_label(true,Res) :- !,
    Res = true.

redefine_transition_label(false,Res) :- !,
    Res = false.

redefine_transition_label(not(AP),Res) :-
    ap_representation(AP,bpred(Pred)),!,
    create_negation(Pred,NegPred),
    create_atomic_b_predicate(NegPred,Res).

redefine_transition_label(AP,Res) :-
    ap_representation(AP,Rep),!,
    Res = ap(Rep).

redefine_transition_label(TP,Res) :-
    tp_representation(TP,Rep),!,
    Res = tp(Rep).

redefine_transition_label(F,Res) :-
    F =.. [Functor|Args],
    maplist(redefine_transition_label,Args,NewArgs),
    Res =.. [Functor|NewArgs].

safe_ltl2ba_init :-
    catch(ltl2ba_init,Exc,
    (add_error(translating_ltl2ba,'Exception when initialising LTL2BA (possibly wrong architecture, try reinstalling with probcli -install ltl2ba):',Exc),fail)).

safety_property_can_be_encoded_directly(F) :- direct_encode_ltl_as_ba(F,false).

translate_and_print_label(Label) :-
    pp_ba_label(Label,Atom,[]),
    ajoin(Atom,Text),
    print_label(Text).

translate_ap(action(BOP),tp(BOP)).

translate_ap(ap(Pred),ap(Pred)).

translate_ap(not(AP),NAP) :- negate_ap(AP,NAP).

translate_ap(false,false).

translate_ap(true,true).

translate_ap(implies(A,B),implies(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).

translate_ap(equivalent(A,B),equivalent(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).

translate_ap(and(A,B),and(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).

translate_ap(or(A,B),or(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).

translate_to_ltl2ba_syntax(Formula,Text) :-
    retractall(ap_representation(_,_)),
    retractall(tp_representation(_,_)),
    retractall(tps_occurring),
    pp_formula_to_ltl2ba_syntax(Formula,Text).