--------------------------------------------------------------------------------
-- T_GCD.tex
--
-- Calculates the GCD, using Euclides' algorithm.
--------------------------------------------------------------------------------

\begin{circus}
    \circchannel\ in, out, read, write: \nat
\end{circus}

\begin{circus}
    \circchannel\ gcd, sum
\end{circus}

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

\begin{circus}
    \circstate\ 
\end{circus}

    \begin{schema}{S}
        a, b: \nat
    \end{schema}
       
\begin{circus}
     Init \defs\ x, y: \nat @ a := x; b := y
\end{circus}

\begin{circus}
        A \defs\ \circmu\ X @ 
            \circif b = 0 \circthen 
                out!a \then Skip
            \circelse b \neq 0 \circthen 
                \circvar t:\nat @ (t := a; a := b; b := t \mod b); X
            \circfi
\end{circus}

\begin{circus}
    @ in?x \then in?y \then Init(x, y); A
    \circend
\end{circus}

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

\begin{circus}
    @ \circmu\ X @ 
        read?x \then read?y \then (
            (gcd \then in!x \then in!y \then out?r \then write!r \then X)
            \extchoice
            (sum \then write!(x+y) \then X)
        )
    \circend
\end{circus}

\begin{circus}
    \circprocess\ SumOrGCD \defs\ 
        (GCDClient 
            \lpar \lchanset in, out \rchanset \rpar
        GCD) \hide \lchanset in, out \rchanset
\end{circus}

