--MODIFICADO, ADAPTADO AO NOVO LATEX----

\begin{zed}
  Color ::= blue | red
\end{zed}  

\begin{circus}
  \circchannel [X]gc1: \nat \cross X
\end{circus}  

\begin{circus}
  \circchannel [X]gc2: X \cross \nat
\end{circus}  

\begin{circus}
  \circchannel [X]gc3: X
\end{circus}  

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

    %\begin{circus}  
    %\circstate
    %\end{circus}
	\begin{circusaction}
    \circstate\ State ~~==~~ [~ x: \nat ~] %\land [~ y: Colour ~]
    \end{circusaction}

%    \begin{schema}{State}
%        x: \nat
%    \end{schema}

    \begin{circusaction}
        Dot \circdef gc1[Color].0.blue \then gc2[Color].red?y \then \Skip
    \end{circusaction}

    \begin{circusaction}
        Dot2 \circdef gc3[Color]?x \then \Skip
    \end{circusaction}

\begin{circusaction}
      \circspot Dot
\end{circusaction}

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

