--------------------------------------------------------------------------------
-- T_Powers.tex
--
-- Simple example to test multi-synchronisation. Parallelism of four processes 
-- that synchronise on channel 'm'. Process 'Read' reads a value from channel 
-- 'n' and processes SecondPower, ThirdPower and FourthPower calculate the
-- second, third and fourth power of the value.
--------------------------------------------------------------------------------

\begin{circus}
    \circchannel\ m, n, sndPower, trdPower, fthPower: \nat
\end{circus}

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

\begin{circus}
    @ n?x \then m!x \then Skip
    \circend
\end{circus}

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

\begin{circus}
    @ m?x \then sndPower!(x \times x) \then Skip
    \circend
\end{circus}

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

\begin{circus}
    @ m?x \then trdPower!(x \times x \times x) \then Skip
    \circend
\end{circus}

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

\begin{circus}
    @ m?x \then fthPower!(x \times x \times x \times x) \then Skip
    \circend
\end{circus}

\begin{circus}
    \circprocess\ Powers \defs\ 
        Read 
            \lpar \lchanset m \rchanset \rpar
        SecondPower
            \lpar \lchanset m \rchanset \rpar
        ThirdPower
            \lpar \lchanset m \rchanset \rpar
        FourthPower
\end{circus}

