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

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

--ADAPTADO COM RESSALVAS

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

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

:: Basic process definition
\begin{circus}  
    \circprocess ProcP \circdef \circbegin
\end{circus}

\begin{circusaction}
      \circspot in?x \then out!x \then \Skip
\end{circusaction}

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

:: Basic parameterized process definition
\begin{circus}
    \circprocess ProcQ \circdef p1: \nat ; p2: Colour \circspot
    \circbegin
\end{circus}

\begin{circusaction}
      \circspot \Skip
\end{circusaction}

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

\begin{circus}
    \circprocess ProcSkip \circdef \circbegin
\end{circus}

\begin{circusaction}
      \circspot \Skip
\end{circusaction}

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

:: Process call
\begin{circus}
    \circprocess ProcCall \circdef ProcP
\end{circus}

:: Parameterized call
\begin{circus}  
    \circprocess ProcParamCall \circdef ProcQ (1, red)
\end{circus}

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

:: Generic instantiation

:: Generic instantiation and parameterized call

:: Sequential composition
\begin{circus}
    \circprocess ProcSeq \circdef
            ProcP \circseq ProcSkip%ProcQ (1, blue)
\end{circus}
Acima, quando ProcQ(1, blue) é descomentado para substituir ProcSkip por ele,
o parsing dá UnsupportedAstClassException, motivo pelo qual substituí por
ProcSkip, implementado por mim (Samuel)

:: External choice

:: Internal choice
\begin{circus}
    \circprocess ProcIntChoiceP \circdef
            ProcP \intchoice %ProcQ (0, blue)
            ( ProcQ (0, blue)
            \intchoice ProcSeq
            )
\end{circus}

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


:: Parallelism

\begin{circus}  
    \circprocess ProcR1 \circdef \circbegin
\end{circus}

\begin{circusaction}
      \circspot in?x \then out!x \then \Skip
\end{circusaction}

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

\begin{circus}  
    \circprocess ProcR2 \circdef \circbegin
\end{circus}

\begin{circusaction}
      \circspot in!blue \then out?x \then \Skip
\end{circusaction}

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

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

:: Iterated sequential composition
\begin{circus}  
    \circprocess ProcSeqIte \circdef \Semi k1, k2: Colour; k3: Colour \circspot ProcP
\end{circus}

:: Iterated internal choice
\begin{circus}
    \circprocess ProcIntChoiceIte \circdef \Intchoice k1, k2: Colour; k3: Colour \circspot ProcP
\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 \circdef \Parallel k: Colour \circspot \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 ProcHide \circdef ProcP \circhide \lchanset in, out \rchanset
\end{circus}

:: Indexed call

:: Implicit indexed call

:: Composition of anonymous processes - internal choice
\begin{circus}
\circprocess ProcSam1 \circdef \circbegin
\end{circus}

	\begin{circusaction}
    \circstate\ State ~~==~~ [~ s1: \nat ~]
    \end{circusaction}

    \begin{circusaction}
    Init1 \circdef s1 := 5
    \end{circusaction}
	
\begin{circusaction}
    \circspot Init1
\end{circusaction}

\begin{circus}
\circend %)
\end{circus}

%\intchoice

%(
\begin{circus}
\circprocess ProcSam2 \circdef \circbegin
\end{circus}

	\begin{circusaction}
    \circstate\ State2 ~~==~~ [~ s2: \nat ~]
    \end{circusaction}

	\begin{circusaction}  	
            Init2 \circdef s2 := 7
	\end{circusaction}
	
\begin{circusaction}
    \circspot Init2
\end{circusaction}

\begin{circus}
\circend %))
\end{circus}

\begin{circus}
\circprocess ProcAnon \circdef ProcSam1 \intchoice ProcSam2
\end{circus}

:: CREATE MORE ELABORATED COMPOSITIONS