%%%%%%%%%%%%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(w(1)).
fluent(w(2)).
fluent(w(3)).
fluent(w(4)).
fluent(holding_coin).
fluent(fated_on_edge).
fluent(on_edge).
fluent(fated_heads_up).
fluent(heads_up).
fluent(fated_tails_up).
fluent(tails_up).
fluent(error).
fluent(fated_flat).
fluent(flat_coin).
fluent(fated_tips_heads).
fluent(fated_tips_tails).

%%% End of Fluents %%%


% non-inertial literals



%%% Actions %%%%

action(toss_coin).
action(examine_flatness).
action(examine_side_up).
action(tip_coin).
action(turn_over).
action(init).

%%% End of Actions %%%


%%% Section: static causal laws %%%%
h(neg(fated_heads_up), T, P):-  time(T), path(P),
        h(w(1), T, P).
h(neg(fated_tails_up), T, P):-  time(T), path(P),
        h(w(1), T, P).
h(fated_on_edge, T, P):-  time(T), path(P),
        h(w(1), T, P).
h(fated_tips_tails, T, P):-  time(T), path(P),
        h(w(1), T, P).
h(neg(fated_heads_up), T, P):-  time(T), path(P),
        h(w(2), T, P).
h(neg(fated_tails_up), T, P):-  time(T), path(P),
        h(w(2), T, P).
h(fated_on_edge, T, P):-  time(T), path(P),
        h(w(2), T, P).
h(fated_tips_heads, T, P):-  time(T), path(P),
        h(w(2), T, P).
h(fated_heads_up, T, P):-  time(T), path(P),
        h(w(3), T, P).
h(neg(fated_tails_up), T, P):-  time(T), path(P),
        h(w(3), T, P).
h(neg(fated_on_edge), T, P):-  time(T), path(P),
        h(w(3), T, P).
h(neg(fated_tips_tails), T, P):-  time(T), path(P),
        h(w(3), T, P).
h(neg(fated_tips_heads), T, P):-  time(T), path(P),
        h(w(3), T, P).
h(fated_tails_up, T, P):-  time(T), path(P),
        h(w(4), T, P).
h(neg(fated_heads_up), T, P):-  time(T), path(P),
        h(w(4), T, P).
h(neg(fated_on_edge), T, P):-  time(T), path(P),
        h(w(4), T, P).
h(neg(fated_tips_tails), T, P):-  time(T), path(P),
        h(w(4), T, P).
h(neg(fated_tips_heads), T, P):-  time(T), path(P),
        h(w(4), 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(heads_up, T+1, P):- time(T), path(P), 
        possible(toss_coin, T, P),
        occ(toss_coin,T,P), 
        h(fated_heads_up, T, P).
h(flat_coin, T+1, P):- time(T), path(P), 
        possible(toss_coin, T, P),
        occ(toss_coin,T,P), 
        h(fated_heads_up, T, P).
h(flat_coin, T+1, P):- time(T), path(P), 
        possible(toss_coin, T, P),
        occ(toss_coin,T,P), 
        h(fated_tails_up, T, P).
h(tails_up, T+1, P):- time(T), path(P), 
        possible(toss_coin, T, P),
        occ(toss_coin,T,P), 
        h(fated_tails_up, 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), 
        h(fated_tips_heads, T, P).
h(neg(on_edge), T+1, P):- time(T), path(P), 
        possible(tip_coin, T, P),
        occ(tip_coin,T,P), 
        h(on_edge, T, P), 
        h(fated_tips_heads, T, P).
h(heads_up, T+1, P):- time(T), path(P), 
        possible(tip_coin, T, P),
        occ(tip_coin,T,P), 
        h(on_edge, T, P), 
        h(fated_tips_heads, 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), 
        h(fated_tips_tails, T, P).
h(neg(on_edge), T+1, P):- time(T), path(P), 
        possible(tip_coin, T, P),
        occ(tip_coin,T,P), 
        h(on_edge, T, P), 
        h(fated_tips_tails, T, P).
h(tails_up, T+1, P):- time(T), path(P), 
        possible(tip_coin, T, P),
        occ(tip_coin,T,P), 
        h(on_edge, T, P), 
        h(fated_tips_tails, T, P).
h(error, T+1, P):- time(T), path(P), 
        possible(tip_coin, T, P),
        occ(tip_coin,T,P), 
        h(neg(on_edge), T, P).
h(tails_up, T+1, P):- time(T), path(P), 
        possible(turn_over, T, P),
        occ(turn_over,T,P), 
        h(heads_up, T, P).
h(neg(heads_up), T+1, P):- time(T), path(P), 
        possible(turn_over, T, P),
        occ(turn_over,T,P), 
        h(heads_up, T, P).
h(heads_up, T+1, P):- time(T), path(P), 
        possible(turn_over, T, P),
        occ(turn_over,T,P), 
        h(tails_up, T, P).
h(neg(tails_up), T+1, P):- time(T), path(P), 
        possible(turn_over, T, P),
        occ(turn_over,T,P), 
        h(tails_up, T, P).
h(error, T+1, P):- time(T), path(P), 
        possible(turn_over, T, P),
        occ(turn_over,T,P), 
        h(neg(tails_up), T, P), 
        h(neg(heads_up), 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(examine_flatness, T, P):- time(T),path(P).
possible(examine_side_up, T, P):- time(T),path(P).
possible(tip_coin, T, P):- time(T),path(P), 
        h(on_edge, T, P).
possible(turn_over, T, P):- time(T),path(P).
possible(init, T, P):- time(T),path(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(on_edge, T, P):- time(T),path(P),
          occ(tip_coin, T, P), 
          possibly_h(on_edge, T, P), 
          possibly_h(fated_tips_heads, T, P).

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

ab(neg(heads_up), T, P):- time(T),path(P),
          occ(toss_coin, T, P), 
          possibly_h(fated_heads_up, T, P).

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

ab(neg(heads_up), T, P):- time(T),path(P),
          occ(turn_over, T, P), 
          possibly_h(tails_up, T, P).

ab(heads_up, T, P):- time(T),path(P),
          occ(turn_over, T, P), 
          possibly_h(heads_up, T, P).

ab(neg(tails_up), T, P):- time(T),path(P),
          occ(toss_coin, T, P), 
          possibly_h(fated_tails_up, T, P).

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

ab(neg(tails_up), T, P):- time(T),path(P),
          occ(turn_over, T, P), 
          possibly_h(heads_up, T, P).

ab(tails_up, T, P):- time(T),path(P),
          occ(turn_over, T, P), 
          possibly_h(tails_up, T, P).

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

ab(neg(error), T, P):- time(T),path(P),
          occ(turn_over, T, P), 
          possibly_h(neg(tails_up), T, P), 
          possibly_h(neg(heads_up), T, P).

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

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

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

ab(neg(flat_coin), T, P):- time(T),path(P),
          occ(tip_coin, T, P), 
          possibly_h(on_edge, T, P), 
          possibly_h(fated_tips_tails, 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(flat_coin).
sense(on_edge).
branch(flat_coin, T, P, P):-
        time(T), path(P), possible(examine_flatness, T, P), occ(examine_flatness, T, P).

1{branch(on_edge, T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(examine_flatness, T, P), occ(examine_flatness, T, P).
sense(heads_up).
sense(tails_up).
branch(heads_up, T, P, P):-
        time(T), path(P), possible(examine_side_up, T, P), occ(examine_side_up, T, P).

1{branch(tails_up, T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(examine_side_up, T, P), occ(examine_side_up, T, P).
sense(w(1)).
sense(w(2)).
sense(w(3)).
sense(w(4)).
branch(w(1), T, P, P):-
        time(T), path(P), possible(init, T, P), occ(init, T, P).

1{branch(w(2), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(init, T, P), occ(init, T, P).
1{branch(w(3), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(init, T, P), occ(init, T, P).
1{branch(w(4), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(init, T, P), occ(init, 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(examine_flatness, flat_coin).
determines(examine_flatness, on_edge).
determines(examine_side_up, heads_up).
determines(examine_side_up, tails_up).
determines(init, w(1)).
determines(init, w(2)).
determines(init, w(3)).
determines(init, w(4)).

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


%%% Section: Initial %%

h(holding_coin, 1, 1).
h(neg(error), 1, 1).
h(neg(on_edge), 1, 1).
h(neg(flat_coin), 1, 1).
h(neg(tails_up), 1, 1).
h(neg(heads_up), 1, 1).

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


%%% Section: Goal %%

goal(T, P):-
         time(T), path(P),
         h(flat_coin, T, P),
         h(heads_up, T, P),
         h(neg(error), 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).