\begin{zsection}
\SECTION chronos \parents expansion\_rules, simplification\_rules%, circus\_toolkit
\end{zsection}

\begin{zed}
	RANGE == 0 .. 59
\end{zed}

\begin{circus}
	\circchannel\ tick, time \\
	\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 \land minute' = minute ] \\
	IncMin == [ \Delta AState | minute' = (minute + 1) mod \ 60 \land second' = second ] \\
	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) \\
	\t1 @ AInit \circseq\ (\circmu\ X @ (Run \circseq\ X)) \\
	\circend
\end{circus}
