--------------------------------------------------------------------------------
-- 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.
--------------------------------------------------------------------------------

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

\begin{circus}
    \circprocess LocalEnv_P \defs pp: \nat @ \circbegin
\end{circus}

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

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

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

    \begin{circus}
    Par \defs ap: \nat @ (\circvar lv: \nat @ ( 
            (pp := pp; sc := sc; ap := ap; lv := axdef)
                \lpar \{ pp, sc, ap, lv \} | \lchanset \rchanset | \lchanset \rchanset | \{  \} \rpar 
            (pp := pp; sc := sc; ap := ap; lv := lv)
    ))
    \end{circus}     

    \begin{circus}
    Rec \defs ap: \nat @ 
        (\circvar lve: \nat @
            (\circmu X @ 
                (\circvar lv: \nat @ 
                    (pp := pp; sc := sc; ap := ap; lv := lv; lve := lve; X)
                )
            )
        )
    \end{circus}     

    \begin{circus}
     SeqIte \defs ap: \nat @ 
        (\circvar lve: \nat @
            (\Semi x_1, x_2, x_3: Colour @ 
                (\circvar lv: \nat @ 
                    (pp := pp; sc := sc; ap := ap; lv := lv; lve := lve; x_1 := blue; x_2 := red; x_3 := green)
                )
            )
        )
    \end{circus}     

    \begin{circus}
     IntChoiceIte \defs ap: \nat @ 
        (\circvar lve: \nat @
            (\Intchoice x_1, x_2, x_3: Colour @ 
                (\circvar lv: \nat @ 
                    (pp := pp; sc := sc; ap := ap; lv := lv; lve := lve; x_1 := blue; x_2 := red; x_3 := green)
                )
            )
        )
    \end{circus}     

\begin{circus}      
      @ Par(0); Rec(0); SeqIte(0); IntChoiceIte(0)
\circend
\end{circus}
