--------------------------------------------------------------------------------
-- T_MSExtChoice2.tex
--
-- This is to test what happens if we have a multisynchronization (Par_ABC, on m1)
-- where two processes (A, B) are in an alternation and the third (C), not.
--
-- And a single synchronization (Par_ABD, on m2) where one process (A) is in an
-- alternation and the other (D), not.
--
--------------------------------------------------------------------------------

\begin{circus}
\circchannel m1, m2, m3
\end{circus}  

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

\begin{circus}  	
    @ 
    (m1 \then Skip) 
    \extchoice 
    (m2 \then Skip)
\circend
\end{circus}

\begin{circus}  
\circprocess MSEC2_B \defs \circbegin
\end{circus}
	
\begin{circus}  	
    @ 
    (m1 \then Skip) 
    \extchoice 
    (m3 \then Skip)
\circend
\end{circus}

\begin{circus}  
\circprocess MSEC2_C \defs \circbegin
\end{circus}
	
\begin{circus}  	
    @ m1 \then Skip
\circend
\end{circus}

\begin{circus}  
\circprocess MSEC2_D \defs \circbegin
\end{circus}
	
\begin{circus}  	
    @ m2 \then Skip
\circend
\end{circus}


\begin{circus}  
\circprocess MSEC2_Par_ABC \defs MSEC2_A \lpar \lchanset m1, m2 \rchanset \rpar MSEC2_B \lpar \lchanset m1, m2 \rchanset \rpar MSEC2_C
\end{circus}

\begin{circus}  
\circprocess MSEC2_Par_ABD \defs MSEC2_A \lpar \lchanset m1, m2 \rchanset \rpar MSEC2_B \lpar \lchanset m1, m2 \rchanset \rpar MSEC2_D
\end{circus}
