%--Exemplo simples de especificação no latex do novo parser
%Tipo livre
%C:\Users\sam\Mestrado\JCircus3\JCircus\src\jcircus\exemplo_czt_1_5_0.tex
\begin{zed}
  SAM ::= sam1 | sam2
\end{zed}
%Definição axiomática
\begin{axdef}
x: SAM \where x = sam1
\end{axdef}

%Paragrafo de canais
\begin{circus}
	\circchannel chan, c, %bidimensional
				chan3 %bidimensional
				: \{0, 2, 4, 5, 6, 7\} \cross \nat%\{0, 2, 4, 5, 6, 7\} 
\end{circus}

\begin{circus}
	\circchannel 
		chan5 %unidimensional
		: \nat \cross \nat
\end{circus}


%Parágrafo de processo
\begin{circus}
	\circprocess P \circdef \circbegin
\end{circus}

\begin{circusaction}
	\circspot 
		chan.3.3
		\then chan.6.5
		\then \Skip
\end{circusaction}

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

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

\begin{circusaction}
	\circspot 
		(c?x.5 % A ação principal de Q é uma escolha externa entre duas prefixing actions, sendo uma delas com comunicação complexa, 
			    % em que há um input (?) em um campo que não é o último campo da comunicação de chan. 
			    % Assim, a comunicação efetuada por chan, na primeira prefixing action, é complexa.
		\then c.6.5
		\then \Skip)
		\extchoice
		(c.6?y \then c.6.5 \then \Skip)
\end{circusaction}

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

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

\begin{circusaction}
	\circspot 
		(chan?x.5 %QInt é uma escolha interna entre duas prefixing actions, em que uma delas tem uma comunicação complexa. 
		\then chan.7.5
		\then \Skip) 
		\intchoice
		(chan.6.5 \then chan.7.6 \then \Skip)
		
\end{circusaction}

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

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

\begin{circusaction}
	\circspot 
		(chan?x.5
		\then chan.7.5
		\then \Skip) 
		\lpar | \lchanset chan \rchanset | \rpar
		(chan.6.5 \then chan.7.6 \then \Skip)
		
\end{circusaction}

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

%(VERIFICADO) R será uma sincronização simples entre P e Q. Como Q se encaixa em um dos casos de comunicação complexa, chan será um GeneralChannel
% bidimensional, independente da condição de multisincronização (se simples ou multi)
\begin{circus}
\circprocess R \circdef P \lpar \lchanset chan \rchanset \rpar Q
\end{circus}

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

\begin{circusaction}
	\circspot 
		chan5.6!5
		\then chan5.7!5
		\then \Skip
\end{circusaction}

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

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

\begin{circusaction}
	\circspot
		chan5.6?x
		\then chan5.7?y 
		\then \Skip
\end{circusaction}

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

%Sincronização simples entre S e T, em que nenhum dos dois processos possui prefixing action com comunicação complexa, e em que chan5 não é utilizado nenhuma vez em ambiente multi-sincronizado. 
	%Assim, chan5 deve ser unidimensional
\begin{circus}
\circprocess U \circdef S \lpar \lchanset chan5 \rchanset \rpar T
\end{circus}

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

\begin{circusaction}
	\circspot 
		chan3.6!5
		\then chan3.7!5 
		\then \Skip
\end{circusaction}

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

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

\begin{circusaction}
	\circspot 
		chan3.6?x
		\then chan3.7?y 
		\then \Skip
\end{circusaction}

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

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

\begin{circusaction}
	\circspot
		chan3.6?x
		\then chan3.7?y 
		\then \Skip
\end{circusaction}

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

\begin{circus}
\circprocess Z \circdef (V \lpar \lchanset chan3 \rchanset \rpar XIS) \lpar
\lchanset chan3 \rchanset \rpar Y
\end{circus}

\begin{circus}
\circprocess DABLIU \circdef (S \lpar \lchanset chan3 \rchanset \rpar XIS)
\end{circus}

%\begin{circus}
%\circprocess IC \circdef (P \intchoice Q) \extchoice V
%\end{circus}

\begin{circus}
\circprocess BE \circdef \circbegin \\
	\circspot chan.5?x \then \chan.6.5 \then \Skip \\
	\circend \\
\end{circus}

\begin{circus}
\circprocess CE \circdef \circbegin \\
	\circspot chan.5?x \then \chan.6.5 \then \Skip \\
	\circend \\
\end{circus}

\begin{circus}
\circprocess GuardsT \circdef BE \lpar \lchanset chan \rchanset \rpar (P \lpar \lchanset chan \rchanset \rpar CE)
\end{circus}
