--------------------------------------------------------------------------------
-- T_Tuna.tex

-- Ana's example.
-- Involves external choice and there is no multi-synchronization.
--------------------------------------------------------------------------------

\begin{circus}
  \circchannel tock, enter, exit, occupied, empty
\end{circus}

\begin{circus}
  \circprocess  SPACEUNLAB \defs \circbegin
\end{circus}

\begin{circus}
    EMPTY \defs (enter \then OCCUPIED) 
                \extchoice 
                (tock \then EMPTY) 
                \extchoice 
                (empty \then EMPTY)
\end{circus}

\begin{circus}
    OCCUPIED \defs (exit \then EMPTY) 
                    \extchoice 
                    (tock \then OCCUPIED) 
                    \extchoice 
                    (occupied \then OCCUPIED)
\end{circus}

\begin{circus}
    @ EMPTY
  \circend
\end{circus}