-- 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.
--------------------------------------------------------------------------------

\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 MS_A \defs \circbegin
\end{circus}

\begin{circus}  	
    @ a?x \then b?y \then Skip
\circend
\end{circus}

Process B reads from the channel.
\begin{circus}  
\circprocess MS_B \defs \circbegin
\end{circus}
	
\begin{circus}  	
    @ a?x \then b?y \then Skip
\circend
\end{circus}

Process C writes on the channel.

\begin{circus}  
\circprocess MS_C \defs \circbegin
\end{circus}
	
\begin{circus}  	
    @ a!blue \then b!blue \then Skip
\circend
\end{circus}


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

\begin{circus}  
\circprocess MS_Int_AB \defs MS_A \intchoice MS_B
\end{circus}


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

\begin{circus}  
\circprocess MS_Int_AB_Par_C \defs MS_Int_AB \lpar \lchanset a \rchanset \rpar MS_C
\end{circus}


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

\begin{circus}  
\circprocess MS_Par_AB \defs MS_A \lpar \lchanset a \rchanset \rpar MS_B
\end{circus}


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

\begin{circus}  
\circprocess MS_Par_ABC \defs MS_Par_AB \lpar \lchanset a \rchanset \rpar MS_C
\end{circus}

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

\begin{circus}  
\circprocess MS_Int_AB_Par_C_ano \defs MS_A \intchoice MS_B \lpar \lchanset a \rchanset \rpar MS_C
\end{circus}

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

\begin{circus}  
\circprocess MS_Par_ABC_ano \defs MS_A \lpar \lchanset a \rchanset \rpar MS_B \lpar \lchanset a \rchanset \rpar MS_C
\end{circus}

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

\begin{circus}  
\circprocess MS_Par_AC \defs MS_A \lpar \lchanset a \rchanset \rpar MS_C
\end{circus}
