\begin{circus}
  	\circchannel\ tick, time
\end{circus}

\begin{circus}
	\circchannel out : RANGE \cross RANGE
\end{circus}

\begin{circus}
   	\circprocess\ Achronometer \circdef \circbegin
    	\also %
    	\circstate\ AState ~~==~~ [~ second, minute : RANGE ~] \\
    	AInit ~~==~~ [~ AState~' | second' = minute' = 0 ~] \\
    	IncSec ~~==~~ [~ \Delta AState | second' = (second + 1) mod \ 60 ~] \\
    	IncMin ~~==~~ [~ \Delta AState | minute' = (minute + 1) mod \ 60 ~] \\
    	IncSec ~~==~~ [\Delta SecSt; \Xi MinSt | 
                                  second' = (second + 1) mod \ 60] \\
    MinInit ~~==~~ [~ MinSt~' | minute' = 0 ~] \\
    IncMin ~~==~~ [\Delta MinSt; \Xi SecSt | 
                                  minute' = (minute + 1) mod \ 60] \\
    	RunSec ~~\circdef~~ 
    		    (tick \then IncSec \circseq 
                  ((\lcircguard (second = 0) \rcircguard 
                        \circguard inc \then \Skip)
                  \extchoice
                  (\lcircguard (second \neq 0) \rcircguard 
                        \circguard \Skip )))
        \extchoice 
            (time \then minsReq \then ans~?mins 
            \then out~!(mins, second) \then \Skip) \\
    RunMin ~~\circdef~~ 
        inc \then IncMin
        \extchoice
        minsReq \then ans~!minute \then \Skip \\
	Run ~~\circdef~~ (tick \then IncSec \circseq\ 
            (( \lcircguard (second = 0) \rcircguard \circguard IncMin) 
            \extchoice 
            ( \lcircguard (second \neq 0) \rcircguard \circguard Skip))) 
        \extchoice (time \then out~!(minute, second) \then Skip) \\
	Init ~~==~~ [~ minute', second' : RANGE | (minute' = 0) \land (second' = 0) ~]
	\t1 @ Init
	\circend
\end{circus}\filter
