--------------------------------------------------------------------------------
-- T_ActionParEx.tex

-- This example is from chapter 'Evaluation' of my dissertation.
-- It shows a problem that appears when one of the parallel actions contains
-- a call to another action.

-- I still have to come up with a solution for this problem.
--------------------------------------------------------------------------------

------ADAPTADO AO NOVO LATEX------

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

	\begin{circusaction}
    \circstate\ S ~~==~~ [~ x, y, z: \nat ~]
    \end{circusaction}

%    \begin{schema}{S}
%    x, y, z: \nat
%    \end{schema}

    \begin{circusaction}
    Init \circdef x := 0 \circseq y := 0 \circseq z := 0
    \end{circusaction}

    \begin{circusaction}
    B \circdef z := 10
    \end{circusaction}

    \begin{circusaction}
    A \circdef (y := 2) \linter \{ y \} | \{ x \} \rinter (x := y + 5 \circseq
    z := 10 \circseq B)
    \end{circusaction}

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

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