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

--ADAPTADO AO LATEX DO NOVO PARSER, 1.5.0!!!!

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

\begin{circus}
  \circchannel m: Color
\end{circus}  

:: write

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

\begin{circusaction}
    \circspot m!blue \then \Skip
\end{circusaction}

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

:: read

\begin{circus}  
\circprocess PaperB \circdef \circbegin
\end{circus}
	
\begin{circusaction}  	
    \circspot m?x \then \Skip
\end{circusaction}

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

:: read

\begin{circus}  
\circprocess PaperC \circdef \circbegin
\end{circus}
	
\begin{circusaction}
    \circspot m?x \then \Skip
\end{circusaction}

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


:: Simple

\begin{circus}  
\circprocess PaperP2 \circdef (PaperA 
								\lpar \lchanset m \rchanset \rpar 
							PaperB)
							\circhide \lchanset m \rchanset
\end{circus}


:: Multi

\begin{circus}  
\circprocess PaperP3 \circdef (PaperA 
								\lpar \lchanset m \rchanset \rpar 
							( PaperB 
								\lpar \lchanset m \rchanset \rpar 
							PaperC ) )
							\circhide \lchanset m \rchanset
\end{circus}

