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

\begin{circus}
    \circchannel a, b, c, ext1, ext2
\end{circus}

\begin{circus}
\circprocess SimpleAnonymous \circdef
	(xis: \nat \circspot \circbegin
    	\circstate ColourState ~~=~~ [~ x: Colour ~] \\
	    %Init1 \circdef x := blue \\
	    \circspot
	    	a \then 
	    	\Skip \\
	\circend
	) (5)
	\intchoice
	(yps: \nat \circspot \circbegin
		\circstate\ State ~~==~~ [~ y : Colour ~] \\
        %Init2 \circdef y := blue \\
		\circspot 
			b \then 
			\Skip \\
	\circend
	) (7)
\end{circus}

%\begin{circus}
%\circprocess Ann \circdef %(
%\circbegin
%	\circstate State ~~==~~ [~x : \nat~] \\
%	Zera \circdef x := 0 \\
%	Unza \circdef x := 1 \\
%	Doisa \circdef ((\circvar y : \nat \circspot (y := 5 \circseq \Skip))  ) \\
%	\circspot Unza \\
%\circend
%\end{circus}