TesteNewPar.tex 22.1 KB
edit raw blame history

%%%%%%%%%TesteNewPar.tex : CASOS DE TESTE PARA A ESTRATÉGIA DE TRADUÇÃO DO PARALELISMO COM MUDANÇA DA AST

%%%Deveremos ter uma atenção especial, pois o resultado da transformação de algumas ações está no formato "a -> SKIP ; b -> SKIP ; SKIP", ao invés de "a -> b -> SKIP". Atualizei apenas as transformações de P e de Rec1, aqui...

\begin{circus}
	\circchannel a , b , c
\end{circus}

\begin{circus}
	\circchannel p : \nat
\end{circus}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%TESTE DE RENAMING%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%23/05/2011 15:31:26 net.sourceforge.czt.z.util.WarningManager doWarn
%AVISO: Process signature for rename process still requires update on all used communications.
%	Process...: RENPROC
%		- could not use pretty printer because 'net.sourceforge.czt.util.CztException: net.sourceforge.czt.session.SourceLocator%$SourceLocatorException: Cannot find source for section Specification with czt.path=null'

%\begin{circus}
%	\circprocess RENACT \circdef \circbegin
%\end{circus}

%\begin{circusaction}
%	A \circdef a \then \Skip
%\end{circusaction}

%\begin{circusaction}
%	\circspot A %(\lcircrename a := b \rcircrename)
%\end{circusaction}

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

%\begin{circus}
%	\circprocess RENPROC \circdef RENACT \lcircrename a := b \rcircrename
%\end{circus}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%OK%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{circus}
%	\circprocess EC \circdef \circbegin
%\end{circus}

%\begin{circusaction}
%\circspot
%	a \then \Skip \extchoice b \then \Skip
%\end{circusaction}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%OK%%%%%%%%%%%%%%%%
%\begin{circus}
%	\circprocess PA \circdef \circbegin
%\end{circus}

%\begin{circusaction}
%\circspot
%	a \then \Skip
%\end{circusaction}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess Rec1 \circdef \circbegin %A transformação da árvore de Rec está correta, e ela está sendo aceita pelo pré-processador de JCircus
\end{circus}

\begin{circusaction}
	A \circdef a \then B
\end{circusaction}

\begin{circusaction}
	B \circdef a \then C
\end{circusaction}

\begin{circusaction}
	C \circdef a \then \Skip
\end{circusaction}

\begin{circusaction}
	D \circdef a \then D
\end{circusaction}

\begin{circusaction}
\circspot
	A \interleave B \interleave C
\end{circusaction}

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

%%%%%RESULTADO DA TRANSFORMAÇÃO DA ÁRVORE PARA Rec1:

%process Rec1 ^= begin
%          A ^= (a -> SKIP ; (a -> SKIP ; (a -> SKIP ; SKIP)))
%          B ^= (a -> SKIP ; (a -> SKIP ; SKIP))
%          C ^= (a -> SKIP ; SKIP)
%          D ^= uXD @ (a -> SKIP ; XD)
%          $$mainAction_L55C0 ^= (((((a0 -> SKIP ; SKIP) ; SKIP) ; (((a0 -> SKIP ; SKIP) ; SKIP) ; (((a0 -> SKIP ; SKIP) ; SKIP) ; SKIP))) || (((a1 -> SKIP %; SKIP) ; SKIP) ; (((a1 -> SKIP ; SKIP) ; SKIP) ; SKIP))) || (((a2 -> SKIP ; SKIP) ; SKIP) ; %SKIP))
%          PreviousA ^= (a -> SKIP ; (a -> SKIP ; (a -> SKIP ; SKIP)))
%          PreviousB ^= (a -> SKIP ; (a -> SKIP ; SKIP))
%          PreviousC ^= (a -> SKIP ; SKIP)
%          PreviousD ^= uXD @ (a -> SKIP ; XD)
%          PreviousMA ^= ((((a -> SKIP ; SKIP) ; ((a -> SKIP ; SKIP) ; ((a -> SKIP ; SKIP) ; SKIP))) || ((a -> SKIP ; SKIP) ; ((a -> SKIP ; SKIP) ; SKIP))) %|| ((a -> SKIP ; SKIP) ; SKIP))
%end


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess Rec2 \circdef \circbegin
\end{circus}

\begin{circusaction}
	A \circdef a \then B
\end{circusaction}

\begin{circusaction}
	B \circdef a \then C
\end{circusaction}

\begin{circusaction}
	C \circdef a \then A
\end{circusaction}

\begin{circusaction}
	D \circdef a \then D
\end{circusaction}

\begin{circusaction}
\circspot
	A \interleave B \interleave C
\end{circusaction}

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

%%%RESULTADO DA TRANSFORMAÇÃO DA ÁRVORE PARA Rec2:

%process Rec2 ^= begin
%          A ^= a -> uXB @ a -> a -> a -> XB
%          B ^= a -> a -> a -> uXB @ a -> a -> a -> XB
%          C ^= a -> a -> uXB @ a -> a -> a -> XB
%          D ^= uXD @ a -> XD
%          $$mainAction_L136C0 ^= ((a0 -> uXB @ a0 -> a0 -> a0 -> XB || a1 -> a1 -> a1 -> uXB @ a0 -> a0 -> a0 -> XB) || a2 -> a2 -> uXB @ a0 -> a0 -> a0 -> XB)
%          PreviousA ^= a -> uXB @ a -> a -> a -> XB
%          PreviousB ^= a -> a -> a -> uXB @ a -> a -> a -> XB
%          PreviousC ^= a -> a -> uXB @ a -> a -> a -> XB
%          PreviousD ^= uXD @ a -> XD
%          PreviousMA ^= ((a -> uXB @ a -> a -> a -> XB || a -> a -> a -> uXB @ a -> a -> a -> XB) || a -> a -> uXB @ a -> a -> a -> XB)
%end

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%TESTA O CASO ESPECIAL 1, EM QUE PODEMOS TER PARALELISMO ENTRE AÇÕES PREFIXADAS COM MAIS DE UM CANAL VISÍVEL%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess P \circdef \circbegin %A transformação da árvore de P está correta, e aceita pelo pré-processador (EnvLoadingVisitor) de JCircus
\end{circus}

\begin{circusaction}

\circspot
	%(a \then c \then \Skip) \lpar | \lchanset a, c \rchanset | \rpar
	((a \then c %\then b
		\then \Skip
	)
	\interleave
	(((a \then c %\then b
		\then \Skip
	)
	\interleave
	(a \then c %\then b
		\then \Skip
	)
	)
	%\lpar | \lchanset a, b, c \rchanset | \rpar
	%((a \then c \then \Skip)
	%\interleave
	%(a \then c \then \Skip))
	))
\end{circusaction}
\begin{circus}
\circend
\end{circus}

%%Resultado da transformação da árvore sintática de P:
%process P ^= begin
%process P ^= begin
          %$$mainAction_L168C0 ^=

%(((((

%a0 -> ((((a0 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP) [] a1 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> %SKIP) [] c4 -> SKIP)) [] a2 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a3 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> %SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a4 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a1 -> ((((a0 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP) [] a1 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a2 %-> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a3 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 %-> SKIP)) [] a4 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP))) [] a2 -> ((((a0 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> %SKIP) [] c3 -> SKIP) [] c4 -> SKIP) [] a1 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a2 -> ((((c0 -> SKIP [] c1 -> %SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a3 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a4 -> ((((c0 %-> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP))) [] a3 -> ((((a0 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 %-> SKIP) [] a1 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a2 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 %-> SKIP) [] c4 -> SKIP)) [] a3 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a4 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 %-> SKIP) [] c3 -> SKIP) [] c4 -> SKIP))) [] a4 -> ((((a0 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP) [] a1 -> ((((c0 -> %SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a2 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] %a3 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP)) [] a4 -> ((((c0 -> SKIP [] c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] %c4 -> SKIP))) || (a0 -> a0 -> c0 -> SKIP || (((a1 -> (a1 -> (c1 -> SKIP [] c3 -> SKIP) [] a3 -> (c1 -> SKIP [] c3 -> SKIP)) [] a3 -> (a1 -> (c1 -> SKIP [] %c3 -> SKIP) [] a3 -> (c1 -> SKIP [] c3 -> SKIP))) || (a2 -> (a2 -> (c2 -> SKIP [] c4 -> SKIP) [] a4 -> (c2 -> SKIP [] c4 -> SKIP)) [] a4 -> (a2 -> (c2 -> %SKIP [] c4 -> SKIP) [] a4 -> (c2 -> SKIP [] c4 -> SKIP)))) || ((a1 -> (a1 -> (c1 -> SKIP [] c2 -> SKIP) [] a2 -> (c1 -> SKIP [] c2 -> SKIP)) [] a2 -> (a1 %-> (c1 -> SKIP [] c2 -> SKIP) [] a2 -> (c1 -> SKIP [] c2 -> SKIP))) || (a3 -> (a3 -> (c3 -> SKIP [] c4 -> SKIP) [] a4 -> (c3 -> SKIP [] c4 -> SKIP)) [] a4 %-> (a3 -> (c3 -> SKIP [] c4 -> SKIP) [] a4 -> (c3 -> SKIP [] c4 -> SKIP)))))))
          %PreviousMA ^= (a -> a -> c -> SKIP || (a -> a -> c -> SKIP || ((a -> a -> c -> SKIP || a -> a -> c -> SKIP) || (a -> a -> c -> SKIP || a -> a -> %c -> SKIP))))
%end
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%Process Q, action null: A prefixing action must be a direct branch of an external choice%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%A TRANSFORMAÇÃO DE Q LEVAVA A ESCOLHAS EXTERNAS DE SEQACTIONS, MAS ISSO JÁ FOI RESOLVIDO...%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess Q \circdef \circbegin %A transformação da árvore de Q está correta
\end{circus}
\begin{circusaction}
\circspot
	(a \then \Skip \extchoice b \then \Skip) \lpar | \lchanset a, b, c \rchanset | \rpar ((a \then \Skip \extchoice b \then \Skip)
	\interleave
	(((a \then \Skip \extchoice b \then \Skip)
	\interleave
	(a \then \Skip \extchoice b \then \Skip))
	\lpar | \lchanset a, b, c \rchanset | \rpar
	((a \then \Skip \extchoice b \then \Skip)
	\interleave
	(a \then \Skip \extchoice b \then \Skip))))
\end{circusaction}
\begin{circus}
\circend
\end{circus}

%process Q ^= begin
%          $$mainAction_L205C0 ^= ((((((((a0 -> SKIP [] a1 -> SKIP) [] a2 -> SKIP) [] a3 -> SKIP) [] a4 -> SKIP) ; SKIP) ; SKIP) [] ((((((b0 -> SKIP [] b1 -> SKIP) [] b2 -> SKIP) [] b3 -> SKIP) [] b4 -> SKIP) ; SKIP) ; SKIP)) || ((((a0 -> SKIP ; SKIP) ; SKIP) [] ((b0 -> SKIP ; SKIP) ; SKIP)) || ((((((a1 -> SKIP [] a3 -> SKIP) ; SKIP) ; SKIP) [] (((b1 -> SKIP [] b3 -> SKIP) ; SKIP) ; SKIP)) || ((((a2 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) [] (((b2 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP))) || (((((a1 -> SKIP [] a2 -> SKIP) ; SKIP) ; SKIP) [] (((b1 -> SKIP [] b2 -> SKIP) ; SKIP) ; SKIP)) || ((((a3 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) [] (((b3 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP))))))
%          PreviousMA ^= (((a -> SKIP ; SKIP) [] (b -> SKIP ; SKIP)) || (((a -> SKIP ; SKIP) [] (b -> SKIP ; SKIP)) || ((((a -> SKIP ; SKIP) [] (b -> SKIP ; SKIP)) || ((a -> SKIP ; SKIP) [] (b -> SKIP ; SKIP))) || (((a -> SKIP ; SKIP) [] (b -> SKIP %; SKIP)) || ((a -> SKIP ; SKIP) [] (b -> SKIP ; SKIP))))))
%end

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess Int1 \circdef \circbegin %A transformação da árvore de Int1 está correta
\end{circus}

\begin{circusaction}

\circspot
	(a \then \Skip)
	\lpar | \lchanset a \rchanset | \rpar
	((a \then \Skip)
	\interleave
	(a \then \Skip))
\end{circusaction}

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

%%%%%%%%%Resultado da transformação da árvore para Int1%%%%%%%%%%%%
%process Int1 ^= begin
%          $$mainAction_L236C0 ^= ((((a0 -> SKIP [] a1 -> SKIP) ; SKIP) ; SKIP) || (((a0 -> SKIP ; SKIP) ; SKIP) || ((a1 -> SKIP ; SKIP) ; SKIP)))
%          PreviousMA ^= ((a -> SKIP ; SKIP) || ((a -> SKIP ; SKIP) || (a -> SKIP ; SKIP)))
%end

\begin{circus}
	\circprocess Int2 \circdef \circbegin %A transformação da árvore de Int2 está correta
\end{circus}
\begin{circusaction}
\circspot
	(a \then \Skip)
	\lpar | \lchanset a \rchanset | \rpar
	((a \then \Skip)
	\interleave
	(a \then \Skip))
\end{circusaction}
\begin{circus}
\circend
\end{circus}

%%%%%%%RESULTADO PARA A TRANSFORMAÇÃO DE ÁRVORE PARA Int2
%process Int2 ^= begin
%          $$mainAction_L252C0 ^= ((((a0 -> SKIP [] a1 -> SKIP) ; SKIP) ; SKIP) || (((a0 -> SKIP ; SKIP) ; SKIP) || ((a1 -> SKIP ; SKIP) ; SKIP)))
%          PreviousMA ^= ((a -> SKIP ; SKIP) || ((a -> SKIP ; SKIP) || (a -> SKIP ; SKIP)))
%end


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%TESTA O CASO ESPECIAL 5, EM QUE PODEMOS TER PARALELISMO ENTRE PROCESSOS...%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
\circprocess IntProc \circdef Int1 \interleave Int2
\end{circus}

%%%%Resultado da transformação da árvore para IntProc. IntProc é transformado em um processo básico
%process IntProc ^= begin
%          PreviousMA ^= (((a -> SKIP ; SKIP) ; SKIP) || (((a -> SKIP ; SKIP) ; SKIP) || ((a -> SKIP ; SKIP) ; SKIP)))
%          PreviousMA ^= (((a -> SKIP ; SKIP) ; SKIP) || (((a -> SKIP ; SKIP) ; SKIP) || ((a -> SKIP ; SKIP) ; SKIP)))
%          $$mainAction ^= ((((((a0 -> SKIP [] a1 -> SKIP) ; SKIP) ; SKIP) ; SKIP) || ((((a0 -> SKIP ; SKIP) ; SKIP) ; SKIP) || (((a1 -> SKIP ; SKIP) ; SKIP) ; SKIP))) || (((((a2 -> SKIP [] a3 -> SKIP) ; SKIP) ; SKIP) ; SKIP) || ((((a2 -> SKIP ; SKIP) ; SKIP) ; SKIP) || (((a3 -> SKIP ; SKIP) ; SKIP) ; SKIP))))
%          PreviousPreviousMA ^= (((a -> SKIP ; SKIP) ; SKIP) || (((a -> SKIP ; SKIP) ; SKIP) || ((a -> SKIP ; SKIP) ; SKIP)))
%          PreviousPreviousMA ^= (((a -> SKIP ; SKIP) ; SKIP) || (((a -> SKIP ; SKIP) ; SKIP) || ((a -> SKIP ; SKIP) ; SKIP)))
%          PreviousMA ^= ((((a -> SKIP ; SKIP) ; SKIP) || (((a -> SKIP ; SKIP) ; SKIP) || ((a -> SKIP ; SKIP) ; SKIP))) || (((a -> SKIP ; SKIP) ; SKIP) || (((a -> SKIP ; SKIP) ; SKIP) || ((a -> SKIP ; SKIP) ; SKIP))))
%end


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%TESTA RAMOS QUE SÃO AÇÕES SEQUENCIAIS%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess R \circdef \circbegin %A transformação da árvore de R está correta
\end{circus}
\begin{circusaction}
\circspot
	(a \then \Skip \circseq b \then \Skip)
	\lpar | \lchanset a, b, c \rchanset | \rpar
	((a \then \Skip \circseq b \then \Skip)
	\interleave
	((a \then \Skip \circseq b \then \Skip
	\interleave
	a \then \Skip \circseq b \then \Skip)
	\lpar | \lchanset a, b, c \rchanset | \rpar
	(a \then \Skip \circseq b \then \Skip
	\interleave
	a \then \Skip \circseq b \then \Skip)))
\end{circusaction}
\begin{circus}
\circend
\end{circus}

%process R ^= begin
%          $$mainAction_L300C0 ^= ((((((((a0 -> SKIP [] a1 -> SKIP) [] a2 -> SKIP) [] a3 -> SKIP) [] a4 -> SKIP) ; SKIP) ; SKIP) ; ((((((b0 -> SKIP [] b1 -> SKIP) [] b2 -> SKIP) [] b3 -> SKIP) [] b4 -> SKIP) ; SKIP) ; SKIP)) || ((((a0 -> SKIP ; SKIP) ; SKIP) ; ((b0 -> SKIP ; SKIP) ; SKIP)) || ((((((a1 -> SKIP [] a3 -> SKIP) ; SKIP) ; SKIP) ; (((b1 -> SKIP [] b3 -> SKIP) ; SKIP) ; SKIP)) || ((((a2 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) ; (((b2 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP))) || (((((a1 -> SKIP [] a2 -> SKIP) ; SKIP) ; SKIP) ; (((b1 -> SKIP [] b2 -> SKIP) ; SKIP) ; SKIP)) || ((((a3 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) ; (((b3 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP))))))
%          PreviousMA ^= (((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP)) || (((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP)) || ((((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP)) || ((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP))) || (((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP)) || ((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP))))))
%end
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%TESTA RAMOS QUE SÃO AÇÕES DE CHAMADA SEM RECURSÃO%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess S \circdef \circbegin %
\end{circus}
\begin{circusaction}
	Act \circdef a \then b \then c \then \Skip
\end{circusaction}
\begin{circusaction}
\circspot
	(Act)
	\lpar | \lchanset a, b, c \rchanset | \rpar
	((Act)
	\interleave
	((Act
	\interleave
	Act)
	\lpar | \lchanset a, b, c \rchanset | \rpar
	(Act
	\interleave
	Act)))
\end{circusaction}
\begin{circus}
\circend
\end{circus}

%process S ^= begin
%          Act ^= (a -> SKIP ; (b -> SKIP ; (c -> SKIP ; SKIP)))
%          $$mainAction_L337C0 ^= ((((((((a0 -> SKIP [] a1 -> SKIP) [] a2 -> SKIP) [] a3 -> SKIP) [] a4 -> SKIP) ; SKIP) ; SKIP) ; (((((((b0 -> SKIP [] b1 -> SKIP) [] b2 -> SKIP) [] b3 -> SKIP) [] b4 -> SKIP) ; SKIP) ; SKIP) ; (((((((c0 -> SKIP [] %c1 -> SKIP) [] c2 -> SKIP) [] c3 -> SKIP) [] c4 -> SKIP) ; SKIP) ; SKIP) ; SKIP))) || ((((a0 -> SKIP ; SKIP) ; SKIP) ; (((b0 -> SKIP ; SKIP) ; SKIP) ; (((c0 -> SKIP ; SKIP) ; SKIP) ; SKIP))) || ((((((a1 -> SKIP [] a3 -> SKIP) ; SKIP) ; SKIP) ; ((((b1 -> SKIP [] b3 -> SKIP) ; SKIP) ; SKIP) ; ((((c1 -> SKIP [] c3 -> SKIP) ; SKIP) ; SKIP) ; SKIP))) || ((((a2 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) ; ((((b2 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP) ; ((((c2 -> SKIP [] c4 -> SKIP) ; SKIP) ; SKIP) ; SKIP)))) || (((((a1 -> SKIP [] a2 -> SKIP) ; SKIP) ; SKIP) ; ((((b1 -> SKIP [] b2 -> SKIP) ; SKIP) ; SKIP) ; ((((c1 -> SKIP [] c2 -> SKIP) ; SKIP) ; SKIP) ; SKIP))) || ((((a3 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) ; ((((b3 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP) ; ((((c3 -> SKIP [] c4 -> SKIP) ; SKIP) ; SKIP) ; SKIP)))))))
%          PreviousAct ^= (a -> SKIP ; (b -> SKIP ; (c -> SKIP ; SKIP)))
%          PreviousMA ^= (((a -> SKIP ; SKIP) ; ((b -> SKIP ; SKIP) ; ((c -> SKIP ; SKIP) ; SKIP))) || (((a -> SKIP ; SKIP) ; ((b -> SKIP ; SKIP) ; ((c -> SKIP ; SKIP) ; SKIP))) || ((((a -> SKIP ; SKIP) ; ((b -> SKIP ; SKIP) ; ((c -> SKIP ; SKIP) ; SKIP))) || ((a -> SKIP ; SKIP) ; ((b -> SKIP ; SKIP) ; ((c -> SKIP ; SKIP) ; SKIP)))) || (((a -> SKIP ; SKIP) ; ((b -> SKIP ; SKIP) ; ((c -> SKIP ; SKIP) ; SKIP))) || ((a -> SKIP ; SKIP) ; ((b -> SKIP ; SKIP) ; ((c -> SKIP ; SKIP) ; SKIP)))))))
%end
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%TESTA RAMOS QUE SÃO AÇÕES GUARDADAS%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%No paralelismo entre ações guardadas, o predicado é mantido intacto, e as ações são mudadas normalmente
\begin{circus}
	\circprocess GUARD \circdef \circbegin %A transformação da árvore de R está correta
\end{circus}
\begin{circusaction}
\circspot
	(\lcircguard true \rcircguard \circguard (a \then \Skip \circseq b \then \Skip))
	\lpar | \lchanset a, b, c \rchanset | \rpar
	((a \then \Skip \circseq b \then \Skip)
	\interleave
	((a \then \Skip \circseq b \then \Skip
	\interleave
	a \then \Skip \circseq b \then \Skip)
	\lpar | \lchanset a, b, c \rchanset | \rpar
	(a \then \Skip \circseq b \then \Skip
	\interleave
	a \then \Skip \circseq b \then \Skip)))
\end{circusaction}
\begin{circus}
\circend
\end{circus}

%%%%%Resultado da transformação da árvore para GUARD:
%process GUARD ^= begin
%          $$mainAction_L371C0 ^= (((PREDICADO) & (((a -> SKIP ; SKIP) ; SKIP) ; ((b -> SKIP ; SKIP) ; SKIP))) || ((((a0 -> SKIP ; SKIP) ; SKIP) ; ((b0 -> SKIP ; SKIP) ; SKIP)) || ((((((a1 -> SKIP [] a3 -> SKIP) ; SKIP) ; SKIP) ; (((b1 -> SKIP [] b3 -> SKIP) ; SKIP) ; SKIP)) || ((((a2 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) ; (((b2 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP))) || (((((a1 -> SKIP [] a2 -> SKIP) ; SKIP) ; SKIP) ; (((b1 -> SKIP [] b2 -> SKIP) ; SKIP) ; SKIP)) || ((((a3 -> SKIP [] a4 -> SKIP) ; SKIP) ; SKIP) ; (((b3 -> SKIP [] b4 -> SKIP) ; SKIP) ; SKIP))))))
%          PreviousMA ^= (((PREDICADO) & ((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP))) || (((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP)) || ((((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP)) || ((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP))) || (((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP)) || ((a -> SKIP ; SKIP) ; (b -> SKIP ; SKIP))))))
%end
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%TESTA O CASO ESPECIAL DO PARALELISMO DE PARALELISMOS PREFIXADOS%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
	\circprocess PARPARPREFIX \circdef \circbegin
\end{circus}

\begin{circusaction}
\circspot (a \then (a \then \Skip \interleave a \then \Skip)) \interleave (a \then (a \then \Skip \interleave a \then \Skip))
\end{circusaction}

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

%%%%%%%%%%%Resultado da transformação da árvore para PARPARPREFIX
%process ParParPrefix ^= begin
%          $$mainAction_L402C0 ^= (((a0 -> SKIP ; SKIP) ; (((a0 -> SKIP ; SKIP) ; SKIP) || ((a1 -> SKIP ; SKIP) ; SKIP))) || ((a2 -> SKIP ; SKIP) ; (((a2 -> SKIP ; SKIP) ; SKIP) || ((a3 -> SKIP ; SKIP) ; SKIP))))
%          PreviousMA ^= ((a -> SKIP ; ((a -> SKIP ; SKIP) || (a -> SKIP ; SKIP))) || (a -> SKIP ; ((a -> SKIP ; SKIP) || (a -> SKIP ; SKIP))))
%end

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%TESTA O CASO ESPECIAL DE PARALELISMOS ENTRE PROCESSOS (COLOCAMOS EM UM ARQUIVO A PARTE, PORQUE AQUI, POR MOTIVOS DESCONHECIDOS, ESTÁ DANDO ERRO DE COMPILAÇÃO)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\begin{circus}
%	\circprocess PARAMP \circdef
%		%x : \nat \circspot
%	\circbegin
%\end{circus}
%\begin{circusaction}
%\circspot p.5 \then \Skip
%\end{circusaction}
%\begin{circus}
%\circend
%\end{circus}

%\begin{circus}
%\circprocess PARAMPROC \circdef PARAMP (2) \interleave PARAMP (3)
%\end{circus}