--------------------------------------------------------------------------------
-- T_AxDef.tex
--
-- To test a function defined in an axiomatic definition.
--
-- Reads a number in channel in and outputs on channel out the function
-- applied to that number.
--
--------------------------------------------------------------------------------

-------ESTÁ COM PROBLEMA AINDA, MAS NÃO ESTOU SABENDO IDENTIFICAR!!
IR PARA O PRÓXIMO AGORA!!!!------

\begin{zed}
    Colour ::= blue | red | green | yellow
\end{zed}

\begin{axdef}
  limit: \nat
\where
  limit = 5
\end{axdef}

\begin{circus}
\circchannel in: Colour; out: \nat ; cend
\end{circus}

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

    \begin{axdef}
      fun: Colour \pfun \nat
    \where
      fun~blue = 1 \land
      fun~red = 2 \land
      fun~green = 3 \land
      fun~yellow = 4
    \end{axdef}
    
%    \begin{circus}
%    \circstate
%    \end{circus}

    \begin{circusaction}
    \circstate\ State ~~==~~ [~ x: \nat ~]
    \end{circusaction}

    \begin{circusaction}
        A \circdef 
            \circvar i: \nat \circspot
                (
                i := 0 \circseq
                \circmu X \circspot
                    \circif i < limit \circthen
                        in?x \then out!(fun~x) \then 
                        i := i + 1 \circseq X
                    \circelse i = limit \circthen
                        cend \then \Skip
                    \circfi
                    )
    \end{circusaction}

\begin{circusaction}  	
    \circspot A
\end{circusaction}

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