--------------------------------------------------------------------------------
-- T_ExtMultiSingle.tex
--
-- To test simple and multi-synchronization in an external choice.
--
--------------------------------------------------------------------------------

\begin{circus}
  \circchannel a, b, c
\end{circus}

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

\begin{circus}
    A \defs 
        (a \then Skip) 
        \extchoice 
        (b \then Skip)
\end{circus}

\begin{circus}
    @ A
  \circend
\end{circus}


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

\begin{circus}
    A \defs 
        (a \then Skip) 
        \extchoice 
        (c \then Skip)
\end{circus}

\begin{circus}
    @ A
  \circend
\end{circus}

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

\begin{circus}
    A \defs 
        (a \then Skip) 
        \extchoice 
        (c \then Skip)
\end{circus}

\begin{circus}
    @ A
  \circend
\end{circus}

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

\begin{circus}
    A \defs (a \then Skip) \extchoice (c \then Skip)
\end{circus}

\begin{circus}
    @ A
  \circend
\end{circus}


In the following process, 'a' is a multi-synch event, performed by A, B and C;
'b' is performed only by A; and 'c' is a single synch event, in which B and C synchronize.

\begin{circus}
    \circprocess  ExtMultiSingle_P \defs 
        ExtMultiSingle_A 
            \lpar \lchanset a \rchanset \rpar 
        (ExtMultiSingle_B \lpar \lchanset a, c \rchanset \rpar ExtMultiSingle_C)
\end{circus}

In the following process, 'a' is a single-synch event, performed by A and B;
'b' and 'c' are performed only by 'A' and 'B', respectively.

\begin{circus}
    \circprocess  ExtMultiSingle_Q \defs 
        ExtMultiSingle_A 
            \lpar \lchanset a \rchanset \rpar 
        ExtMultiSingle_B
\end{circus}

In the following process, C and D are identical processes; therefore, we
have two single synchronizations, in channels "a" and "c".


\begin{circus}
    \circprocess  ExtMultiSingle_R \defs 
        ExtMultiSingle_C 
            \lpar \lchanset a \rchanset \rpar 
        ExtMultiSingle_D
\end{circus}

