-- T_MS.tex
--
-- To test multi-synchronization.
-- Three processes, A, B (readers) and C (writer), synchronizing on channels a and b.
-- Testing different combinations of these processes, some involving simple-sync,
-- others involving multi-sync.
--------------------------------------------------------------------------------

--ADAPTAÇÃO AO LATEX DO NOVO PARSER OK! 1.5.0

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

\begin{circus}
  \circchannel a, b: Color
\end{circus}  

The process A reads from the channel.

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

\begin{circusaction}
    \circspot a?x \then b?y \then \Skip
\end{circusaction}

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

Process B reads from the channel.
\begin{circus}  
\circprocess MSB \circdef \circbegin
\end{circus}
	
\begin{circusaction}  	
    \circspot a?x \then b?y \then \Skip
\end{circusaction}

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

Process C writes on the channel.

\begin{circus}  
\circprocess MSC \circdef \circbegin
\end{circus}
	
\begin{circusaction}  	
    \circspot a!blue \then b!blue \then \Skip
\end{circusaction}

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


:: Intchoice between A and B. There is no parallelism, and channel a will appear in the gui.

\begin{circus}  
\circprocess MSIntAB \circdef MSA \intchoice MSB
\end{circus}


:: Intchoice between A and B, in parallel with C. Single-sync, channel not in gui.

\begin{circus}  
\circprocess MSIntABParC \circdef MSIntAB \lpar \lchanset a \rchanset \rpar MSC
\end{circus}


:: Parallelism between A and B. Single-sync, channel not in gui. 
:: Error, because both want to read.

\begin{circus}  
\circprocess MSParAB \circdef MSA \lpar \lchanset a \rchanset \rpar MSB
\end{circus}


:: Parallelism between A, B and C. Multi-sync, channel not in gui.

\begin{circus}
\circprocess MSParABC \circdef MSParAB \lpar \lchanset a \rchanset \rpar MSC
\end{circus}

:: Intchoice between A and B, in parallel with C, anonymous. Single-sync, channel not in gui.

\begin{circus}  
\circprocess MSIntABParCano \circdef MSA \intchoice MSB \lpar \lchanset a \rchanset \rpar MSC
\end{circus}

:: Parallelism between A, B and C, anonymous. Multi-sync, channel not in gui.

\begin{circus}
\circprocess MSParABCano \circdef MSA \lpar \lchanset a \rchanset \rpar
( MSB \lpar \lchanset a \rchanset \rpar MSC )
\end{circus}

:: Parallelism between A and C. Single-sync, channel not in gui.
J
\begin{circus}  
\circprocess MSParAC \circdef MSA \lpar \lchanset a \rchanset \rpar MSC
\end{circus}
