--ESPECIFICAÇÃO ADAPTADA AO NOVO LATEX---

\begin{circus}
    \circchannel\ tick, time, inc, notInc, minsReq
\end{circus}

\begin{circus}
    \circchannel\ out, ans: \nat
\end{circus}

\begin{circus}
    \circchannelset\ Sync == \lchanset inc, notInc, minsReq, ans \rchanset
\end{circus}

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

%\begin{circus}
%    \circstate\ 
%\end{circus}
	\begin{circusaction}
    \circstate\ SecSt ~~==~~ [~ sec: \nat ~]
    \end{circusaction}

%    \begin{schema}{SecSt}
%        sec: \nat
%    \end{schema}

        
\begin{circusaction}
        SecInit \circdef sec := 0
\end{circusaction}

\begin{circusaction}
        IncSec \circdef sec := (sec+1) \mod 60
\end{circusaction}

\begin{circusaction}
        RunSec \circdef
            tick \then (IncSec 
            	\circseq
                (
                (\lcircguard sec = 0 \rcircguard \circguard inc \then \Skip)
                \extchoice
                (\lcircguard sec \neq 0 \rcircguard \circguard notInc \then
                \Skip)
                )
                )
            \extchoice
            time \then (minsReq \then ans?mins \then out!mins
            \then out!sec
            \then \Skip
            )
\end{circusaction}

\begin{circusaction}
    \circspot SecInit \circseq \circmu X \circspot (RunSec \circseq X)
\end{circusaction}

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

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

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

%    \begin{schema}{MinSt}
%        minute: \nat
%    \end{schema}
	\begin{circusaction}
    \circstate\ MinSt ~~==~~ [~ minute: \nat ~]
    \end{circusaction}

\begin{circusaction}
        MinInit \circdef\ minute := 0
\end{circusaction}

\begin{circusaction}
        IncMin \circdef minute := minute + 1
\end{circusaction}

\begin{circusaction}
        RunMin \circdef
            (inc \then IncMin)
            \extchoice 
            (notInc \then \Skip)
            \extchoice 
            (minsReq \then ans!minute \then \Skip)
\end{circusaction}

\begin{circusaction}
    \circspot MinInit \circseq \circmu X \circspot (RunMin \circseq X)
\end{circusaction}

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

\begin{circus}
    \circprocess\ ChrChronometer \circdef (ChrSeconds \lpar Sync \rpar
    ChrMinutes) \circhide Sync
\end{circus}
