%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% domain independent axioms for GOLOG programs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
trans(P,Tb,Te):-
    time(Tb), time(Te), leq(Tb,Te),
    time(Te1), leq(Tb, Te1), leq(Te1,Te),
    proc(P),
    head(P,P1),
    trans(P1,Tb,Te1),
    tail(P,P2),
    trans(P2,Te1,Te).

trans(A,Tb,Tb+1):- time(Tb),
    action(A), neq(A, null),
    occ(A,Tb).

trans(A,Tb,Tb):- time(Tb),
    action(A),
    A = null.

trans(N,Tb,Te):- time(Tb), time(Te), leq(Tb,Te),
    choiceAction(N),
    in(P1,N),
    trans(P1,Tb,Te).

trans(F,Tb,Tb):- time(Tb),
    is_formula(F),
    hf(F,Tb).

trans(I,Tb,Te):- time(Tb), time(Te), leq(Tb,Te),
    if(I,F,P1,P2),
    hf(F,Tb),
    trans(P1,Tb,Te).

trans(I,Tb,Te):- time(Tb), time(Te), leq(Tb,Te),
    if(I,F,P1,P2),
    not hf(F,Tb),
    trans(P2,Tb,Te).

trans(W,Tb,Te):- time(Tb), time(Te), leq(Tb,Te),
    while(W,F,P),
    hf(F,Tb),
    time(Te1), leq(Tb, Te1), leq(Te1,Te),
    trans(P,Tb,Te1),
    trans(W,Te1,Te).

trans(W,Tb,Tb):- time(Tb),
    while(W,F,P),
    not hf(F,Tb).

trans(S, Tb, Te):-
    time(Tb), time(Te), leq(Tb,Te),
    choiceArgs(S,F,P),
    hf(F, Tb),
    trans(P, Tb, Te).

trans(P, Tb, Tb):-
    time(Tb),
    star(P, P1).

trans(P,Tb,Te):- time(Tb), time(Te), Tb <= Te,
    star(P, P1),
    time(Te1), Tb <= Te1, Te1 <= Te,
    trans(P1,Tb,Te1),
    trans(P,Te1,Te).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% removing some predicates from output
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

hide trans(P,T1,T2).
hide head(P,P1).
hide tail(P,P2).
hide proc(P).
hide star(P,P1).
hide choiceAction(P).
hide if(I,P,P1,P2).
hide while(W,F,P).
hide holdf(C,T).
hide choiceArgs(S,F,P).
hide conj(F).
hide disj(F).
hide negation(F,G).
hide exists(F,F1).
hide forall(F,F1).