\section{First Past the Post Voting Protocol}
\label{sec:fptp}

\begin{verbatim}
nat : type.
z : nat.
s nat : nat.

candidate : type.
elected candidate : pred.
defeated candidate : pred.
ballot candidate : pred.
hopeful candidate nat : pred.

stage count = {
  count_ballot : ballot C * hopeful C N -o hopeful C (s N).
}

- : qui * stage count -o stage pick * max z.

lt nat nat : bwd.
lt/z : lt z (s N).
lt/s : lt (s N) (s M)
      <- lt N M.

max nat : pred.

stage pick = {
  increase : max N * hopeful C N' * lt N N'  
               -o hopeful C N' * max N'.
  eliminate : max N * hopeful C N' * lt N' N
               -o max N * !defeated C.
}

- : qui * stage pick * hopeful C N -o stage done * !elected C.

stage done = {
  cleanup : max _ -o ().
}

% domain instantiation
alice : candidate.
bob : candidate.
charlie : candidate.

context init =
{ballot alice, ballot alice, ballot charlie, ballot bob,
ballot bob, ballot alice,
hopeful alice z,
hopeful bob z,
hopeful charlie z }.

#trace _ count init.
\end{verbatim}

\section{Sokoban}
\label{sec:sokoban}

\begin{verbatim}
layer : type.
location : type.
entity : type.
direction : type.
intention : type.

% Instantiations that exist for every game
player : entity.
 
go direction : intention.
x : intention.
stationary : intention.
 
right : direction.
left : direction.
up : direction.
down : direction.
 
available intention : bwd.
available/left : available (go left).
available/right : available (go right).
available/down : available (go down).
available/up : available (go up).
available/x : available x.

% Persistent facts
adjacent location direction location : bwd.
 
% Game state that exists for every game
at layer location entity intention : pred.
empty layer location : pred.
turn : pred.
 
% Game-specific terms and state
crate : entity.
 
stage impartIntentions = {
  press_arrow : 
    turn
      * available Intent
      * at Layer Loc player _
    -o at Layer Loc player Intent.
}
#interactive impartIntentions.
qui * stage impartIntentions -o stage processIntentions * turn.
 
% this is the part written by the game author in PuzzleScript
stage processIntentions = {
  % propagate player intention to crate
  push_crate : 
    turn *
    $at Layer Loc player (go Dir) * adjacent Loc Dir Loc'
      * at Layer Loc' crate _
    -o at Layer Loc' crate (go Dir).
}
qui * stage processIntentions -o stage carryOutIntentions.

% resolve intentions in a nondeterministic order.
stage carryOutIntentions = {
  move :
    at Layer L Ent (go Dir) * adjacent L Dir L'
       * empty Layer L' -o at Layer L' Ent stationary * empty Layer L.
}
qui * stage carryOutIntentions -o stage cleanup.

% friction! otherwise stuff w/intent to move would keep moving...
stage cleanup = {
  spare_turns : turn -o ().
  friction : at Layer L Ent (go Dir) -o at Layer L Ent stationary.
}
qui * stage cleanup -o stage impartIntentions * turn.

% layer/level definitions
bg : layer.
fg : layer.

cell00 : location.
cell01 : location.
cell02 : location.
cell10 : location.
cell11 : location.
cell12 : location.
cell20 : location.
cell21 : location.
cell22 : location.
 
% 00 01 02
adjacent cell00 right cell01.
adjacent cell01 left cell00.
adjacent cell01 right cell02.
adjacent cell02 left cell01.
adjacent cell00 down cell10.

% 10 11 12
adjacent cell10 up cell00.
adjacent cell10 right cell11.
adjacent cell11 left cell10.
adjacent cell11 up cell01.
adjacent cell01 down cell11.
adjacent cell11 right cell12.
adjacent cell12 left cell11.
adjacent cell12 up cell02.
adjacent cell02 down cell12.
 
% 20 21 22
adjacent cell10 down cell20.
adjacent cell20 up cell10.
adjacent cell20 right cell21.
adjacent cell21 left cell20.
adjacent cell21 up cell11.
adjacent cell11 down cell21.
adjacent cell21 right cell22.
adjacent cell22 left cell21.
adjacent cell22 up cell12.
adjacent cell12 down cell22.

context init =
{ turn,
  at fg cell00 player stationary,
  at fg cell01 crate stationary,
  empty fg cell02,
  empty fg cell10,
  empty fg cell11,
  empty fg cell12,
  empty fg cell20,
  empty fg cell21,
  empty fg cell22}.
 
#trace _ impartIntentions init.
\end{verbatim}

\section{Tower of Hanoi}
\label{sec:hanoi}

\begin{verbatim}
ring : type.
smaller ring ring : bwd.

place : type.
post : type.
top_of ring : place.
bottom post : place.
post : place.

on ring place : pred.
clear place : pred.
arm_free : pred.
arm_holding ring : pred.

stage do = {
pickup 
  : clear (top_of R) * on R P * arm_free -o arm_holding R * clear P.

putdown_on_ring
  : arm_holding R * clear (top_of R') * smaller R R'
      -o arm_free * on R (top_of R') * clear (top_of R).

putdown_on_post
  : arm_holding R * clear (bottom P)
      -o arm_free * on R (bottom P) * clear (top_of R).
}
#interactive do.

% domain instantiation

p1 : post.
p2 : post.
p3 : post.

r1 : ring. 
r2 : ring.
r3 : ring.

smaller r1 r2.
smaller r1 r3.
smaller r2 r3.

context init =
{clear (bottom p2), clear (bottom p3),
    on r3 (bottom p1),
    on r2 (top_of r3),
    on r1 (top_of r2), 
    clear (top_of r1),
    arm_free}.

#trace _ do init.
\end{verbatim}


