--------------------------------------------------------------------------------
-- T_Ex1.tex

-- Some examples to demonstrate the GUI.
--------------------------------------------------------------------------------

--ADAPTADO AO NOVO LATEX, OK!!--

\begin{zed}
  Color ::= blue | red
\end{zed}  

\begin{circus}
  \circchannel ch, ch2, soma1, subtrai2, divide2
\end{circus}  

\begin{circus}
  \circchannel a, b, somaN, multiplicaN, out: \nat
\end{circus}  

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

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

%	\begin{schema}{State}
%		x: \nat
%	\end{schema}

	\begin{circusaction}
	      Init \circdef x := 0 
	\end{circusaction}     
	
	\begin{circusaction}
	      Add1 \circdef \circmu X \circspot (x := x + 1 \circseq a!x \then X)
	\end{circusaction}     

\begin{circusaction}      
      \circspot Init \circseq Add1
\end{circusaction}

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

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

\begin{circusaction}      
      \circspot ch \then \Skip
\end{circusaction}

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

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

    \begin{circusaction}
        MainAction \circdef \circmu X \circspot a?x \then b!x \then X
    \end{circusaction}

\begin{circusaction}      
      \circspot MainAction
\end{circusaction}

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

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

    \begin{circusaction}
        MainAction \circdef 
            ((\lcircguard true \rcircguard \circguard ch \then \Skip)
            \extchoice
            (\lcircguard true \rcircguard \circguard ch2 \then \Skip))
            \circseq
            MainAction
    \end{circusaction}

\begin{circusaction}
      \circspot MainAction
\end{circusaction}

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

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

    %\begin{circus}  
    %\circstate
    %\end{circus}

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

	\begin{circusaction}
	      Init \circdef x := 0
	\end{circusaction}     

    \begin{circusaction}
        A \circdef 
            (soma1 \then (x := x + 1 \circseq out!x \then A))
            \extchoice
            (\lcircguard x \geq 2 \rcircguard \circguard subtrai2 \then (x := x
            - 2 \circseq out!x \then A))
            \extchoice
            (somaN?n \then (x := x + n \circseq out!x \then A))
    \end{circusaction}

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

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

%%  Nao funciona como deveria. Obs: aqui, o programa nao trava como acontece 
%% quando, por ex., eu aperto um botao errado em Ex1_C
\begin{circus}
    \circprocess Ex1Par \circdef Ex1B \lpar \lchanset ch \rchanset \rpar Ex1B
\end{circus}

