--------------------------------------------------------------------------------
-- T_LocalEnv.tex
--
-- To test how process parameters (pp), state components (sc),
-- action parameters (ap) and local variables (lv) must be declared, initialized
-- and used in the translation of constructors that use local environments.
--
-- These variables are in the partition of one of the sides of the parallelism
-- and are not in the other.
--------------------------------------------------------------------------------

--ADAPTADO AO LATEX DO NOVO PARSER! 1.5.0!

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

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

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

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

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

    \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}
     SeqIte \circdef ap: \nat \circspot 
        (\circvar lve: \nat \circspot
            (\Semi x1, x2, x3: Colour \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: Colour \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 SeqIte(0) \circseq IntChoiceIte(0)
\end{circusaction}
\begin{circus}
\circend
\end{circus}
