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

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

--ADAPTADO AO LATEX DO NOVO PARSER, 1.5.0 CZT

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

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

\begin{circusaction}
    EMPTY \circdef (enter \then OCCUPIED) 
                \extchoice 
                (tock \then EMPTY) 
                \extchoice 
                (empty \then EMPTY)
\end{circusaction}

\begin{circusaction}
    OCCUPIED \circdef (exit \then EMPTY) 
                    \extchoice 
                    (tock \then OCCUPIED) 
                    \extchoice 
                    (occupied \then OCCUPIED)
\end{circusaction}

\begin{circusaction}
    \circspot EMPTY
\end{circusaction}

\begin{circus}
  \circend
\end{circus}