%%%%%%%%%%%%Begin auxiliary predicates

time(1..length).
path(1..level).
literal(F):- fluent(F).
literal(neg(F)):- fluent(F).
contrary(F, neg(F)):- fluent(F).
contrary(neg(F), F):- fluent(F).

new_branch(L, L1):-
    path(L), path(L1), L < L1.
h(F, T+1, P1):-
  	path(P), time(T), path(P1), P <= P1, sense(F),
	branch(F, T, P, P1).

used(T+1, P1):- 
  	path(P), time(T), path(P1), P <= P1, sense(F),
	branch(F, T, P, P1).

:- path(L), time(T), fluent(F), action(A),
   determines(A, F), occ(A, T, L),
   known(F, T, L).

h(G, T+1, L1):-
    time(T), path(L1), path(L), 
    literal(G),
    sense(F), L <= L1,
    branch(F, T, L, L1),
    h(G, T, L).

unknown(F, T, L):-
    path(L), time(T), fluent(F),
    not known(F, T, L).

known(F, T, L):-
    path(L), time(T), fluent(F),
    h(F, T, L).

known(F, T, L):-
    path(L), time(T), fluent(F), contrary(F, G),
    h(G, T, L).

used(1, 1).
used(T+1, L):- time(T), path(L), used(T, L).

1{occ(A, T, P) : action(A)}1:-
    time(T),
    path(P),
    used(T, P),
    not goal(T, P).

:-  time(T),  path(P),
     used(T, P),  action(A),
     occ(A,T,P), not possible(A, T, P).
%%%%% End auxiliary section

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%    Domain Description               %%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% Fluents %%%%

fluent(holding_coin).
fluent(fated_on_edge).
fluent(fated_flat).
fluent(on_edge).
fluent(flat_coin).

%%% End of Fluents %%%


% non-inertial literals



%%% Actions %%%%

action(toss_coin).
action(inspect_and_decide_coin).
action(tip_coin).

%%% End of Actions %%%


%%% Section: static causal laws %%%%
h(fated_on_edge, T, P):-  time(T), path(P),
        h(neg(fated_flat), T, P).
h(fated_flat, T, P):-  time(T), path(P),
        h(neg(fated_on_edge), T, P).

%%% End section: static causal laws %%%%

%%% Section: dynamic causal laws %%%%
h(neg(holding_coin), T+1, P):- time(T), path(P), 
        possible(toss_coin, T, P),
        occ(toss_coin,T,P), 
        h(holding_coin, T, P).
h(on_edge, T+1, P):- time(T), path(P), 
        possible(toss_coin, T, P),
        occ(toss_coin,T,P), 
        h(fated_on_edge, T, P).
h(flat_coin, T+1, P):- time(T), path(P), 
        possible(toss_coin, T, P),
        occ(toss_coin,T,P), 
        h(fated_flat, T, P).
h(flat_coin, T+1, P):- time(T), path(P), 
        possible(tip_coin, T, P),
        occ(tip_coin,T,P), 
        h(on_edge, T, P).

%%% End section: dynamic causal laws %%%%


%%% Section: Executability Conditions %%

possible(toss_coin, T, P):- time(T),path(P), 
        h(holding_coin, T, P).
possible(inspect_and_decide_coin, T, P):- time(T),path(P).
possible(tip_coin, T, P):- time(T),path(P), 
        h(on_edge, T, P).

%%% End of section: Executability Conditions %%%%


%%% Section: Abnormality of fluent %%

possibly_h(F, T, P):-
              literal(F), literal(G),
              contrary(F, G),
              time(T), path(P),
              not h(G, T, P).



ab(holding_coin, T, P):- time(T),path(P),
          occ(toss_coin, T, P), 
          possibly_h(holding_coin, T, P).

ab(neg(on_edge), T, P):- time(T),path(P),
          occ(toss_coin, T, P), 
          possibly_h(fated_on_edge, T, P).

ab(neg(flat_coin), T, P):- time(T),path(P),
          occ(toss_coin, T, P), 
          possibly_h(fated_flat, T, P).

ab(neg(flat_coin), T, P):- time(T),path(P),
          occ(tip_coin, T, P), 
          possibly_h(on_edge, T, P).

h(F, T+1, P):-
              literal(F), 
              time(T), path(P),
              h(F, T, P),
              not noninertial(F),
              literal(G), contrary(F, G),
              not h(G, T+1, P),
              not ab(F, T, P).

%%% End Section: Abnormality of fluent %%



%%% Section: Sensing Actions %%
sense(fated_on_edge).
sense(fated_flat).
branch(fated_on_edge, T, P, P):-
        time(T), path(P), possible(inspect_and_decide_coin, T, P), occ(inspect_and_decide_coin, T, P).

1{branch(fated_flat, T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(inspect_and_decide_coin, T, P), occ(inspect_and_decide_coin, T, P).

:- time(T), path(P1), path(P2),
    path(L1), P1 <= P2, L1 <= P2,
    sense(F), sense(G), neq(F,G),
    domain(F,V), domain(G,V1),
    branch(F,V,T,P1,P2),
    branch(G,V,T,L1,P2).

:- time(T), T > 1,
    path(P1), path(P2), P1 < P2,
    sense(F), domain(F,V),
    branch(F,V,T,P1,P2), used(T,P2).



determines(inspect_and_decide_coin, fated_on_edge).
determines(inspect_and_decide_coin, fated_flat).

%%% End of section: Sensing Actions %%%%


%%% Section: Initial %%

h(holding_coin, 1, 1).
h(neg(on_edge), 1, 1).
h(neg(flat_coin), 1, 1).

%%% End of section: Initial %%%%


%%% Section: Goal %%

goal(T, P):-
         time(T), path(P),
         h(flat_coin, T, P).
goal(T+1, P):-
    time(T), path(P),
    goal(T, P).

ggoal(P):- path(P), time(T), used(T, P), goal(length, P).
:- path(P), used(length, P), not ggoal(P).

%%% End of section: Goal %%%%

:-  time(T),  path(P),
    literal (P),  literal(G),
    contrary(F,G), h(F, T, P), h(G, T, P).

hide time(T).
hide path(L).
hide action(A).
hide determines(A,F).
hide contrary(F,G).
hide fluent(F).
hide literal(L).
hide unknown(F, T, L).
hide known(F, T, L).
hide used(T, L).
hide sense(F).
%hide ggoal(L).
hide goal(T,L).
hide new_branch(L, L1).
hide executable(A,S).
hide possible(A, T, L).
hide ab(F, T, L).
hide h(F, T, L).
hide noninertial(F).
hide possibly_h(F, T, L).