%%
%% This is file `circus.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% circus.dtx  (with options: `package')
%%
%% This is a generated file
%%
%% Copyright (C) 2008 Leo Freitas.
%% University of York All rights reserved.
%%
%% This is a generated file for Circus within the
%% Community Z Tools (CZT). It is based on the zed-csp.sty
%% package distribution.  Permission is granted to to
%% customize the declarations in this file to serve the
%% needs of your installation.  However, no permission
%% is granted to distribute a modified version of this
%% file under its original name.
%%
\def\fileversion{v.1.0}
\def\filedate{2008/10/01}
\def\filedesc{Circus style file by the Community Z Tools}

\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{circus}
    [\filedate\space\fileversion\space \filedesc]
\message{`\filedesc'\space \fileversion\space <\filedate>}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Design guidelines:
%   1) keep it minimal + simple + consistent
%   2) for machine readable Circus only
%   3) identify code sources (when different)
%   4) normalise definitions for consistency
%   5) complete missing cases (use common sense)
%   6) keep it well documented, but not verbose
%   7) order of definitions from Circus.xsd, circus_prelude.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Package options - zed.sty (old version of zed-csp.sty)        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% Call czt.sty with the same options as given for circus.sty
\RequirePackageWithOptions{czt}[2008/10/01]

% create conditionals for each option available, init=false
\newif\if@ctkkeyword@ \@ctkkeyword@false

% Pass czt.sty options to its package
\DeclareOption{lucida}{\PassOptionsToPackage{lucida}{czt}}
\DeclareOption{color}{\PassOptionsToPackage{color}{czt}}
\DeclareOption{colour}{\PassOptionsToPackage{colour}{czt}}
\DeclareOption{mathit}{\PassOptionsToPackage{mathit}{czt}}
\DeclareOption{mathrm}{\PassOptionsToPackage{mathrm}{czt}}
\DeclareOption{tkkeyword}{\PassOptionsToPackage{tkkeyword}{czt}}
\DeclareOption{cntglobally}{\PassOptionsToPackage{cntglobally}{czt}}
\DeclareOption{cntbychapter}{\PassOptionsToPackage{cntbychapter}{czt}}
\DeclareOption{cntbysection}{\PassOptionsToPackage{cntbysection}{czt}}

% New options from this package
\DeclareOption{ctkkeyword}{\PackageInfo{circus}{'ctkkeyword' option chosen} \@ctkkeyword@true}

% default option as using math italics for mathcode names.
\ExecuteOptions{mathit,colour,cntglobally}
\ProcessOptions\relax

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Treating colours                                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% If colouring is available
\if@color@
  \PackageInfo{circus}{Rendering Circus math mode with colours}

  % check whether to load color package or not
  \@ifpackageloaded{color}{%
        \relax
  }{%
        \PackageInfo{circus}{Package `color' loaded with `dvipsnames' \MessageBreak and `usenames' options}
        \RequirePackage[dvipsnames,usenames]{color}
  }

  \definecolor{CSPBoxColor}{cmyk}{1,0,1,0}% Green
  \definecolor{MetaColor}{cmyk}{0,0.61,0.87,0}% Orange
  \definecolor{CSPColor}{cmyk}{0.50,1,0,0}% Plum

  \PackageInfo{circus}{Circus colours defined as:\MessageBreak%
    \space\space CSPBoxColor\space\space          = cmyk(   1,   0,   1,0) \MessageBreak%
    \space\space MetaColor\space\space\space      = cmyk(   0,0.61,0.87,0) \MessageBreak%
    \space\space CSPColor\space\space\space\space = cmyk(0.50,   1,   0,0)}%

\else
  \PackageInfo{circus}{Rendering Circus math mode in monochrome.}

  \@ifpackageloaded{color}{\relax}{\def\color#1{\relax}}
\fi

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Loading mathematical symbols from AMS/Lucuida fonts           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% declares the math version for fonts as circus -
% there is no need to create a new math version for Circus
%\DeclareMathVersion{circus}
%\PackageInfo{circus}{Creating `circus' math version}

\@ifpackageloaded{lucidabr}{%
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  % Lucida Bright font setup                                      %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %                                                               %
    \PackageInfo{circus}{Loading Lucida Bright font symbols for Circus}

  %%%%%%%%%%%%%%%%% 1) BRACKETS - brackets used in Circus         %

    \def \csym@lchanset      {{\{}\mkern-5mu{|}~}%{\{\!|~}
    \def \csym@rchanset      {~{|}\mkern-5mu{\}}}%{~|\!\}}
    \DeclareMathSymbol{\csym@lcircindex}{\mathopen}{symbols}{"62}% \lfloor
    \DeclareMathSymbol{\csym@rcircindex}{\mathclose}{symbols}{"63}% \rfloor
    \def \csym@lcircguard    {\zbig{(}}
    \def \csym@rcircguard    {\zbig{)}}
    \def \csym@lschexpract   {\zBig{(}}
    \def \csym@rschexpract   {\zBig{)}}
    \def \csym@linter        {|\!|\hspace{-5pt}[}
    \def \csym@rinter        {]\hspace{-5pt}|\!|}
    %\def \csym@lpar          {{\mid}\mkern -2mu{[}\mkern-1mu}
    %\def \csym@rpar          {\mkern-1mu{]}\mkern -2mu{\mid}}
    \DeclareMathSymbol{\csym@lpar}{\mathopen}{letters}{"82}%
    \DeclareMathSymbol{\csym@rpar}{\mathclose}{letters}{"83}%
    \def \csym@lcircrename   {[}%{\left[}
    \def \csym@rcircrename   {]}%{\right]}

  %%%%%%%%%%%%%%%%% 2) Special symbols used in Circus             %

    \DeclareMathSymbol{\csym@circrefines}{\mathrel}{symbols}{"76}%   \sqsubseteq
    \DeclareMathSymbol{\csym@circsimulates}{\mathrel}{letters}{"EC}% \succcurlyeq
    \DeclareMathSymbol{\csym@circassertref}{\mathrel}{symbols}{"F0}%
    \def \csym@circdef       {\widehat=}
    \DeclareMathSymbol{\csym@spotbase}{\mathord}{symbols}{"0F}%
    \def \csym@circspot      {\zbig{\csym@spotbase}}
    \DeclareMathSymbol{\csym@circindex}{\mathbin}{symbols}{"0C}%

  %%%%%%%%%%%%%%%%% 3) CSP symbols used in Circus                 %

    \def\indexed@op#1{\mathop{\zBIG{\mathstrut#1}}\nolimits} %

    \let \csym@cspthen       \longrightarrow
    \def \csym@prefixcolon   {\zbig{:}}
    \def \csym@cspSemi       {\indexed@op{;}}

    %\def \csym@cspinterleave  {{|}\mkern-2mu{|}\mkern-2mu{|}}
    \DeclareMathSymbol{\csym@cspinterleave}{\mathbin}{stmry}{"39}%
    \def \csym@cspInterleave {\indexed@op{\csym@cspinterleave}}
    %\DeclareMathSymbol{\csym@cspInterleave}{\mathbin}{stmry}{"67}%

    %\def \csym@cspParallel   {\parallel}
    \DeclareMathSymbol{\csym@cspParallelbase}{\mathop}{stmry}{"66}%
    \def \csym@cspParallel    {\mathop{\mathstrut \csym@cspParallelbase}\nolimits}

    \DeclareMathSymbol{\csym@cspextchoice}{\mathbin}{stmry}{"40}%
    \def \csym@cspExtchoice  {\indexed@op{\csym@cspextchoice}}
    %\DeclareMathSymbol{\csym@cspExtchoice}{\mathbin}{stmry}{"65}%

    \DeclareMathSymbol{\csym@cspintchoice}{\mathrel}{symbols}{"7D}%
    \def \csym@cspIntchoice  {\indexed@op{\csym@cspintchoice}}

    \def \csym@circhide      {\zbig{\zsym@solidus}}
    \def \csym@circseq       {\zbig{;}}
    \def \csym@circmu        {\zbig{\zsym@mu}}
    \def \csym@circthen      {\zbig{\longrightarrow}}
    \DeclareMathSymbol{\csym@circelse}{\mathbin}{stmry}{"38}% %\def \csym@circelse {[\!]}
    \DeclareMathSymbol{\csym@circguard}{\mathbin}{stmry}{"4E}% \let \csym@circguard \&

  %%%%%%%%%%%%%%%%% 4) Special CSP symbols                        %

    \DeclareMathSymbol{\csym@tick}{\mathord}{arrows}{"AC}%

  %%%%%%%%%%%%%%%%% 5) Circus prelude symbols                     %

    \def \csym@boolean       {\mathbb B}
    \def \csym@universe      {\mathbb U}

  %%%%%%%%%%%%%%%%% 6) Circus model checking toolkit symbols      %

    \DeclareMathSymbol{\cmcsym@gendj}{\mathbin}{letters}{"F2}%
    \DeclareMathSymbol{\cmcsym@regions}{\mathbin}{symbols}{"0A}% \otimes
    \DeclareMathSymbol{\cmcsym@dsetminusbase}{\mathbin}{symbols}{"26}%
    \def \cmcsym@dsetminus {\zbig{\cmcsym@dsetminusbase}}
    \DeclareMathSymbol{\cmcsym@dcap}{\mathbin}{arrows}{"08}% \lozenge

  %%%%%%%%%%%%%%%%% 7) Special symbols used for Z bags            %

    % added symbols for bags within Circus.sty
    \def \zsym@lbag    {{[}\mkern-3mu{[}~}%{[\![~}
    \def \zsym@rbag    {{]}\mkern-3mu{]}~}%{]\!]~}
    \def \zsym@inbag   {\mbox{\texttt{E}}}
    \def \zsym@uminus{\setbox0=\hbox{$\cup$}\rlap{\hbox
                        to\wd0{\hss\raise0.3ex\hbox{$\scriptscriptstyle{-}$}\hss}}\box0}
    \let \zsym@otimes   \otimes
    \let \zsym@uplus    \uplus
    \let \zsym@bcount   \sharp
    \let \zsym@subbageq \sqsubseteq

}{%
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  % AMS font setup                                                %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %                                                               %
    \PackageInfo{circus}{Loading AMS font symbols for Circus}

  %%%%%%%%%%%%%%%%% 1) BRACKETS - brackets used in Circus         %

    \def \csym@lchanset      {{\{}\mkern-3.5mu{|}~}%{\{\!|~}
    \def \csym@rchanset      {~{|}\mkern-3.5mu{\}}}%{~|\!\}}
    \let \csym@lcircindex    \lfloor
    \let \csym@rcircindex    \rfloor
    \def \csym@lcircguard    {\zbig{(}}
    \def \csym@rcircguard    {\zbig{)}}
    \def \csym@lschexpract   {\zBig{(}}
    \def \csym@rschexpract   {\zBig{)}}
    \def \csym@linter        {|\!|\hspace{-4pt}[}
    \def \csym@rinter        {]\hspace{-4pt}|\!|}
    %\def \csym@lpar          {{\mid}\mkern -2mu{[}\mkern-1mu}
    %\def \csym@rpar          {\mkern-1mu{]}\mkern -2mu{\mid}}
    \DeclareMathSymbol{\csym@lpar}{\mathopen}{stmry}{"4A}%
    \DeclareMathSymbol{\csym@rpar}{\mathclose}{stmry}{"4B}%
    \def \csym@lcircrename   {[}%{\left[}
    \def \csym@rcircrename   {]}%{\right]}

  %%%%%%%%%%%%%%%%% 2) Special symbols used in Circus             %

    \let \csym@circrefines   \sqsubseteq
    \DeclareMathSymbol{\csym@circsimulates}{\mathrel}{AMSa}{"34}% \succcurlyeq
    \DeclareMathSymbol{\csym@circassertref}{\mathrel}{AMSa}{"0D}%
    \def \csym@circdef       {\widehat=}
    \def \csym@circspot      {\zbig{\spot}}
    \let \csym@circindex     \odot

  %%%%%%%%%%%%%%%%% 3) CSP symbols used in Circus                 %

    \def\indexed@op#1{\mathop{\zBIG{\mathstrut#1}}\nolimits} %

    \let \csym@cspthen       \longrightarrow
    \def \csym@prefixcolon   {\zbig{:}}
    \def \csym@cspSemi       {\indexed@op{;}}

    %\def \csym@cspinterleave  {{|}\mkern-2mu{|}\mkern-2mu{|}}
    \DeclareMathSymbol{\csym@cspinterleave}{\mathbin}{stmry}{"39}%
    \def \csym@cspInterleave {\indexed@op{\csym@cspinterleave}}
    %\DeclareMathSymbol{\csym@cspInterleave}{\mathbin}{stmry}{"67}%

    %\def \csym@cspParallel   {\parallel}
    \DeclareMathSymbol{\csym@cspParallelbase}{\mathop}{stmry}{"66}%
    \def \csym@cspParallel    {\mathop{\mathstrut \csym@cspParallelbase}\nolimits}

    \DeclareMathSymbol{\csym@cspextchoice}{\mathbin}{stmry}{"40}%
    \def \csym@cspExtchoice  {\indexed@op{\csym@cspextchoice}}
    %\DeclareMathSymbol{\csym@cspExtchoice}{\mathbin}{stmry}{"65}%

    \let \csym@cspintchoice  \sqcap
    \def \csym@cspIntchoice  {\indexed@op{\csym@cspintchoice}}
    %\DeclareMathSymbol{\csym@cspIntchoice}{\mathbin}{stmry}{"64}%

    \def \csym@circhide      {\zbig{\zsym@solidus}}
    \def \csym@circseq       {\zbig{;}}
    \def \csym@circmu        {\zbig{\zsym@mu}}
    \def \csym@circthen      {\zbig{\longrightarrow}}
    \DeclareMathSymbol{\csym@circelse}{\mathbin}{stmry}{"38}% %\def \csym@circelse {[\!]}
    \DeclareMathSymbol{\csym@circguard}{\mathbin}{stmry}{"4E}% \let \csym@circguard \&

  %%%%%%%%%%%%%%%%% 4) Special CSP symbols                        %

    \DeclareMathSymbol{\csym@tick}{\mathord}{AMSa}{"58}%

  %%%%%%%%%%%%%%%%% 5) Circus prelude symbols                     %

    \def \csym@boolean       {\mathbb B}
    \def \csym@universe      {\mathbb U}

  %%%%%%%%%%%%%%%%% 6) Circus model checking toolkit symbols      %

    \DeclareMathSymbol{\cmcsym@gendj}{\mathbin}{AMSa}{"47}%
    \let \cmcsym@regions   \otimes
    \let \cmcsym@dsetminus \searrow
    \DeclareMathSymbol{\cmcsym@dcap}{\mathbin}{AMSa}{"06}% \lozenge

  %%%%%%%%%%%%%%%%% 7) Special symbols used for Z bags            %

    % added symbols for bags within Circus.sty
    \def \zsym@lbag    {{[}\mkern-2mu{[}~}%{[\![~}
    \def \zsym@rbag    {{]}\mkern-2mu{]}~}%{]\!]~}
    \def \zsym@inbag   {\mbox{\texttt{E}}}                 % ??? find something better ???
    \def \zsym@uminus{\setbox0=\hbox{$\cup$}\rlap{\hbox
                        to\wd0{\hss\raise0.3ex\hbox{$\scriptscriptstyle{-}$}\hss}}\box0}
    \let \zsym@otimes   \otimes
    \let \zsym@uplus    \uplus
    \let \zsym@bcount   \sharp
    \let \zsym@subbageq \sqsubseteq
}

% sets the math version
% keep the math version as CZT
%\mathversion{circus}%
%\PackageInfo{circus}{Current math version set to `circus'}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Circus registers: skip, dimen, tab, etc                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

%%%%%%%%%% new registers                                        %

% Low-level TeX register used to define what to count
% 0 = channels     (i.e., \circchannel, \circchannelfrom)
% 1 = channel sets (i.e., \circchanset)
% 2 = processes
% 3 = process ref.
% 4 = start action counting
% 5 = name sets
% 6 = actions
% 7 = action ref.
% 8 = end action counting
% 99= nothing
\newcount\@circuscountingwhat
\@circuscountingwhat=99

% Flag used to switch tools-only commands typesetting on/off
\newif\ifTypesetCircusToolsCmds

% Few counters used to calculate number of definitions.
% Reset is controlled by flag/option, default is "cntglobally".
% Stared versions of environments, which are not parsed, are not counted.
% We do not care about parsing rules here (i.e., incorrect specs
% are going to be counted incorrectly). We have local and global counters.
% Global counters accumulate decls from the whole documents.
%
% Global paragraphs    | Keywords used for counting
%  Z paragraphs        |  see czt.sty counters
%  Channels            |  \circchannel, \circchannelfrom
%  Channel sets        |  \circchannelset
%  Process             |  \circprocess
%  Process refinement  |  \circassertref
%
% Local paragraphs     | Keywords used for counting
%  Z paragraphs        |  see czt.sty counters
%  Action para         |  \circdef after passed \circbegin
%  Action refinement   |  \circassertref after passed \circbegin
%  Name sets           |  \circnameset
%
% Global counters:
%  a) number of channel declarations (not channels declared - may have more than one per \circchannel!)
%  b) number of channel set declarations (the number declared - only one per \circchannelset!)
%  c) number of processes
%  d) number of process assertions
%
%  e) total number of declarations per (basic) process (total within each basic process)
%  f) total number of global declarations (don't consider local numbers within basic processes)
%  g) total number of all declarations (all declarations including within basic processes)
\newcounter{cntCircusChannel}
\newcounter{cntCircusChannelset}
\newcounter{cntCircusProcess}
\newcounter{cntCircusProcessRef}
\newcounter{cntCircusNameset}[cntCircusProcess]
\newcounter{cntCircusAction}[cntCircusProcess]
\newcounter{cntCircusActionRef}[cntCircusProcess]
\newcounter{cntCircusDeclShallow}[cntCircusProcess]
\newcounter{cntCircusDeclDeep}

\newcounter{cntCircusZunboxed}[cntCircusProcess]
\newcounter{cntCircusZaxdef}[cntCircusProcess]
\newcounter{cntCircusZgendef}[cntCircusProcess]
\newcounter{cntCircusZschema}[cntCircusProcess]
\newcounter{cntCircusZgenschema}[cntCircusProcess]

\newcounter{cntCircustotChannel}
\newcounter{cntCircustotChannelset}
\newcounter{cntCircustotProcess}
\newcounter{cntCircustotProcessRef}
\newcounter{cntCircustotNameset}
\newcounter{cntCircustotAction}
\newcounter{cntCircustotActionRef}
\newcounter{cntCircustotDeclShallow}
\newcounter{cntCircustotDeclDeep}

\newcounter{cntCircusZtotunboxed}
\newcounter{cntCircusZtotaxdef}
\newcounter{cntCircusZtotgendef}
\newcounter{cntCircusZtotschema}
\newcounter{cntCircusZtotgenschema}

% update the reseting rationale based on package options.
% maybe put this code at the \DeclareOption part (?)
%\if@cntbychapter@
%  \@addtoreset{cntCircusChannel}{chapter}
%  \@addtoreset{cntCircusChannelset}{chapter}
%  \@addtoreset{cntCircusProcess}{chapter}
%  \@addtoreset{cntCircusProcessRef}{chapter}
%  \@addtoreset{cntCircusDeclDeep}{chapter}
%
%%  \@addtoreset{cntCircusNameset}{chapter}
%%  \@addtoreset{cntCircusAction}{chapter}
%%  \@addtoreset{cntCircusActionRef}{chapter}
%%  \@addtoreset{cntCircusDeclShallow}{chapter}
%
%
%%  \renewcommand{\thecntCircusChannel}{\arabic{cntCircus} unboxed \ifnum \arabic{cntZaxdef} = 1 item \else items\fi in Chapter~\thechapter}
%%  \renewcommand{\thecntCircusChannelset}{\arabic{cntZaxdef} axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Chapter~\thechapter}
%%  \renewcommand{\thecntCircusProcess}{\arabic{cntZgendef} generic axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Chapter~\thechapter}
%%  \renewcommand{\thecntCircusProcessRef}{\arabic{cntZschema} \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Chapter~\thechapter}
%%  \renewcommand{\thecntCircusNameset}{\arabic{cntZgenschema} generic \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Chapter~\thechapter}
%%  \renewcommand{\the}{\arabic{cntZdecl} in Chapter~\thechapter}
%\else
%  \if@cntbysection@
%     \@addtoreset{cntCircusChannel}{chapter}
%     \@addtoreset{cntCircusChannelset}{chapter}
%     \@addtoreset{cntCircusProcess}{chapter}
%     \@addtoreset{cntCircusProcessRef}{chapter}
%     \@addtoreset{cntCircusDeclDeep}{chapter}
%
%%     \@addtoreset{cntCircusNameset}{chapter}
%%     \@addtoreset{cntCircusAction}{chapter}
%%     \@addtoreset{cntCircusActionRef}{chapter}
%%     \@addtoreset{cntCircusDeclShallow}{chapter}
%
%%    % this is not a very helpful command. TODO: CHANGE PLEASE
%%    \renewcommand{\thecntZunboxed}{\arabic{cntZunboxed} unboxed \ifnum \arabic{cntZaxdef} = 1 item \else items\fi in Section~\thesection}
%%    \renewcommand{\thecntZaxdef}{\arabic{cntZaxdef} axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Section~\thesection}
%%    \renewcommand{\thecntZgendef}{\arabic{cntZgendef} generic axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Section~\thesection}
%%    \renewcommand{\thecntZschema}{\arabic{cntZschema} \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Section~\thesection}
%%    \renewcommand{\thecntZgenschema}{\arabic{cntZgenschema} generic \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Section~\thesection}
%%    \renewcommand{\thecntZdecl}{\arabic{cntZdecl} in Section~\thesection}
%  \fi
%  %\else \if@cntglobally@ \relax \fi
%\fi

%%%%%%%%%% registers initialisation                             %

\TypesetCircusToolsCmdsfalse

\PackageInfo{circus}{%
    Initialising Circus registers with default values.\MessageBreak
    \space\space\space\protect\TypesetCircusToolsCmds=\ifTypesetCircusToolsCmds true \else false \fi%
}

\let\@@countZGlobal=\@countZGlobal
\def\@countZGlobal {%
    \@@countZGlobal
    \@countCircusGlobal%
}
\let\@@countZPara=\@countZPara
\def\@countZPara {%
    \ifCountDefs
       \ifnum \@circuscountingwhat < 4      % x < 4
          % count Z global, updating circus global counters
          \@@countZPara
       \else
          \ifnum \@circuscountingwhat < 8   % 4 <= x < 8
            % count Z para
            \@countCircusZPara
          \else                             % x >= 8
            % do the default Z counting (?) or just \relax?
            \@@countZPara
          \fi
       \fi
    \else
       \relax
    \fi
}

\def\@countCircusZPara{%
   \ifCountDefs
       \ifnum \@zcountingwhat = 0
          %unboxed para code...
          \stepcounter{cntCircusZunboxed}
          \stepcounter{cntCircusZtotunboxed}
          \@countCircusGlobal
       \else
          \ifnum \@zcountingwhat = 1
             %axdef code...
             \stepcounter{cntCircusZaxdef}
             \stepcounter{cntCircusZtotaxdef}
             \@countCircusGlobal
          \else
             \ifnum \@zcountingwhat = 2
                %gendef code...
                \stepcounter{cntCircusZgendef}
                \stepcounter{cntCircusZtotgendef}
                \@countCircusGlobal
             \else
                \ifnum \@zcountingwhat = 3
                   %schemas code...
                   \stepcounter{cntCircusZschema}
                   \stepcounter{cntCircusZtotschema}
                   \@countCircusGlobal
                \else
                   \ifnum \@zcountingwhat = 4
                      %gen schemas code...
                      \stepcounter{cntCircusZgenschema}
                      \stepcounter{cntCircusZtotgenschema}
                      \@countCircusGlobal
                   \else
                      %don't count at all
                      \relax
                   \fi
                \fi
             \fi
          \fi
       \fi
   \else
      \relax
   \fi
}

\def\@countCircusGlobal{%
      \stepcounter{cntCircusDeclShallow}
      \stepcounter{cntCircustotDeclShallow}
      \stepcounter{cntCircusDeclDeep}
      \stepcounter{cntCircustotDeclDeep}}
\def\@countCircusPara{%
   \ifCountDefs
       \ifnum \@circuscountingwhat = 0
          %channel and channel from para code...
          \stepcounter{cntCircusChannel}
          \stepcounter{cntCircustotChannel}
          \@countCircusGlobal
       \else
          \ifnum \@circuscountingwhat = 1
              %channel set code...
              \stepcounter{cntCircusChannelset}
              \stepcounter{cntCircustotChannelset}
              \@countCircusGlobal
          \else
             \ifnum \@circuscountingwhat = 2
                %process code...
                \stepcounter{cntCircusProcess}
                \stepcounter{cntCircustotProcess}
                \@countCircusGlobal
             \else
                \ifnum \@circuscountingwhat = 3
                   %process refinement code...
                   \stepcounter{cntCircusProcessRef}
                   \stepcounter{cntCircustotProcessRef}
                   \@countCircusGlobal
                \else
                   \ifnum \@circuscountingwhat = 4
                      %inner basic process counting code...
                      %we need to redefine the way \@countZPara works
                      \relax % TODO!
                   \else
                       % if within \circbegin (4) .. \circend (8)
                       \ifnum \@circuscountingwhat > 4
                          \ifnum \@circuscountingwhat < 8
                             % inner basic process counting code...
                             \ifnum \@circuscountingwhat = 5
                                %name set code...
                                \stepcounter{cntCircusNameset}
                                \stepcounter{cntCircustotNameset}
                                \@countCircusGlobal
                             \else
                                \ifnum \@circuscountingwhat = 6
                                   %action code...
                                   \stepcounter{cntCircusAction}
                                   \stepcounter{cntCircustotAction}
                                   \@countCircusGlobal
                                \else
                                   \ifnum \@circuscountingwhat = 7
                                      %action code...
                                      \stepcounter{cntCircusActionRef}
                                      \stepcounter{cntCircustotActionRef}
                                      \@countCircusGlobal
                                   \else
                                      % don't count, e.g., \@circuscountingwhat=99
                                      \relax
                                   \fi
                                \fi
                             \fi
                          \else
                             % don't count, reached \circend, \@circuscountingwhat=8
                             \relax
                          \fi
                       \else
                          %don't count, e.g., \@circuscountingwhat=99
                          \relax
                       \fi
                   \fi
                \fi
             \fi
          \fi
       \fi
   \else
      \relax
   \fi
}

% NOTE: maybe using the "ifthen.sty" package would be a good idea here?
\def\@circusPossibleInnerParaCount#1#2{%
      \ifCountDefs
         % if not knowing where we are counting from
         \ifnum \@circuscountingwhat = 99
            % we are at process refinement level
            \@circuscountingwhat=#1
         \else
            % if we know and we are not within a basic process
            \ifnum \@circuscountingwhat < 4
               % we are at process refinement level
               \@circuscountingwhat=#1
            \else
               % we are within basic process before \circend
               \ifnum \@circuscountingwhat < 8
                   \@circuscountingwhat=#2
               \fi
            \fi
         \fi
         % actually count the paragraph
         \@countCircusPara
      \fi}

\def \CircusDeclSummary {%
   %\ZDeclSummary
   \ifCountDefs
      \begin{table}[ht]
        \begin{center}
            \if@cntglobally@
                \begin{tabular}{|l|l|r|}
                    \hline
                    \textbf{Category} & \textbf{Declarations}   & \textbf{Total} \\
                    \hline
                                      & Unboxed items           & \arabic{cntZtotunboxed} \\
                    & \multicolumn{2}{c}{\hline} \\
                                      & Axiomatic defs          & \arabic{cntZtotaxdef} \\
                    \hline
                    Top-level         & Generic axiomatic defs. & \arabic{cntZtotgendef} \\
                    \hline
                    Z decls           & Schemas                 & \arabic{cntZtotschema} \\
                    \hline
                                      & Generic schemas         & \arabic{cntZtotgenschema} \\
                    \hline
                                      & \textbf{Total}          & \textbf{\arabic{cntZtotdecl}} \\
                    \hline
                    \hline
                                      & Channel decls.          & \arabic{cntCircustotChannel} \\
                    \hline
                    Top-level         & Channel set decls.      & \arabic{cntCircustotChannelset} \\
                    \hline
                    \Circus{} decs    & Process decls.          & \arabic{cntCircustotProcess} \\
                    \hline
                                      & Process ref. assertions & \arabic{cntCircustotProcessRef} \\
                    \hline
                                      & \textbf{Total}          & \textbf{\arabic{cntCircustotDeclShallow}} \\
                    \hline
                    \hline
                    Overall           & \textbf{Total}          &  \\% \textbf{\arabic{cntZtotdecl}\plus\arabic{cntCircustotDeclShallow}} \\
                    \hline
                \end{tabular}
            \else
                \def \@circuscntpart {%
                    \if@cntbychapter@ Chapter \else \if@cntbysection@ Section \else ??? \fi \fi}
                \begin{tabular}{|l|c|c|}
                    \hline
                    \textbf{Declarations}   & \textbf{This \@circuscntpart}       & \textbf{Globally} \\
                    \hline
                    Unboxed items           & \arabic{cntZunboxed}           & \arabic{cntZtotunboxed} \\
                    \hline
                    Axiomatic definitions   & \arabic{cntZaxdef}             & \arabic{cntZtotaxdef} \\
                    \hline
                    Generic axiomatic defs. & \arabic{cntZgendef}            & \arabic{cntZtotgendef} \\
                    \hline
                    Schemas                 & \arabic{cntZschema}            & \arabic{cntZtotschema} \\
                    \hline
                    Generic schemas         & \arabic{cntZgenschema}         & \arabic{cntZtotgenschema} \\
                    \hline
                    \textbf{Total}          & \textbf{\arabic{cntZdecl}} & \textbf{\arabic{cntZtotdecl}} \\
                    \hline
                \end{tabular}
            \fi
        \end{center}
        \if@cntglobally@
           \caption{Summary of all \Circus{} declarations.}\label{tbl:circusdecl:global}
        \else
          \if@cntbychapter@
             \caption{Summary of \Circus{} declarations for Chapter~\thechapter.}\label{tbl:circusdecl:\thechapter}
          \else
            \if@cntbysection@
               \caption{Summary of \Circus{} declarations for Section~\thesection.}\label{tbl:circusdecl:\thesection}
            \fi
          \fi
        \fi
      \end{table}
   \else
      \relax
   \fi
}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Circus environments                                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\@circus#1{%
    \@circuscountingwhat=#1
    \zed}
\def\circus{\@circus{0}}       % make it as global (top level)
\let\endcircus=\endzed

\def\circusaction{\@circus{4}} % make it as local (\circbegin)
\let\endcircusaction=\endzed

\PackageInfo{circus}{Setting up Circus LaTeX environments}

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Language keywords                                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Just like in Z, but with \textsl and underline instead of \texrm.
% This (i.e., being different from Z keywords) is useful because
% some names are reused (e.g., if)
%
\def\mathsl#1{\hbox{\slshape #1}}
\def\circusword#1{\z@word{\mathsl{#1}}}
\def\circuskeyword#1{\z@word{\mathsl{\textbf{#1}}}}
\def\circustoolkit#1{\if@ctkkeyword@ \circuskeyword{#1} \else \circusword{#1} \fi}

%%%%%%%%%%%%%%%%% 1) Guarded commands                           %

\def \circif      {\zpreop{\circuskeyword{if}}}
\def \circfi      {\zpostop{\circuskeyword{fi}}}
\def \circdo      {\zpreop{\circuskeyword{do}}}
\def \circod      {\zpostop{\circuskeyword{od}}}
\def \circcon     {\zpreop{\circuskeyword{con}}}
\def \circvar     {\zpreop{\circuskeyword{var}}}
\def \circval     {\zpreop{\circuskeyword{val}}}
\def \circres     {\zpreop{\circuskeyword{res}}}
\def \circvres    {\zpreop{\circuskeyword{vres}}}

%%%%%%%%%%%%%%%%% 2) Channel and name set                       %

\def \circchannel     {\zpreop{\circuskeyword{channel}}\@circuscountingwhat=0 \@countCircusPara}
\def \circchannelfrom {\zpreop{\circuskeyword{channelfrom}}\@circuscountingwhat=0 \@countCircusPara}
\def \circchannelset  {\zpreop{\circuskeyword{channelset}}\@circuscountingwhat=1 \@countCircusPara}
\def \circnameset     {\zpreop{\circuskeyword{nameset}}\@circuscountingwhat=15 \@countCircusPara}

%%%%%%%%%%%%%%%%% 3) Processes                                  %

\def \circprocess {\zpreop{\circuskeyword{process}}\@zcountingwhat=3 \@countCircusPara}
\def \circbegin   {\zpreop{\circuskeyword{begin}}\@zcountingwhat=4}
\def \circend     {\zpreop{\circuskeyword{end}}}
\def \circstate   {\zpreop{\circuskeyword{state}}}

%%%%%%%%%%%%%%%%% 4) Actions                                    %

\def \Skip        {\zordop{\circuskeyword{Skip}}}
\def \Stop        {\zordop{\circuskeyword{Stop}}}
\def \Chaos       {\zordop{\circuskeyword{Chaos}}}

\PackageInfo{circus}{Loading Circus keywords}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Core symbols                                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%% 1) BRACKETS - brackets used in Circus         %

\def \lchanset      {\zopenop{\csym@lchanset}}
\def \rchanset      {\zcloseop{\csym@rchanset}}
\def \lcircindex    {\zopenop{\csym@lcircindex}}
\def \rcircindex    {\zcloseop{\csym@rcircindex}}
\def \lcircguard    {\zopenop{\csym@lcircguard}}
\def \rcircguard    {\zcloseop{\csym@rcircguard}}
\def \lschexpract   {\zopenop{\csym@lschexpract}}
\def \rschexpract   {\zcloseop{\csym@rschexpract}}
\def \linter        {\zbinop{\zopenop{\csym@linter}}}
\def \rinter        {\zbinop{\zcloseop{\csym@rinter}}}
\def \lpar          {\zbinop{\zopenop{\csym@lpar}}}
\def \rpar          {\zbinop{\zcloseop{\csym@rpar}}}
\def \lcircrename   {\zopenop{\csym@lcircrename}}
\def \rcircrename   {\zcloseop{\csym@rcircrename}}

\PackageInfo{circus}{Loading Circus brackets}

%%%%%%%%%%%%%%%%% 2) Special symbols used in Circus             %

\def \circrefines   {\zrelop{\csym@circrefines}}
\def \circsimulates {\zrelop{\csym@circsimulates}}
\def \circspot      {\zrelop{\csym@circspot}}
\def \circindex     {\zrelop{\csym@circindex}}

% count paragraphs: 3=process ref, 7=action ref; 2=process, 6=action
\def \circdef       {\zrelop{\csym@circdef}\@circusPossibleInnerParaCount{3}{7}}
\def \circassertref {\zrelop{\csym@circassertref}\@circusPossibleInnerParaCount{2}{6}}

\PackageInfo{circus}{Loading Circus special symbols}

%%%%%%%%%%%%%%%%% 3) CSP symbols used in Circus                 %

\def \then          {\zbinop{\csym@cspthen}}
\def \prefixcolon   {\zbinop{\csym@prefixcolon}}
\def \Semi          {\zpreop{\csym@cspSemi}}
\def \interleave    {\zbinop{\csym@cspinterleave}}
\def \Parallel      {\zpreop{\csym@cspParallel}}
\def \Interleave    {\zpreop{\csym@cspInterleave}}
\def \extchoice     {\zbinop{\csym@cspextchoice}}
\def \Extchoice     {\zpreop{\csym@cspExtchoice}}
\def \intchoice     {\zbinop{\csym@cspintchoice}}
\def \Intchoice     {\zpreop{\csym@cspIntchoice}}
\def \circhide      {\zbinop{\csym@circhide}}
\def \circseq       {\zbinop{\csym@circseq}}
\def \circmu        {\zbinop{\csym@circmu}}
\def \circthen      {\zbinop{\csym@circthen}}
\def \circelse      {\zbinop{\csym@circelse}}
\def \circguard     {\zbinop{\csym@circguard}}

\PackageInfo{circus}{Loading Circus CSP symbols}

%%%%%%%%%%%%%%%%% 4) Circus boxing characters                   %

%    <BOXCHAR>
%      <char id="CIRCUSCHAR" hex="257A" description="box drawings thick horizontal line to the right."/>
%      <char id="CIRCUSACTIONCHAR" hex="2576" description="box drawings thin horizontal line to the right."/>
%    </BOXCHAR>

%  <SPECIAL>
%    <BOXCHAR>
%      <char id="CIRCUSJOKERCHAR" hex="2606" description="hollow version of JOKER char."/>
%      <char id="CIRCUSACTIONLAWCHAR" hex="25A1" description="hollow version of Rule char."/>
%      <char id="CIRCUSPROCESSLAWCHAR" hex="25A3" description="hollow contained version of Rule char."/>
%    </BOXCHAR>
%  </SPECIAL>

\PackageInfo{circus}{Loading Circus boxing symbols}

%%%%%%%%%%%%%%%%% 5) Circus prelude symbols                     %

\def \boolean  {\zordop{\csym@boolean}}
\def \universe {\zordop{\csym@universe}}

\renewcommand{\true}{\zordop{\circuskeyword{True}}}
\renewcommand{\false}{\zordop{\circuskeyword{False}}}

\PackageInfo{circus}{Loading Circus circus\_prelude symbols}

%%%%%%%%%%%%%%%%% 6) Circus model checking toolkit symbols      %

\def \gendj     {\zbinop{\cmcsym@gendj}}
\def \regions   {\zbinop{\cmcsym@regions}}
\def \dsetminus {\zbinop{\cmcsym@dsetminus}}
\def \dcap      {\zbinop{\cmcsym@dcap}}
\def \minimal   {\zordop{\circustoolkit{minimal}}}

\PackageInfo{circus}{Loading Circus circus\_mc\_toolkit symbols}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Few extra helpful commands                                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% users referring to this file in their \LaTeX
\def \circusstylefile {\texttt{circus.sty}}

\def \Circus {{\sf\slshape Circus}}

\def \tick   {\zordop{\csym@tick}}

% Special Circus tool controlling commands
\newcommand{\circblockbegin}{\begin{zedblock}}
\newcommand{\circblockend}{\end{zedblock}}
\newcommand{\circtoolson}{\ifTypesetCircusToolsCmds \hbox{[\textsl{\textbf{Circus tools on}}]} \else \relax \fi}
\newcommand{\circtoolsoff}{\ifTypesetCircusToolsCmds \hbox{[\textsl{\textbf{Circus tools off}}]} \else \relax \fi}

\newlength{\circnotewidth}
\setlength{\circnotewidth}{.75\linewidth}
%\newlength{\circnoteindent}
%\circnoteindent=\zedtab or dimen?
%\setlength{\circnoteindent}{2em}
\newcommand{\circnote}[1]{\ifTypesetCircusToolsCmds \ensuremath{\t1}\parbox{\circnotewidth}{\small \textsf{#1}}\ensuremath{\\} \else \relax \fi}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Extra symbols for Bags                                        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

\def \bag     {\zpreop{\ztoolkit{bag}}}              % G
\def \bcount  {\zbinop{\zsym@bcount}}                % F
\def \otimes  {\zbinop{\zsym@otimes}}                % F
\def \uplus   {\zbinop{\zsym@uplus}}                 % F
\def \uminus  {\zbinop{\zsym@uminus}}                % F
\def \subbageq{\zrelop{\zSmall{\zsym@subbageq}}}     % R  % \subbageq smaller to avoid confusion with \circrefines, which has the same symbol
\def \inbag   {\zrelop{\zsym@inbag}}                 % R
\def \lbag    {\zopenop{\zsym@lbag}}
\def \rbag    {\zcloseop{~\zsym@rbag}}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Extra environments from zed.sty                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% NOT PARSEABLE - pointless.
% Same as zed environment, yet allows column alignment
%\def\syntax{\@zed\@znoskip \halign\bgroup
%  \strut$\@zlign##$\hfil &\hfil$\@zlign{}##{}$\hfil
%  &$\@zlign##$\hfil\cr}
%\let\endsyntax=\endzed

% Environment to display informal proof steps / arguments,
% but it considers the alignment as in zed-csp, and colours
% as in encoded here (which renders the same as there, but
% slightly differently coded).
\def\@argue{\ifvmode\@zleavevmode\fi
  $$\global\zt@ptrue
  \@setzsize
  \advance\linewidth by-\zedindent
  \advance\displayindent by\zedindent
  \def\\{\crcr}% Must have \def and not \let for nested alignments.
  \let\par=\relax
  \tabskip=0pt}
\def\argue{\@argue \interzedlinepenalty=\interdisplaylinepenalty
  \openup\@jot \halign to\linewidth\bgroup
  {\strut$\color{ZedColor}\@zlign##$}\hfil \tabskip=0pt plus1fil
  &\hbox to0pt{\hss[\@zlign##\unskip]}\tabskip=0pt\cr
  \noalign{\vskip-\@jot}}
\let\endargue=\endzed

% Environment to display natural deduction inference rules
\def\infrule{\@zed\@znoskip \halign\bgroup
  \strut\quad$\@zlign##$\quad\hfil&\quad\@zlign##\hfil\cr}
\let\endinfrule=\endzed

\def\derive{\crcr \noalign{\vskip\@jot} \omit\@zrulefill
  \@ifnextchar[{\@xderive}{\@yderive}}
\def\@xderive[#1]{&$\smash{\lower 0.5ex\hbox{$[\;#1\;]$}}$\cr
  \noalign{\vskip\@jot}}
\def\@yderive{\cr \noalign{\vskip\@jot}}

\endinput
%%
%% End of file `circus.sty'.
%
%% Some useful symbols for the UTP:

%\def\II{\hbox{\texttt{\slshape I \kern -7.5pt I}}}
%\def\circledR{{\mathhexbox\msafam@72 }}
