--------------------------------------------------------------------------------
-- T_Act.tex

-- Tests translation rules for actions.
--------------------------------------------------------------------------------

---ADAPTADO AO LATEX DO NOVO PARSER---

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

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

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

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

	%\begin{schema}{State}
        %\circstate
    %    x, y: Colour
	%\end{schema}
	\begin{circusaction}
    \circstate\ State ~~==~~ [~ x, y: Colour ~]
    \end{circusaction}

    \begin{circusaction}
		Porr \circdef x := red
    \end{circusaction}

    \begin{circusaction}
        Skp \circdef \Skip
    \end{circusaction}

    \begin{circusaction}
        Stp \circdef \Stop
    \end{circusaction}

    \begin{circusaction}
        Chs \circdef \Chaos
    \end{circusaction}     

    \begin{circusaction}
        Seq \circdef (a \then Skp) \circseq (b \then Stp)
    \end{circusaction}

%        ExtChoice \defs
%            (\true \guard (ext1 \then Skip)) 
%            \extchoice 
%            (\true \guard (ext2 \then Skip))
    \begin{circusaction}
        ExtChoice \circdef
            (\lcircguard true \rcircguard \circguard ext1 \then \Skip)
            \extchoice
            (\lcircguard true \rcircguard \circguard ext2 \then \Skip)
    \end{circusaction}

    \begin{circusaction}
        IntChoice \circdef 
            (a \then \Skip) 
            \intchoice
            (b \then \Skip) 
            \intchoice
            (c \then \Skip) 
    \end{circusaction}

    \begin{circusaction}
        Parallel \circdef 
            (\circvar\ l: Colour \circspot (
                (x := red \circseq l := blue)
                    \lpar 
                        \{ x, l \} | 
                        \lchanset  \rchanset | 
%                        \lchanset  \rchanset | 
                        \{ y \} 
                    \rpar 
                (y := red)
            ))
    \end{circusaction}

    \begin{circusaction}
        Rec \circdef
            \circvar\ loc: Colour \circspot 
                (\circmu X \circspot out!x \then out!loc \then X)
    \end{circusaction}

    \begin{circusaction}
        SuperRec \circdef
            (\circmu X \circspot (X \circseq (\circmu X \circspot X) \circseq
            X)) \circseq \circmu X \circspot X
    \end{circusaction}

    \begin{circusaction}
        ParamActDef \circdef p: Colour \circspot x := p
    \end{circusaction}

    \begin{circusaction}
        ParamCall \circdef ParamActDef(blue)
    \end{circusaction}

    \begin{circusaction}
        IterSeq \circdef \Semi k1, k2: Colour; k3: Colour \circspot \Skip
    \end{circusaction}

    \begin{circusaction}
        IterIntChoice \circdef \Intchoice k1, k2: Colour; k3: Colour \circspot \Skip
    \end{circusaction}

    \begin{circusaction}
        IfComm \circdef
            \circif (true \land 1 = 1) \circthen 
                \Skip
            \circelse false \circthen 
                \Stop
            \circfi
    \end{circusaction}

\begin{circusaction}
      \circspot \Skip
\end{circusaction}

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