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

--ADAPTADO AO LATEX DO NOVO PARSER, 1.5.0--

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

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

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

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

	\begin{circusaction}
    \circstate\ S ~~==~~ [~ a, b: \nat ~] %\land [~ y: Colour ~]
    \end{circusaction}

    %\begin{schema}{S}
    %    a, b: \nat
    %\end{schema}
       
\begin{circusaction}
     Init \circdef x, y: \nat \circspot a := x \circseq b := y
\end{circusaction}

\begin{circusaction}
        A \circdef \circmu X \circspot 
            \circif b = 0 \circthen 
                out!a \then \Skip
            \circelse b \neq 0 \circthen 
                \circvar t:\nat \circspot (t := a \circseq a := b \circseq b :=
                t \mod b) \circseq X
            \circfi
\end{circusaction}

\begin{circusaction}
    \circspot in?x \then in?y \then Init(x, y) \circseq A
\end{circusaction}

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

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

\begin{circusaction}
    \circspot \circmu X \circspot 
        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)
        )
\end{circusaction}

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

\begin{circus}
    \circprocess SumOrGCD \circdef
        (GCDClient 
            \lpar \lchanset in, out \rchanset \rpar
        GCDEuclideanUm) \circhide \lchanset in, out \rchanset
\end{circus}

