ltlc

c_ltl_aptp(Formula,ApTp) :-
    c_ltl_closure(Formula,_,_,ApTp).

c_ltl_closure(Formula,Closure,Main,Atomics) :-
    %ltl_translate:pp_ltl_formula(Formula,FTxt), format('Normalising: ~w~n',[FTxt]),
    ( ltl_norm(Formula, Normalised) ->
    debug_println(normal_form(Normalised))
    ; atom(Formula) ->
    add_internal_error('ltl_norm failed for formula, be sure to pass it as term and not as atom: ',Formula),
    fail
    ;
    add_internal_error('ltl_norm failed for formula: ',Formula),
    fail),
    %ltl_translate:pp_ltl_formula(Normalised,NTxt), format('Normalised = ~w~n',[NTxt]),
    positive_closure(Normalised, PClosure),
    stripClosure(PClosure, Normalised, Main, Closure, Atomics).

c_ltl_modelcheck(Formula, Startnodes, Result, CModule:Callback) :-
    c_ltl_modelcheck(Formula, Startnodes, Result, CModule:Callback, none, none, none, [], []).

c_ltl_modelcheck(Formula, Startnodes, Result, Callback,
    Update, GetTransIdsPred, GetEnabledActionsPred, WeakFairnessArgs, StrongFairnessArgs) :-
    c_ltl_closure(Formula,Closure,Main,_),
    debug_println(9,closure(Formula,Closure,Main)),
    debug_println(9,fairness(GetTransIdsPred, WeakFairnessArgs, StrongFairnessArgs)),
    ltlc_modelcheck(Closure, Startnodes, Callback,
    Update, GetTransIdsPred, GetEnabledActionsPred, WeakFairnessArgs, StrongFairnessArgs, Main, Result).

closure(F,C) :- closure([F],[],C).

closure([],Acc,Acc).

closure([true|Rest],Acc,Closure) :-
    !,closure(Rest,Acc,Closure).

closure([F|Rest],Acc,Closure) :-
    findall(G,dclosure(F,G),Gen),
    filternew(Gen,Acc,Rest,New),
    append(Rest,New,Next),
    closure(Next,[F|Acc],Closure).

dclosure(F,Neg) :- negate(F,Neg).

dclosure(or(F,_),F).

dclosure(or(_,F),F).

dclosure(next(F),F).

dclosure(yesterday(F),F).

dclosure(not(next(F)),next(Neg)) :- negate(F,Neg).

dclosure(not(yesterday(F)),yesterday(Neg)) :- negate(F,Neg).

dclosure(until(F,_),F).

dclosure(until(_,F),F).

dclosure(until(A,B),next(until(A,B))).

dclosure(since(F,_),F).

dclosure(since(_,F),F).

dclosure(since(A,B),yesterday(since(A,B))).

deps(true,[]).

deps(not(F),[F]).

deps(ap(_),[]).

deps(or(A,B),[A,B]).

deps(next(F),D) :- (F=not(N) -> D=[next(N)]; D=[]).

deps(yesterday(F),D) :- (F=not(N) -> D=[yesterday(N)]; D=[]).

deps(until(A,B),[A,B,next(until(A,B))]).

deps(since(A,B),[A,B,yesterday(since(A,B))]).

deps(action(_),[]).

filter_parts(Ap,Tp,Next,Nextnot,Yest,Yestnot) -->
    filter_terms(Ap, ap(_)),
    filter_terms(Tp, action(_)),
    filter_terms(Nextnot, next(not(_))),
    filter_terms(Next, next(_)),
    filter_terms(Yestnot, yesterday(not(_))),
    filter_terms(Yest, yesterday(_)).

filter_terms(Filtered,Pattern,In,Out) :- filter_terms2(In,Pattern,Filtered,Out).

filter_terms2([],_,[],[]).

filter_terms2([E|Rest],Term,A,B) :-
    ( copy_term(Term, E) ->
    A=[E|ARest],B=BRest
    ;
    A=ARest,B=[E|BRest]),
    filter_terms2(Rest,Term,ARest,BRest).

filternew([],_,_,[]).

filternew([F|Rest],Ex1,Ex2,Result) :-
    (\+ member(F,Ex1), \+ member(F,Ex2)
    -> Result = [F|FRest]
    ; Result = FRest),
    filternew(Rest,Ex1,Ex2,FRest).

findref(not(F),L,neg(N)) :- !,finduref(F,L,N).

findref(F,L,pos(N)) :- finduref(F,L,N).

finduref(true,_,-1) :- !.

finduref(F,L,N) :- nth0(N,L,F).

foreign(ltlc_modelcheck,ltlc_modelcheck(+term,+term,+term,+term,+term,+term,+term,+term,+term,-term)).

foreign_resource(ltlc, [ltlc_modelcheck]).

loadfr :- (loaded -> true
    ; (assertz(loaded),
    load_foreign_resource(library(ltlc)))
).

ltl_norm(false,not(true)).

ltl_norm(and(A,B),N) :- ltl_norm(not(or(not(A),not(B))),N).

ltl_norm(implies(A,B),N) :- ltl_norm(or(not(A),B),N).

ltl_norm(equivalent(A,B),N) :- ltl_norm(and(implies(A,B),implies(B,A)),N).

ltl_norm(finally(F),N) :- ltl_norm(until(true,F),N).

ltl_norm(globally(F),N) :- ltl_norm(not(finally(not(F))),N).

ltl_norm(weakuntil(A,B),N) :- ltl_norm(or(globally(A),until(A,B)),N).

ltl_norm(release(A,B),N) :- ltl_norm(not(until(not(A),not(B))),N).

ltl_norm(once(F),N) :- ltl_norm(since(true,F),N).

ltl_norm(historically(F),N) :- ltl_norm(not(once(not(F))),N).

ltl_norm(trigger(A,B),N) :- ltl_norm(not(since(not(A),not(B))),N).

ltl_norm(true,true).

ltl_norm(next(F),next(NF)) :- ltl_norm(F,NF).

ltl_norm(yesterday(F),yesterday(NF)) :- ltl_norm(F,NF).

ltl_norm(or(A,B),or(NA,NB)) :-
    ltl_norm(A,NA),ltl_norm(B,NB).

ltl_norm(not(F),N) :- ltl_norm(F,N1), (N1=not(P) -> N=P; N=not(N1)).

ltl_norm(ap(X),N) :-
    (X=available(F) ->
    ltl_norm(available(F),N)
    ; N = ap(X)
).

ltl_norm(until(A,B),until(NA,NB)) :-
    ltl_norm(A,NA),ltl_norm(B,NB).

ltl_norm(since(A,B),since(NA,NB)) :-
    ltl_norm(A,NA),ltl_norm(B,NB).

ltl_norm(action(Op),action(Op)).

ltl_norm(fairnessimplication(_Assumptions,F),NF) :-
    ltl_norm(F,NF).

ltl_norm(available(F),N) :-
    ltl_norm(
    until( action(csp(tau,_,[])),
    or(and(ap(enabled(csp(tau,_,[]))),not(action(csp(tau,_,[])))),
    and(ap(enabled(F)),not(ap(enabled(csp(tau,_,[])))))
    )
    ),N).

ltlc_init :- loadfr.

negate(not(F),F) :- !.

negate(F,not(F)).

numeric_refs([],_,[]).

numeric_refs([F|Rest],L,[R|RRest]) :-
    xconv(F,L,R),numeric_refs(Rest,L,RRest).

positive_closure(F,NDPositive) :-
    closure(F,Closure),
    sort_closure(Closure,Sorted),
    remove_negatives(Sorted,Positive),
    remove_duplicates(Positive,NDPositive).

remove_duplicates(In,Out) :- remove_duplicates2(In,[],Out).

remove_duplicates2([],_,[]).

remove_duplicates2([E|Rest],Before,Out) :-
    ( member(E,Before) ->
    !,remove_duplicates2(Rest,Before,Out)
    ;
    Out=[E|DRest],remove_duplicates2(Rest,[E|Before],DRest)).

remove_negatives([],[]).

remove_negatives([F|Rest],Positive) :-
    (F = not(_)
    -> !,Positive = PRest
    ; Positive = [F|PRest]),
    remove_negatives(Rest,PRest).

select_formula([F|FRest],Sorted,F,FRest) :-
    deps(F,Deps),
    subset(Deps,Sorted),!.

select_formula([F|FRest],Sorted,S,[F|Rest]) :-
    select_formula(FRest,Sorted,S,Rest).

sort_closure(In,Out) :- sort_closure2(In,[],Out).

sort_closure2([],_,[]) :- !.

sort_closure2(Unsorted,Sorted,[F|RestSorted]) :-
    select_formula(Unsorted,Sorted,F,URest),
    sort_closure2(URest,[F|Sorted],RestSorted).

stripClosure(Unsorted, MainIn, MainOut, Result, Atomics) :-
    filter_parts(Ap,Tp,Next,Nextnot,Yest,Yestnot,Unsorted,Generic),
    append([Ap,Tp,Next,Nextnot,Yest,Yestnot,Generic], Sorted),
    append(Ap,Tp,Atomics),
    findref(MainIn,Sorted,MainOut),
    numeric_refs(Sorted,Sorted,Result).

subset([],_).

subset([F|Rest],Superset) :-
    (F=true;member(F,Superset)),!,subset(Rest,Superset).

xconv(ap(AP),_,ap(AP)).

xconv(action(TP),_,tp(TP)).

xconv(next(not(X)),L,nextnot(R)) :- !,finduref(X,L,R),!.

xconv(next(X),L,next(R)) :- finduref(X,L,R),!.

xconv(yesterday(not(X)),L,yesterdaynot(R)) :- !,finduref(X,L,R),!.

xconv(yesterday(X),L,yesterday(R)) :- finduref(X,L,R),!.

xconv(or(A,B),L,or(RA,RB)) :- findref(A,L,RA),findref(B,L,RB).

xconv(until(A,B),L,until(RA,RB,RN)) :-
    findref(A,L,RA),
    findref(B,L,RB),
    findref(next(until(A,B)),L,pos(RN)).

xconv(since(A,B),L,since(RA,RB,RY)) :-
    findref(A,L,RA),
    findref(B,L,RB),
    findref(yesterday(since(A,B)),L,pos(RY)).