%\documentclass{article}

%\usepackage[margin=30mm,a4paper]{geometry}
%\usepackage{circus}

%\AddToShipoutPicture{\AtTextLowerLeft{\framebox(\LenToUnit{\textwidth},\LenToUnit{\textheight}){}}}

%\begin{document}

\begin{zsection}
  \SECTION CircusFormalSyntax \parents ZFormalSyntax
\end{zsection}

\begin{zed}
N == NAME\\
Par == Paragraph\\
CSExp ::= csname \ldata N \rdata |\\
cs \ldata \seq N \rdata |\\
csunion \ldata CSExp \cross CSExp \rdata |\\
csinter \ldata CSExp \cross CSExp \rdata |\\
csminus \ldata CSExp \cross CSExp \rdata\\
NSExp ::= ns \ldata \seq N \rdata |\\
nsunion \ldata NSExp \cross NSExp \rdata |\\
nsinter \ldata NSExp \cross NSExp \rdata |\\
nsminus \ldata NSExp \cross NSExp \rdata\\
\end{zed}

\begin{axdef}
BOOL,T,F: N
\end{axdef}

\begin{zed}
Program ::= program \ldata \seq CircusPar \rdata
\&
CircusPar ::= zparagraphdeclaration \ldata Par \rdata |\\
channeldeclaration \ldata CDecl \rdata |\\
channelsetdeclaration \ldata N \cross CSExp \rdata |\\
processdeclaration \ldata ProcDecl \rdata
\&
SimpleCDecl ::= simplecdecl \ldata \seq_1 N \rdata |\\
typedsimplecdecl \ldata \seq_1 N \cross Expression \rdata |\\
genericcdecl \ldata Formals \cross \seq_1 N \cross Expression \rdata\\
\&
CDecl ::= cdecl \ldata \seq_1 SimpleCDecl \rdata
\&
ProcDecl ::= simpleprocessdeclaration \ldata N \cross ProcDef \rdata |\\
genericprocessdeclaration \ldata N \cross Formals \cross ProcDef \rdata\\
\&
ProcDef ::= processdefinition \ldata Proc \rdata |\\
parameterisedprocessdefinition \ldata DeclPart \cross Proc \rdata |\\
indexedprocessdefinition \ldata DeclPart \cross Proc \rdata
\&
ProcessState ::= stateExpr \ldata Expression \rdata |\\
stateDecl \ldata DeclName \cross Expression \rdata\\
\&
Proc ::= proc \ldata \seq PPar \cross ProcessState \cross \seq PPar \cross Action \rdata |\\
processsequentialcomposition \ldata Proc \cross Proc \rdata |\\
processexternalchoice \ldata Proc \cross Proc \rdata |\\
processinternalchoice \ldata Proc \cross Proc \rdata |\\
procesparallelcomposition \ldata Proc \cross CSExp \cross Proc \rdata |\\
processinterleave \ldata Proc \cross Proc \rdata |\\
processhiding \ldata Proc \cross CSExp \rdata |\\
processinstantiation \ldata DeclPart \cross ProcDef \cross \seq_1 Expression \rdata |\\
processcallinstantiation \ldata N \cross \seq_1 Expression \rdata |\\
processcall \ldata N \rdata |\\
indexedprocessinstantiation \ldata DeclPart \cross ProcDef \cross \seq_1 Expression \rdata |\\
incexedprocesscallinstantiation \ldata N \cross \seq_1 Expression \rdata |\\
processrenaming \ldata Proc \cross \seq_1 N \cross \seq_1 N \rdata |\\
genericprocessinstantiation \ldata N \cross \seq_1 Expression \rdata |\\
iteratedprocesssequentialcomposition \ldata DeclPart \cross Proc \rdata |\\
iteratedprocessexternalchoice \ldata DeclPart \cross Proc \rdata |\\
iteratedprocessinternalchoice \ldata DeclPart \cross Proc \rdata |\\
iteratedprocessparallelcomposition \ldata CSExp \cross DeclPart \cross Proc \rdata |\\
iteratedprocessinterleave \ldata DeclPart \cross Proc \rdata\\
\&
PPar ::= zparagraph \ldata Par \rdata |\\
actionparagraph \ldata N \cross ParAction \rdata |\\
namesetparagraph \ldata N \cross NSExp \rdata\\
\&
ParAction ::= paraction \ldata Action \rdata |\\
parameterisedparaction \ldata DeclPart \cross ParAction \rdata\\
\&
Action ::= schemaaction \ldata Expression \rdata |\\
commandaction \ldata Command \rdata |\\
namedaction \ldata N \rdata |\\
cspaction \ldata CSPAction \rdata |\\
renamingaction \ldata Action \cross \seq_1 (N \cross Expression) \rdata\\
\&
CParameter ::= inputparameter \ldata N \rdata |\\
guardedinputparameter \ldata N \cross Predicate \rdata |\\
outputparameter \ldata Expression \rdata |\\
simpleparameter \ldata Expression \rdata\\
\&
Comm ::= communication \ldata N \cross \seq CParameter \rdata |\\
genericcommunication \ldata N \cross \seq_1 Expression \cross \seq CParameter \rdata\\
\&
Command ::= assignment \ldata \seq_1(N \cross Expression) \rdata |\\
ifcommand \ldata GActions \rdata |\\
variableblock \ldata DeclPart \cross Action \rdata |\\
actionspecification \ldata \seq_1 N \cross Predicate \cross Predicate \rdata |\\
assumption \ldata Predicate \rdata |\\
coercion \ldata Predicate \rdata |\\
substitutionbyvalue \ldata DeclPart \cross Action \rdata |\\
substitutionbyresult \ldata DeclPart \cross Action \rdata |\\
substitutionbyvalueresult \ldata DeclPart \cross Action \rdata\\
\&
GActions ::= gactions \ldata \seq_1 (Predicate \cross Action) \rdata
\&
CSPAction ::= skip | stop | chaos |\\
interruptaction \ldata Action \cross Action \rdata |\\
prefixedaction \ldata Comm \cross Action \rdata |\\
guardedaction \ldata Predicate \cross Action \rdata |\\
actionsequentialcomposition \ldata Action \cross Action \rdata |\\
actionexternalchoice \ldata Action \cross Action \rdata |\\
actioninternalchoice \ldata Action \cross Action \rdata |\\
actionparallelcomposition\ldata Action \cross NSExp \cross CSExp \cross NSExp \cross Action \rdata |\\
actioninterleave \ldata Action \cross NSExp \cross NSExp \cross Action \rdata |\\
actionhding \ldata Action \cross CSExp \rdata |\\
paractioninstantiation \ldata ParAction \cross \seq_1 Expression \rdata |\\
recursiveaction \ldata N \cross Action \rdata |\\
iteratedactionsequentialcomposition \ldata DeclPart \cross Action \rdata |\\
iteratedactionexternalchoice \ldata DeclPart \cross Action \rdata |\\
iteratedactioninternalchoice \ldata DeclPart \cross Action \rdata |\\
iteratedactionparallelcomposition \ldata CSExp \cross DeclPart \cross NSExp \cross Action \rdata |\\
iteratedactioninterleave \ldata DeclPart \cross NSExp \cross Action \rdata
\end{zed}
