CRefine version 2.1
<Refinement version="2.1">
  <historico>
    <Load>
      <especificacao>\begin{zsection}&#x0D;
\SECTION chronos \parents expansion\_rules, simplification\_rules%, circus\_toolkit&#x0D;
\end{zsection}&#x0D;
&#x0D;
\begin{zed}&#x0D;
	RANGE == 0 .. 59&#x0D;
\end{zed}&#x0D;
&#x0D;
\begin{circus}&#x0D;
	\circchannel\ tick, time \\&#x0D;
	\circchannel\ out : RANGE \cross RANGE&#x0D;
\end{circus}&#x0D;
&#x0D;
\begin{circus}&#x0D;
\circprocess\ Achronometer \circdef \circbegin&#x0D;
\also %&#x0D;
    \circstate\ AState == [ second, minute : RANGE ] \\&#x0D;
    	 AInit == [ AState&apos; | second&apos; = minute&apos; = 0 ] \\&#x0D;
	IncSec == [ \Delta AState | second&apos; = (second + 1) mod \ 60 \land minute&apos; = minute ] \\&#x0D;
	IncMin == [ \Delta AState | minute&apos; = (minute + 1) mod \ 60 \land second&apos; = second ] \\&#x0D;
	Run \circdef (tick \then IncSec \circseq\ (&#x0D;
        ( \lcircguard (second = 0) \rcircguard \circguard IncMin) &#x0D;
        \extchoice &#x0D;
        ( \lcircguard (second \neq 0) \rcircguard \circguard Skip)))&#x0D;
	\extchoice (time \then out~!(minute, second) \then Skip) \\&#x0D;
	\t1 @ AInit \circseq\ (\circmu\ X @ (Run \circseq\ X)) \\&#x0D;
	\circend&#x0D;
\end{circus}&#x0D;
</especificacao>
      <markupInicial>LATEX</markupInicial>
    </Load>
    <circusRefine.core.storage.InsertParagraph>
      <text>\begin{circus}
    \circchannel\ inc, minsReq
\end{circus}</text>
    </circusRefine.core.storage.InsertParagraph>
    <circusRefine.core.storage.InsertParagraph>
      <text>\begin{circus}
    \circchannel ans : 0 .. 59
\end{circus}</text>
    </circusRefine.core.storage.InsertParagraph>
    <circusRefine.core.storage.InsertParagraph>
      <text>\begin{circus}
    \circchannelset\ Sync == \lchanset inc, minsReq, ans \rchanset
\end{circus}</text>
    </circusRefine.core.storage.InsertParagraph>
    <LawApp linhaInicial="37" linhaFinal="37">
      <params class="linked-list"/>
      <cod>Cpy_Rule_Name</cod>
    </LawApp>
    <LawApp linhaInicial="59" linhaFinal="59">
      <params class="linked-list"/>
      <cod>Normalize</cod>
    </LawApp>
    <LawApp linhaInicial="61" linhaFinal="61">
      <params class="linked-list">
        <string>second&apos; = 0 \land minute&apos; = 0</string>
      </params>
      <cod>TransformPredicate</cod>
    </LawApp>
    <LawApp linhaInicial="63" linhaFinal="63">
      <params class="linked-list">
        <string>second&apos;</string>
      </params>
      <cod>C-72</cod>
    </LawApp>
    <Collect>
      <tipo>PROCESSO</tipo>
      <nome>Achronometer</nome>
    </Collect>
    <LawApp linhaInicial="69" linhaFinal="105">
      <params class="linked-list">
        <string>SecSt == [ second: RANGE ]</string>
      </params>
      <cod>InserirPara</cod>
    </LawApp>
    <LawApp linhaInicial="107" linhaFinal="142">
      <params class="linked-list">
        <string>MinSt == [ minute: RANGE ]</string>
      </params>
      <cod>InserirPara</cod>
    </LawApp>
    <LawApp linhaInicial="144" linhaFinal="181">
      <params class="linked-list">
        <string>SecInit == [ SecSt&apos; | second&apos; = 0 ]</string>
      </params>
      <cod>InserirPara</cod>
    </LawApp>
    <LawApp linhaInicial="183" linhaFinal="222">
      <params class="linked-list">
        <string>MinInit == [ MinSt&apos; | minute&apos; = 0 ]</string>
      </params>
      <cod>InserirPara</cod>
    </LawApp>
    <LawApp linhaInicial="251" linhaFinal="251">
      <params class="linked-list"/>
      <cod>Normalize</cod>
    </LawApp>
    <LawApp linhaInicial="267" linhaFinal="267">
      <params class="linked-list">
        <string>second&apos; = 0</string>
      </params>
      <cod>TransformPredicate</cod>
    </LawApp>
    <LawApp linhaInicial="253" linhaFinal="253">
      <params class="linked-list"/>
      <cod>Normalize</cod>
    </LawApp>
    <LawApp linhaInicial="271" linhaFinal="271">
      <params class="linked-list">
        <string>minute&apos; = 0</string>
      </params>
      <cod>TransformPredicate</cod>
    </LawApp>
    <Collect>
      <tipo>PROCESSO</tipo>
      <nome>Achronometer</nome>
    </Collect>
    <LawApp linhaInicial="275" linhaFinal="319">
      <params class="linked-list">
        <string>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))</string>
      </params>
      <cod>InserirPara</cod>
    </LawApp>
    <LawApp linhaInicial="321" linhaFinal="378">
      <params class="linked-list">
        <string>RunMin \circdef 
        (inc \then IncMin) \extchoice (minsReq \then ans~!minute \then Skip)</string>
      </params>
      <cod>InserirPara</cod>
    </LawApp>
    <LawApp linhaInicial="439" linhaFinal="442">
      <params class="linked-list">
        <string>((\circmu\ X @ RunSec \circseq X) 
	\lpar \{ second \}| Sync | \{ minute \} \rpar 
	(\circmu\ X @ RunMin \circseq X)) \circhide\ Sync</string>
      </params>
      <cod>C.129</cod>
    </LawApp>
    <LawApp linhaInicial="435" linhaFinal="437">
      <params class="linked-list">
        <string>Sync</string>
      </params>
      <cod>C.120</cod>
    </LawApp>
    <Collect>
      <tipo>ACAO</tipo>
      <nome>$$mainAction</nome>
    </Collect>
    <LawApp linhaInicial="463" linhaFinal="477">
      <params class="linked-list"/>
      <cod>C.125</cod>
    </LawApp>
    <LawApp linhaInicial="483" linhaFinal="491">
      <params class="linked-list"/>
      <cod>C.76</cod>
    </LawApp>
    <Collect>
      <tipo>ACAO</tipo>
      <nome>$$mainAction</nome>
    </Collect>
    <LawApp linhaInicial="505" linhaFinal="517">
      <params class="linked-list"/>
      <cod>SequenceAssociativity</cod>
    </LawApp>
    <LawApp linhaInicial="522" linhaFinal="532">
      <params class="linked-list"/>
      <cod>C-73</cod>
    </LawApp>
    <LawApp linhaInicial="534" linhaFinal="544">
      <params class="linked-list"/>
      <cod>C.76</cod>
    </LawApp>
    <Collect>
      <tipo>ACAO</tipo>
      <nome>$$mainAction</nome>
    </Collect>
    <LawApp linhaInicial="559" linhaFinal="571">
      <params class="linked-list"/>
      <cod>C-73</cod>
    </LawApp>
    <LawApp linhaInicial="574" linhaFinal="574">
      <params class="linked-list"/>
      <cod>Cpy_Rule_Expr</cod>
    </LawApp>
    <LawApp linhaInicial="581" linhaFinal="581">
      <params class="linked-list"/>
      <cod>Cpy_Rule_Expr</cod>
    </LawApp>
    <LawApp linhaInicial="382" linhaFinal="382">
      <params class="linked-list">
        <string>second</string>
      </params>
      <cod>SchemaDecomposition</cod>
    </LawApp>
    <LawApp linhaInicial="386" linhaFinal="386">
      <params class="linked-list">
        <string>AState</string>
      </params>
      <cod>Cpy_Rule_Name</cod>
    </LawApp>
    <LawApp linhaInicial="596" linhaFinal="596">
      <params class="linked-list"/>
      <cod>Normalize</cod>
    </LawApp>
    <LawApp linhaInicial="598" linhaFinal="598">
      <params class="linked-list">
        <string>(second \in 0 .. 59 \land second&apos; \in 0 .. 59 \land second&apos; = (second + 1) mod\ 60) \land (minute&apos; \in 0 .. 59 \land minute \in 0 .. 59 \land minute&apos; = minute)</string>
      </params>
      <cod>TransformPredicate</cod>
    </LawApp>
    <LawApp linhaInicial="600" linhaFinal="600">
      <params class="linked-list">
        <string>second, second&apos;</string>
      </params>
      <cod>SchemaDecomposition2</cod>
    </LawApp>
    <LawApp linhaInicial="604" linhaFinal="604">
      <params class="linked-list">
        <string>minute&apos; = minute \land (minute \in 0 \upto 59 \land minute&apos; \in 0 \upto 59)</string>
      </params>
      <cod>TransformPredicate</cod>
    </LawApp>
    <LawApp linhaInicial="606" linhaFinal="606">
      <params class="linked-list">
        <string>MinSt</string>
      </params>
      <cod>XiSchemaLeft</cod>
    </LawApp>
    <Collect>
      <tipo>PROCESSO</tipo>
      <nome>Achronometer</nome>
    </Collect>
    <LawApp linhaInicial="620" linhaFinal="622">
      <params class="linked-list"/>
      <cod>ZeroAnd</cod>
    </LawApp>
    <circusRefine.core.storage.SetandoFormaOP>
      <indiceOP>23</indiceOP>
    </circusRefine.core.storage.SetandoFormaOP>
    <circusRefine.core.storage.SetandoFormaOP>
      <indiceOP>23</indiceOP>
    </circusRefine.core.storage.SetandoFormaOP>
    <LawApp linhaInicial="624" linhaFinal="624">
      <params class="linked-list">
        <string>AState</string>
      </params>
      <cod>Cpy_Rule_Name</cod>
    </LawApp>
    <LawApp linhaInicial="691" linhaFinal="691">
      <params class="linked-list"/>
      <cod>Normalize</cod>
    </LawApp>
    <LawApp linhaInicial="693" linhaFinal="693">
      <params class="linked-list">
        <string>(minute \in 0 \upto 59 \land minute&apos; \in 0 \upto 59 \land minute&apos; = (minute + 1) \mod\ 60) \land (second \in 0 \upto 59 \land second&apos; \in 0 \upto 59 \land second&apos; = second)</string>
      </params>
      <cod>TransformPredicate</cod>
    </LawApp>
    <LawApp linhaInicial="695" linhaFinal="695">
      <params class="linked-list">
        <string>minute, minute&apos;</string>
      </params>
      <cod>SchemaDecomposition2</cod>
    </LawApp>
    <LawApp linhaInicial="699" linhaFinal="699">
      <params class="linked-list">
        <string>second&apos; = second \land (second \in 0 \upto 59 \land second&apos; \in 0 \upto 59)</string>
      </params>
      <cod>TransformPredicate</cod>
    </LawApp>
    <LawApp linhaInicial="701" linhaFinal="701">
      <params class="linked-list">
        <string>SecSt</string>
      </params>
      <cod>XiSchemaLeft</cod>
    </LawApp>
    <Collect>
      <tipo>PROCESSO</tipo>
      <nome>Achronometer</nome>
    </Collect>
    <LawApp linhaInicial="717" linhaFinal="719">
      <params class="linked-list"/>
      <cod>ZeroAnd</cod>
    </LawApp>
    <Collect>
      <tipo>PROCESSO</tipo>
      <nome>Achronometer</nome>
    </Collect>
    <LawApp linhaInicial="786" linhaFinal="861">
      <params class="linked-list">
        <string>Run</string>
      </params>
      <cod>RemoverPara</cod>
    </LawApp>
    <LawApp linhaInicial="863" linhaFinal="922">
      <params class="linked-list">
        <string>AInit</string>
      </params>
      <cod>RemoverPara</cod>
    </LawApp>
    <LawApp linhaInicial="926" linhaFinal="926">
      <params class="linked-list"/>
      <cod>Cpy_Rule_Expr</cod>
    </LawApp>
    <LawApp linhaInicial="928" linhaFinal="928">
      <params class="linked-list"/>
      <cod>Cpy_Rule_Expr</cod>
    </LawApp>
    <Collect>
      <tipo>PROCESSO</tipo>
      <nome>Achronometer</nome>
    </Collect>
    <LawApp linhaInicial="987" linhaFinal="1047">
      <params class="linked-list">
        <string>Seconds</string>
        <string>Minutes</string>
        <string>(SecInit \circseq (\circmu X @ RunSec \circseq X))</string>
        <string>(MinInit \circseq (\circmu X @ RunMin \circseq X))</string>
      </params>
      <cod>C.146</cod>
    </LawApp>
  </historico>
  <redoList/>
</Refinement>