--------------------------------------------------------------------------------
-- This test file is to test how process parameters (pp), state
-- components (sc), action parameters (ap) and local variables (lv) 
-- must be declared, initialized and used in an action parallelism.

-- These variables are in the partition of one of the sides of the 
-- parallelism and are not in the other.
--------------------------------------------------------------------------------

------ADAPTADO AO NOVO LATEX------

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

\begin{circus}
    \circprocess APP \circdef pp: \nat \circspot \circbegin
\end{circus}

%    \begin{circus}  
%    \circstate
%    \end{circus}

    %\begin{schema}{State}
    %    sc: \nat
    %\end{schema}
	\begin{circusaction}
    \circstate\ State ~~==~~ [~ sc: \nat ~]
    \end{circusaction}
	

    \begin{axdef}
        axdef: \nat
    \where
        axdef = 5
    \end{axdef}

%	\begin{circusaction}
%    Acao \circdef \circif axdef = 5 \circthen \Skip \circelse axdef \neq 5 
%   \circthen \Stop \circfi
%    \end{circusaction}

    \begin{circusaction}
    Par \circdef ap: \nat \circspot (\circvar lv: \nat \circspot ( 
            (pp := pp \circseq sc := sc \circseq ap := ap \circseq lv := axdef)
                \lpar \{ pp, sc, ap, lv \} 
                | \lchanset \rchanset |
                % \lchanset \rchanset | 
                \{  \} \rpar 
            (pp := pp \circseq sc := sc \circseq ap := ap \circseq lv := lv)
    ))
    \end{circusaction}

    \begin{circusaction}
    Rec \circdef ap: \nat \circspot 
        (\circvar lve: \nat \circspot
            (\circmu X \circspot 
                (\circvar lv: \nat \circspot 
                    (pp := pp \circseq sc := sc \circseq ap := ap \circseq lv
                    := lv \circseq lve := lve \circseq X) )
            )
        )
    \end{circusaction}     

    \begin{circusaction}
     ParIte \circdef ap: \nat \circspot 
        (\circvar lve: \nat \circspot
            (\Semi x1, x2, x3: Color \circspot 
                (\circvar lv: \nat \circspot 
                    (pp := pp \circseq sc := sc \circseq ap := ap \circseq lv :=
                    lv \circseq lve := lve \circseq x1 := blue \circseq x2 :=
                    red \circseq x3 := green) ) )
        )
    \end{circusaction}     

    \begin{circusaction}
     IntChoiceIte \circdef ap: \nat \circspot 
        (\circvar lve: \nat \circspot
            (\Intchoice x1, x2, x3: Color \circspot 
                (\circvar lv: \nat \circspot 
                    (pp := pp \circseq sc := sc \circseq ap := ap \circseq lv
                    := lv \circseq lve := lve \circseq x1 := blue \circseq x2
                    := red \circseq x3 := green) ) )
        )
    \end{circusaction}     

\begin{circusaction}      
      \circspot Par(0) \circseq Rec(0) \circseq ParIte(0) \circseq
      IntChoiceIte(0)
\end{circusaction}

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