--------------------------------------------------------------------------------
-- T_SomeParamProc.tex

-- To test the GUI for parameterized processes.
-- P and Q are parameterized, and R is not.
--------------------------------------------------------------------------------

--ADAPTADO AO LATEX DO NOVO PARSER, 1.5.0

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

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

\begin{circus}
    \circprocess SomeParamProcP \circdef p: Colour \circspot \circbegin
\end{circus}

%    \begin{circus}  
%    \circstate
%    \end{circus}
	\begin{circusaction}
    \circstate\ State ~~==~~ [~ x: Colour ~]
    \end{circusaction}

%    \begin{schema}{State}
%        x: Colour
%    \end{schema}

    \begin{circusaction}
        Init \circdef x := p
    \end{circusaction}

\begin{circusaction}
      \circspot Init
\end{circusaction}

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

\begin{circus}  
    \circprocess SomeParamProcQ \circdef a, b: \nat; c: Colour \circspot \circbegin
\end{circus}

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

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

    \begin{circusaction}
        Init \circdef x := (a + b)
    \end{circusaction}

\begin{circusaction}
      \circspot Init
\end{circusaction}

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

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

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

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

    \begin{circusaction}
        Init \circdef x := 1
    \end{circusaction}

\begin{circusaction}
      \circspot Init
\end{circusaction}

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