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

\begin{gendef}[ACTION, NAME]
   FV: ACTION \fun \power~NAME
\end{gendef}

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

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

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

\begin{schema}{AState}
	second, minute :  0 .. 59
\end{schema}

\begin{schema}{ AInit }
   	AState~' 
	\where
	second' = minute' = 0 \land FV(Process)
\end{schema}

\begin{circus}
\circprocess\ Achronometer \circdef \circbegin
\also %
    \circstate\ AState ~~==~~ [second: RANGE ] \land [minute : RANGE]  \\
	IncSec ~~==~~ [~ \Delta AState | second' = (second + 1) mod \ 60 ~] \\
	IncMin ~~==~~ [~ \Delta AState | minute' = (minute + 1) mod \ 60 ~] \\
	Def ~~==~~ [~ second', minute': \nat | second' = 0 \land minute' = 0´\land 1 \in \emptyset ~] \\
	Run ~~\circdef~~ \Skip  \\
	A2 \circdef\ ((\circmu\ X @ RunSec \circseq X) 
	\lpar \{ second \}| Sync | \{ minute \} \rpar 
	(\circmu\ X @ RunMin \circseq X)) \circhide\ Sync \\
	\t1 @ (\alpha(AInit) \circseq\ (\circmu\ X @ (Run \circseq\ X))) \\
	\circend
\end{circus}

\begin{circus}
\circprocess\ Seconds \circdef \circbegin
    \also
    \circstate SecSt == [ second: RANGE ]\\
    SecInit == [ SecSt' | second' = 0 ] \\
    IncSec == [ \Delta SecSt | second' = (second + 1) mod\ 60 ] \\
    NewAction \circdef FV \Skip \\
    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))\\
    @ SecInit \circseq (\circmu\ X @ RunSec \circseq X)
\circend
\end{circus}

\begin{circus}
\circprocess\ Minutes \circdef \circbegin
    \also
    \circstate MinSt == [ minute: RANGE ] \\
    MinInit == [ MinSt' | minute' = 0 ] \\
    Teste ==  [ y: \nat ; x : \nat ; [ x : \nat | x > 0 ]| y = 0 \land x > 2 ] \\
    IncMin == [ \Delta MinSt | minute' = (minute + 1) mod\ 60 ] \\
    RunMin \circdef 
        (inc \then IncMin) \extchoice (minsReq \then ans~!minute \then Skip)
    @ MinInit \circseq (\circmu\ X @ RunMin \circseq X)
\circend
\end{circus}

\begin{circus}
\circprocess\ Chronometer \circdef Seconds \lpar Sync \rpar Minutes \circhide Sync
\end{circus}

\begin{circus}
\circprocess\ ToSplitChronometer \circdef \circbegin
\also %
    \circstate\ AState ~~==~~ SecSt \land MinSt \\
     SecSt ==  [ second: RANGE ]\\
     MinSt == [ minute: RANGE ] \\
    SecInit == [ AState' | second' = 0 ] \\
    IncSec == [ \Delta SecSt | second' = (second + 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))\\
    MinInit == [ MinSt' | minute' = 0 ] \\
    IncMin == [ \Delta MinSt | minute' = (minute + 1) mod\ 60 ] \\
    RunMin \circdef 
        (inc \then IncMin) \extchoice (minsReq \then ans~!minute \then Skip)	 
	
   \t1 @ (SecInit \circseq ( \circmu X @ RunSec \circseq X )) 
   		\lpar \{second \} | 
		Sync | 
		\{ minute \} \rpar 
		(MinInit \circseq ( \circmu X @ RunMin \circseq X ))  \\
   \circend
\end{circus}

\begin{circus}
\circprocess\ OtherChronometer2 \circdef P
\end{circus}
