-- T_MS3.tex
--
-- This is similar to T_MS2, but channel a is generic and of synchronization on
-- multiple values
--
--------------------------------------------------------------------------------

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

\begin{zed}
  Weekend ::= saturday | sunday
\end{zed} 

\begin{circus}
  \circchannel [X, Y]a: X \cross Y
\end{circus}  

\begin{circus}
  \circchannel [X, Y]b: X \cross Y
\end{circus}  

\begin{circus}
  \circchannel c
\end{circus}  

The process A reads from the channel.

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

\begin{circusaction}  	
    \circspot a[Colour, Weekend].blue.sunday 
        \then b[Colour, Colour].blue.red 
        \then c 
        \then \Skip
\end{circusaction}

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

Process B reads from the channel.
\begin{circus}  
\circprocess MS3B \circdef \circbegin
\end{circus}
	
\begin{circusaction}  	
    \circspot a[Colour, Weekend].blue.sunday
        \then b[Colour, Colour].blue.red 
        \then \Skip
\end{circusaction}

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

Process C writes on the channel.

\begin{circus}  
\circprocess MS3C \circdef \circbegin
\end{circus}
	
\begin{circusaction}  	
    \circspot a[Colour, Weekend].blue.sunday
        \then b[Colour, Colour].blue.red 
        \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 MS3IntAB \circdef MS3A \intchoice MS3B
\end{circus}


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

\begin{circus}
\circprocess MS3IntABParC \circdef MS3IntAB \lpar \lchanset a[Colour, Weekend]
\rchanset \rpar MS3C
\end{circus}


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

\begin{circus}  
\circprocess MS3ParAB \circdef MS3A \lpar \lchanset a[Colour, Weekend]
\rchanset \rpar MS3B
\end{circus}


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

\begin{circus}  
\circprocess MS3ParABC \circdef MS3ParAB \lpar \lchanset a[Colour, Weekend]
\rchanset \rpar MS3C
\end{circus}

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

\begin{circus}  
\circprocess MS3IntABParCano \circdef MS3A \intchoice MS3B \lpar \lchanset
a[Colour, Weekend] \rchanset \rpar MS3C
\end{circus}

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

\begin{circus}  
\circprocess MS3ParABCano \circdef MS3A \lpar \lchanset a[Colour, Weekend]
\rchanset \rpar ( MS3B \lpar \lchanset a[Colour, Weekend] \rchanset \rpar MS3C )
\end{circus}

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

\begin{circus}  
\circprocess MS3ParAC \circdef MS3A \lpar \lchanset a[Colour, Weekend]
\rchanset \rpar MS3C
\end{circus}

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

\begin{circus}  
\circprocess MS3ParABCanoHid \circdef 
    ( MS3A \lpar \lchanset a[Colour, Weekend] \rchanset \rpar ( MS3B \lpar
    \lchanset a[Colour, Weekend], b[Colour, Colour] \rchanset \rpar MS3C ) )
    \circhide \lchanset a[Colour, Weekend], b[Colour, Colour] \rchanset
\end{circus}

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

\begin{circus}  
\circprocess MS3ParACHid \circdef (MS3A \lpar \lchanset a[Colour, Weekend],
b[Colour, Colour] \rchanset \rpar MS3C) \circhide \lchanset a[Colour, Weekend],
b[Colour, Colour] \rchanset
\end{circus}
