--------------------------------------------------------------------------------
-- T_Proc.tex

-- Tests translation rules for compound processes.
--------------------------------------------------------------------------------

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

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

:: Basic process definition
\begin{circus}  
    \circprocess Proc_P \defs \circbegin
\end{circus}

\begin{circus}      
      @ in?x \then out!x \then Skip
\circend
\end{circus}

:: Basic parameterized process definition
\begin{circus}  
    \circprocess Proc_Q \defs p1: \nat; p2: Colour @ \circbegin
\end{circus}

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

:: Process call
\begin{circus}  
    \circprocess Proc_Call \defs Proc_P
\end{circus}

:: Parameterized call
\begin{circus}  
    \circprocess Proc_ParamCall \defs Proc_Q (1, red)
\end{circus}

:: Implicit parameterized call. 
:: JCircus does not deal with this yet.
begin{circus}  
    \circprocess Proc_ImpParamCall \defs (p: Colour; n: \nat @ Proc_P) (blue, 0) 
\end{circus}

:: Generic instantiation

:: Generic instantiation and parameterized call

:: Sequential composition
\begin{circus}  
    \circprocess Proc_Seq \defs 
            Proc_P; Proc_Q(1, blue)
\end{circus}

:: External choice

:: Internal choice
\begin{circus}  
    \circprocess Proc_IntChoiceP \defs 
            Proc_P 
                \intchoice 
            Proc_Q(0, blue) 
                \intchoice 
            Proc_Seq
\end{circus}

:: Channel renaming
:: Parser does not accept.
begin{circus}  
    \circprocess Proc_ChanRename \defs Proc_P [out, in := rOut, rIn]
\end{circus}


:: Parallelism

\begin{circus}  
    \circprocess Proc_R1 \defs \circbegin
\end{circus}

\begin{circus}      
      @ in?x \then out!x \then Skip
\circend
\end{circus}

\begin{circus}  
    \circprocess Proc_R2 \defs \circbegin
\end{circus}

\begin{circus}      
      @ in!blue \then out?x \then Skip
\circend
\end{circus}

:: There should not be an error here.
begin{circus}  
    \circprocess Proc_Paral \defs 
        Proc_R1
            \lpar \lchanset in, out \rchanset \rpar 
        Proc_R2
\end{circus}

:: Iterated sequential composition
\begin{circus}  
    \circprocess Proc_SeqIte \defs \Semi k1, k2: Colour; k3: Colour @ Proc_P
\end{circus}

:: Iterated internal choice
\begin{circus}  
    \circprocess Proc_IntChoiceIte \defs \Intchoice k1, k2: Colour; k3: Colour @ Proc_P
\end{circus}

:: Iterated parallelism
:: OBS: If the parallelism involves more than two processes then there is
:: the possibility of multi-synchronization.
begin{circus}  
    \circprocess Proc_ParIte \defs \Parallel k: Colour @ \lpar \lchanset in, out \rchanset \rpar Proc_P
\end{circus}


:: Hiding
:: OBS: Hiding can only occur for processes (not for actions). It must be the 
:: last operator applied in a process declaration
\begin{circus}  
    \circprocess Proc_Hide \defs Proc_P \hide \lchanset in, out \rchanset
\end{circus}

:: Indexed call

:: Implicit indexed call

:: Composition of anonymous processes - internal choice
\begin{circus}  
\circprocess Proc_Anon \defs ((\circbegin
\end{circus}

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

    \begin{schema}{State}
    s1: Colour
    \end{schema}

    \begin{circus}  	
    Init1 \defs s1 := blue
    \end{circus}    
	
\begin{circus}  	
    @ Init1
\circend)

\intchoice

(\circbegin
\end{circus}

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

	\begin{schema}{State}
            s2: Colour
	\end{schema}
	
	\begin{circus}  	
            Init2 \defs s2 := red
	\end{circus}    
	
\begin{circus}  	
    @ Init2
\circend))
\end{circus}

:: CREATE MORE ELABORATED COMPOSITIONS