--------------------------------------------------------------------------------
-- T_Err.tex

-- Situations where the translator should give an error message, because the 
-- input does not conform with the requirements for the translation.
--------------------------------------------------------------------------------

--ADAPTADO AO NOVO LATEX!!!!!!!--

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

\begin{circus}
    \circchannel in, out: Colour
\end{circus}  

:: Only one declaration is allowed in the axiomatic definition
\begin{axdef}
    a, b: \nat \\
    c: Colour
\where
    a = 10
\end{axdef}

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

\begin{circusaction}
      \circspot in!red \then \Skip
\end{circusaction}

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

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

\begin{circusaction}
      \circspot in!blue \then Skip
\end{circusaction}

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

:: Channel 'in' is used for read and write in the same process.
\begin{circus}  
    \circprocess Err_E1 \circdef \circbegin
\end{circus}

\begin{circusaction}
      \circspot in?x \then in!blue \then \Skip
\end{circusaction}

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

:: More than one writer in the paralelism
\begin{circus}  
    \circprocess Err_E2 \circdef 
            Err_P
                \lpar \lchanset in \rchanset \rpar
            Err_Q
\end{circus}

:: Redeclaration of action parameters or local variables.
\begin{circus}  
    \circprocess Err_E3 \circdef \circbegin
\end{circus}

\begin{circusaction}
    A \circdef 
        p: \nat \circspot (
            p := 0 \circseq
            \circvar\ p: \nat \circspot (
                p := 1 \circseq
                \circvar\ p: \nat \circspot
                    p := 2
            )
        )
\end{circusaction}

\begin{circusaction}
      \circspot A(1)
\end{circusaction}

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

:: Hiding not allowed
\begin{circus}
    \circprocess Err_E4 \circdef Err_P \circseq (Err_P \circhide \lchanset in
    \rchanset)
\end{circus}

