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

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

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

\begin{circusaction}
    A \circdef 
        (a \then Skip) 
        \extchoice 
        (b \then Skip)
\end{circusaction}

\begin{circusaction}
    \circspot A
\end{circusaction}

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


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

\begin{circusaction}
    A \circdef 
        (a \then \Skip) 
        \extchoice 
        (c \then \Skip)
\end{circusaction}

\begin{circusaction}
    \circspot A
\end{circusaction}

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

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

\begin{circusaction}
    A \circdef 
        (a \then \Skip) 
        \extchoice 
        (c \then \Skip)
\end{circusaction}

\begin{circusaction}
    \circspot A
\end{circusaction}

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

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

\begin{circusaction}
    A \circdef (a \then \Skip) \extchoice (c \then \Skip)
\end{circusaction}

\begin{circusaction}
    \circspot A
\end{circusaction}

\begin{circus}
  \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  ExtMultiSingleP \circdef 
        ExtMultiSingleA 
            \lpar \lchanset a \rchanset \rpar 
        (ExtMultiSingleB \lpar \lchanset a, c \rchanset \rpar ExtMultiSingleC)
\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  ExtMultiSingleQ \circdef 
        ExtMultiSingleA 
            \lpar \lchanset a \rchanset \rpar 
        ExtMultiSingleB
\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  ExtMultiSingleR \circdef 
        ExtMultiSingleC 
            \lpar \lchanset a \rchanset \rpar 
        ExtMultiSingleD
\end{circus}

