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

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

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

\begin{circus}      
      @ in!red \then Skip
\circend
\end{circus}

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

\begin{circus}      
      @ in!blue \then Skip
\circend
\end{circus}

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

\begin{circus}      
      @ in?x \then in!blue \then Skip
\circend
\end{circus}

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

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

\begin{circus}      
    A \defs 
        p: \nat @ (
            p := 0;
            \circvar\ p: \nat @ (
                p := 1;
                \circvar\ p: \nat @
                    p := 2
            )
        )
\end{circus}

\begin{circus}      
      @ A(1)
\circend
\end{circus}

:: Hiding not allowed
\begin{circus}  
    \circprocess Err_E4 \defs Err_P; (Err_P \hide \lchanset in \rchanset)
\end{circus}

