--------------------------------------------------------------------------------
-- T_SyncOnMultiple.tex

-- This test is to investigate how to define which is the reader and writer on a 
-- synchronization of a generic channel.
--------------------------------------------------------------------------------

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


\begin{circus}
  \circchannel [X]c : X
\end{circus}  


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

\begin{circus}      
      @ c[Colour].blue \then Skip
\circend
\end{circus}

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

\begin{circus}      
      @ c[Colour].blue \then Skip
\circend
\end{circus}

\begin{circus}  
    \circprocess SyncOnMultiple_R \defs 
        SyncOnMultiple_P 
            \lpar \lchanset c \rchanset \rpar 
        SyncOnMultiple_Q
\end{circus}

