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

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

\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 Ex1_A \defs \circbegin
\end{circus}

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

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

	\begin{circus}
	      Init \defs x := 0 
	\end{circus}     
	
	\begin{circus}
	      Add1 \defs \circmu X @ (x := x + 1; a!x \then X)
	\end{circus}     

\begin{circus}      
      @ Init; Add1
\circend
\end{circus}

\begin{circus}  
\circprocess Ex1_B \defs \circbegin
\end{circus}

\begin{circus}      
      @ ch \then Skip
\circend
\end{circus}

\begin{circus}  
\circprocess Ex1_C \defs \circbegin
\end{circus}

    \begin{circus}
        MainAction \defs \circmu X @ a?x \then b!x \then X
    \end{circus}

\begin{circus}      
      @ MainAction
\circend
\end{circus}

\begin{circus}  
\circprocess Ex1_D \defs \circbegin
\end{circus}

    \begin{circus}
        MainAction \defs 
            ((\true \guard ch \then Skip) 
            \extchoice 
            (\true \guard ch2 \then Skip)); 
            MainAction
    \end{circus}

\begin{circus}      
      @ MainAction
\circend
\end{circus}

\begin{circus}  
\circprocess Ex1_E \defs \circbegin
\end{circus}

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

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

	\begin{circus}
	      Init \defs x := 0
	\end{circus}     

    \begin{circus}
        A \defs 
            (soma1 \then (x := x + 1; out!x \then A))
            \extchoice 
            ((x \geq 2) \guard subtrai2 \then (x := x - 2; out!x \then A))
            \extchoice
            (somaN?n \then (x := x + n; out!x \then A))
    \end{circus}

\begin{circus}      
      @ Init; A
\circend
\end{circus}


