--AINDA NÃO TERMINADA A ADAPTAÇÃO, TEM O LANCE DOS PARÊNTESES ESTRANHOS ANTES
--DE circbegin e circend

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

\begin{circus}
    \circchannel in, out: Colour
\end{circus}

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

\begin{circus}
  \circchannel d: \nat \cross \nat
\end{circus}

\begin{circus}
  \circchannelset cs == \lchanset a, b, c \rchanset
\end{circus}

\begin{circus}  
    \circprocess SimpleP \circdef pp: Colour \circspot \circbegin
    %\begin{circus}  
    %\circstate
    %end{circus}

    %\begin{schema}{State}
    %    x: Colour \\
    %    y: Colour
    %\end{schema}

    \circstate\ State ~~==~~ [~ x, y: Colour ~] \\
    Init \circdef x := blue \\
	A \circdef (\circvar\ y: Colour \circspot (y := blue \circseq out!y \then in?x
	\then \Skip)) \\
	
	B \circdef \circif (true \land 1 = 1) \circthen A \circelse false \circthen
    A \circfi \\
    
    Parallel \circdef (\circvar\ l: Colour \circspot ((x := red
    \circseq l := blue) \lpar \{ x, l \}
        %| \lchanset in, out \rchanset 
        | \lchanset in, out \rchanset 
        | \{ y \} \rpar (y := red))) \\
        Recursive \circdef \circvar\ loc: Colour \circspot (\circmu X \circspot
        out!x \then out!loc \then X) \\
    
    SuperRecursion \circdef (\circmu X \circspot (X \circseq (\circmu X
        \circspot X) \circseq X)) \circseq \circmu X \circspot X \\
    
%    :: Problema com o CallAction no novo framework.
    Instantiation \circdef 
    (
    \circvar loc: Colour
    \circspot 
    (
    (
    par: Colour
        \circspot
        (
        %loc := blue \circseq
        par := red \circseq out!par \then \Skip
        )
     )
     (x)
     )
     )
      \\
    
    IntChoice \circdef (a \then \Skip) \intchoice (b \then \Skip) \intchoice (c
    \then \Skip) \\

    ExtChoice \circdef (\lcircguard true \rcircguard \circguard (ext1 \then
    \Skip)) \extchoice (\lcircguard true \rcircguard \circguard (ext2 \then \Skip)) \\

    IterSeqAction \circdef \Semi k1, k2: Colour ; k3: Colour \circspot \Skip \\

    IterIntChoiceAction \circdef \Intchoice k1, k2: Colour ; k3: Colour
    \circspot \Skip \\
	
    ParAction \circdef y: Colour \circspot out!y \then \Skip \\

    Multisync \circdef d.0.1 \then \Skip \\

    \circspot ExtChoice \\
\circend
\end{circus}
\begin{circus}  
    \circprocess SimpleInstP \circdef SimpleP(blue) 
\end{circus}
        :: Problema com o CallProcess no novo framework.
%        begin{circus}
%            \circprocess SimpleInstP2 \circdef (y: Colour \circspot
%           SimpleInstP) (blue)
%        \end{circus}

\begin{circus}  
    \circprocess SimpleIntChoiceP \circdef SimpleInstP \intchoice SimpleInstP \intchoice (SimpleP(blue))
\end{circus}

        :: Parser nao reconhece
%        begin{circus}  
%            \circprocess SimpleRenameP \circdef SimpleInstP [out, in := rOut,
%            rIn]
%        \end{circus}

:: More than one writer in the paralelism. Must give an error message.
%\begin{circus}  
%    \circprocess SimpleParalP \circdef SimpleInstP \lpar \lchanset a, b, c
%    \rchanset \rpar SimpleInstP
%\end{circus}

\begin{circus}
    \circprocess SimpleIterSeqP \circdef \Semi k1, k2: Colour ; k3: Colour
    \circspot (SimpleP(k1))
\end{circus}

\begin{circus}  
    \circprocess SimpleIterIntChoiceP \circdef \Intchoice k1, k2: Colour ; k3:
    Colour \circspot SimpleInstP
\end{circus}

\begin{circus}
    \circprocess SimpleIterParallelP \circdef \Parallel k: Colour \lpar \lchanset in \rchanset \rpar \circspot SimpleP(k)
\end{circus}

\begin{circus}  
    \circprocess SimpleHidingP \circdef SimpleInstP \circhide \lchanset a
    \rchanset
\end{circus}

%:: This was only a test for the typechecker. Process 'NotDeclared'
%:: has not been declared!
%begin{circus}  
%    \circprocess Test \circdef SimpleHidingP \intchoice NotDeclared
%\end{circus}

%:: Elaborar estrategia para tratar de processos anonimos
\begin{circus}
\circprocess SimpleAnonymous \circdef 
	(\circbegin
%    	\circstate State ~~=~~ [~x1: Colour~] \\
%	    Init1 \circdef x1 := blue \\
	    \circspot 
	    	a \then 
	    	\Skip \\
	\circend
	)
	\intchoice
	(\circbegin
%		\circstate\ State ~~==~~ [~ x2 : Colour ~] \\
%       Init2 \circdef x2 := blue \\
		\circspot 
			b \then 
			\Skip \\
	\circend
	)
\end{circus}
