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

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

\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 Act_P \defs \circbegin
\end{circus}

    :: State declaration
    \begin{circus}  
    \circstate
    \end{circus}

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

    :: Skip
    \begin{circus}
        Skp \defs Skip
    \end{circus}     

    :: Stop
    \begin{circus}
        Stp \defs Stop
    \end{circus}     

    :: Chaos
    \begin{circus}
        Chs \defs Chaos
    \end{circus}     

    :: Sequential composition
    \begin{circus}
        Seq \defs (a \then Skp); (b \then Stp)
    \end{circus}     

    :: External choice
    \begin{circus}
        ExtChoice \defs 
            (\true \guard (ext1 \then Skip)) 
            \extchoice 
            (\true \guard (ext2 \then Skip))
    \end{circus}

    :: Internal choice
    \begin{circus}
        IntChoice \defs 
            (a \then Skip) 
            \intchoice 
            (b \then Skip) 
            \intchoice 
            (c \then Skip) 
    \end{circus}

    :: Parallelism with internal actions
    \begin{circus}
        Parallel \defs 
            (\circvar\ l: Colour @ (
                (x := red; l := blue) 
                    \lpar 
                        \{ x, l \} | 
                        \lchanset  \rchanset | 
                        \lchanset  \rchanset | 
                        \{ y \} 
                    \rpar 
                (y := red)
            ))
    \end{circus}

    :: Parallelism with communication.
    :: Test also if it is possible to introduce a var in an input communication
    :: with the same name as an state component.

    :: This causes: ChanUseUnificationException: Channel 'ch': Input (old), Output(new)
    begin{circus}
        ParallelComm \defs 
                (ch?x \then Skip)
                    \lpar 
                        \{ \} | 
                        \lchanset ch \rchanset | 
                        \lchanset ch \rchanset | 
                        \{ \} 
                    \rpar 
                (ch!x \then Skip)
    \end{circus}

    :: Recursive action
    \begin{circus}
        Rec \defs 
            \circvar\ loc: Colour @ 
                (\circmu X @ out!x \then out!loc \then X)
    \end{circus}

    :: Recursive actions in sequence to test if the index is being updated 
    :: properly
    \begin{circus}
        SuperRec \defs 
            (\circmu X @ (X ; (\circmu X @ X) ; X)); 
            \circmu X @ X
    \end{circus}

    :: Parameterized action definition.
    \begin{circus}
        ParamActDef \defs p: Colour @ x := p
    \end{circus}

    :: Parameterized call.
    \begin{circus}
        ParamCall \defs ParamActDef(blue)
    \end{circus}

    :: Obs: Implicit parameterized call is not yet treated by JCircus.
    begin{circus}
        ImpParamCall \defs 
            \circvar\ loc: Colour @ (
                (p: Colour @ (loc := blue; p := red; out!p \then  Skip))(x)
            )
    \end{circus}

    :: Implicit recursive parameterized call

    :: Iterated sequential composition
    \begin{circus}
        IterSeq \defs \Semi k1, k2: Colour; k3: Colour @ Skip
    \end{circus}

    :: Iterated internal choice
    \begin{circus}
        IterIntChoice \defs \Intchoice k1, k2: Colour; k3: Colour @ Skip
    \end{circus}

    :: Multiple assignment
    :: Parser does not recognize for now.
    begin{circus}
        MultAssign \defs x, y := blue, red
    \end{circus}

    :: Multiple assignment with sequential composition
    :: Parser does not recognize for now.
    begin{circus}
        MultAssignSeq \defs (x, y := blue, red);(x, y := green, yellow)
    \end{circus}

    :: If command
    \begin{circus}
        IfComm \defs 
            \circif (\true \land 1 = 1) \circthen 
                Skip
            \circelse \false \circthen 
                Stop
            \circfi
    \end{circus}

    :: Assumption
    :: Parser does not recognize for now.
    begin{circus}
        Assump \defs \{ x = blue \} x := red
    \end{circus}

\begin{circus}      
      @ Skip
\circend
\end{circus}
