b2latex.sty

%----------------------------------------------------------------------------
% This is b2latex.sty, generated by B2Latex plugin on Rodin
% Author: K. DAMCHOOM, kd06r@ecs.soton.ac.uk
% Copyright(c) 2008 - 2012 University of Southampton and others.
%----------------------------------------------------------------------------
% This style is required for all latex files generated by the
% B2Latex plugin 0.7.x. It can be modified for your own style.
% Internal commands, which are not contained in the generated
% latex document, are marked by the character '@' in the name.
%----------------------------------------------------------------------------

\usepackage[top=2.5cm, bottom=2.0cm, left=2.5cm, right=2.5cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage[ddmmyyyy]{datetime}
\usepackage{fancyhdr,lastpage,color}

\definecolor{keycolor}{rgb}{0,0,0.8}     % Keywords, blue
\definecolor{labelcolor}{rgb}{0,0.4,0.8} % Labels, cyan
\definecolor{codecolor}{rgb}{0,0,0}      % Formulas, black
\definecolor{inhcolor}{rgb}{0.6,0.2,0}   % Inherited formulas, maroon
\definecolor{cmtcolor}{rgb}{0,0.4,0}     % Comments, green

%\renewcommand{\chaptername}{}
%\renewcommand{\thechapter}{}
\renewcommand{\dateseparator}{.}

% Reduce space between paras
\newcommand{\paraSpc@} {\hspace*{\fill} \setlength{\parskip}{-2pt}}
% Reduce space between para items
\newcommand{\itemSpc@} {\setlength{\itemsep}{-0pt}}

% Keywords
\newcommand{\key@}[1]{\textcolor{keycolor}{#1}}
% Labels
\newcommand{\lbl@}[1]{\textcolor{labelcolor}{\small{\texttt{#1}}}}
% Formulas
\newcommand{\code@}[1]{\textcolor{codecolor}{\small{#1}}}
% Inherited formulas
\newcommand{\inh@}[1]{\textcolor{inhcolor}{\small{#1}}}
% Comments
\newcommand{\cmt@}[1]{\textcolor{cmtcolor}{\small{#1}}}
% Modifiers (inline keywords)
\newcommand{\mod@}[1]{\key@{\small{$\langle$#1$\rangle$}}}

% Optional comment
\newcommand{\cmtOpt@}[1]{\ifthenelse{\equal{#1}{}}{}{\cmt@{#1}}}
% Alternate keyword
\newcommand{\keyAlt@}[3]{\ifthenelse{\boolean{#1}}{\key@{#2}}{\key@{#3}}}
% Optional modifier
\newcommand{\modOpt@}[2]{\ifthenelse{\boolean{#1}}{\mod@{#2}}{}}
% Code or inherited code
\newcommand{\codeInh@}[2]{\ifthenelse{\boolean{#1}}{\code@{#2}}{\inh@{\textit{#2}}}}

%----------------------------------------------------------------------------

% Common header definition
\newcommand{\Header@}{
  \lfoot{\today~\currenttime}
  \cfoot{}
  \rfoot{\rm Page \thepage~of \pageref{LastPage}}
  \pagestyle{fancy}
}

% Header used if a single context or machine is exported
% #1: Context / Machine name
\newcommand{\SingleHeader}[1]{
  \Header@{}
  \lhead{}
  \chead{An Event-B Specification of #1}
  \rhead{}
}

% Title page used if a whole project is exported
% #1: Project name
\newcommand{\MultiTitle}[1]{
  \Header@{}
  \lhead{An Event-B Specification of #1}
  \chead{}
  \rhead{}
  \fancypagestyle{plain}{}
  \tableofcontents
}

% Subheader for each component if a whole project is exported
% #1: Component type (CONTEXT / MACHINE); #2: Component name
\newcommand{\MultiHeader}[2]{
  \newpage{}
  \rhead{\texttt{#1} #2}
%  \addcontentsline{toc}{chapter}{\texttt{#1} #2}
}

%----------------------------------------------------------------------------
% Special commands for CONTEXT
%----------------------------------------------------------------------------

% #1: Context name; #2: Extended contexts (optional); #3: Comment (optional)
\newcommand{\CONTEXT}[3]{
  \begin{description}
  \item[\key@{CONTEXT}] #1 \cmtOpt@{#3} \paraSpc@
  \ifthenelse{\equal{#2}{}}{}{
    \item[\key@{EXTENDS}] #2 \paraSpc@
  }
}
% Alternative compact display:
%\newcommand{\CONTEXT}[3]{
%  \begin{description}
%  \item[\key@{CONTEXT}] #1
%  \ifthenelse{\equal{#2}{}}{}{\key@{EXTENDS} #2}
%  \cmtOpt@{#3}
%  \paraSpc@
%}

% #1: Sets definitions
\newcommand{\SETS}[1]{
  \item[\key@{SETS}] \paraSpc@
  \begin{description} #1 \end{description}
}

% #1: Identifier; #2: Comment (optional)
\newcommand{\Set}[2]{
  \item \code@{#1} \cmtOpt@{#2} \itemSpc@
}

% #1: Constants definitions
\newcommand{\CONSTANTS}[1]{
  \item[\key@{CONSTANTS}] \paraSpc@
  \begin{description} #1 \end{description}
}

% #1: Identifier; #2: Comment (optional)
\newcommand{\Constant}[2]{
  \item \code@{#1} \cmtOpt@{#2} \itemSpc@
}

% #1: Axioms definitions
\newcommand{\AXIOMS}[1]{
  \item[\key@{AXIOMS}] \paraSpc@
  \begin{description} #1 \end{description}
}

% #1: Label; #2: true if theorem; #3: Predicate; #4: Comment (optional)
\newcommand{\Axiom}[4]{
  \item \lbl@{#1}: \modOpt@{#2}{theorem} \code@{#3} \cmtOpt@{#4} \itemSpc@
}

%----------------------------------------------------------------------------
% Special commands for MACHINE
%----------------------------------------------------------------------------

% #1: Machine name; #2: Refined machines (optional);
% #3: Seen contexts (optional); #4: Comment (optional)
\newcommand{\MACHINE}[4]{
  \begin{description}
  \item[\key@{MACHINE}] #1 \cmtOpt@{#4} \paraSpc@
  \ifthenelse{\equal{#2}{}}{}{
    \item[\key@{REFINES}] #2 \paraSpc@
  }
  \ifthenelse{\equal{#3}{}}{}{
    \item[\key@{SEES}] #3 \paraSpc@
  }
}

% #1: variables definitions
\newcommand{\VARIABLES}[1]{
  \item[\key@{VARIABLES}] \paraSpc@
  \begin{description} #1 \end{description}
}

% #1: Identifier; #2: Comment (optional)
\newcommand{\Variable}[2]{
  \item \code@{#1} \cmtOpt@{#2} \itemSpc@
}

% #1: Invariants definitions
\newcommand{\INVARIANTS}[1]{
  \item[\key@{INVARIANTS}] \paraSpc@
  \begin{description} #1 \end{description}
}

% #1: Label; #2: true if theorem; #3: Predicate; #4: Comment (optional)
\newcommand{\Invariant}[4]{
  \item \lbl@{#1}: \modOpt@{#2}{theorem} \code@{#3} \cmtOpt@{#4} \itemSpc@
}

% #1: Variants definitions
\newcommand{\VARIANT}[1]{
  \item[\key@{VARIANT}] \paraSpc@
  \begin{description} #1 \end{description}
}

% #1: Expression; #2: Comment (optional)
\newcommand{\Variant}[2]{
  \item \code@{#1} \cmtOpt@{#2} \itemSpc@
}

\newcommand{\EVENTS}{
  \item[\key@{EVENTS}] \paraSpc@
}

% #1: true if extended; #2: Comment (optional); #3: Event content
\newcommand{\INITIALISATION}[3]{
  \item[\key@{Initialisation}] \modOpt@{#1}{extended} \cmtOpt@{#2} \paraSpc@
  \begin{description} #3 \end{description}
}

% #1: Event name; #2: true if extended; #3 convergence;
% #4: Refined events (optional);  #5: Comment (optional); #6: Event content
\newcommand{\EVT}[6]{
  \item[\key@{Event}] #1
% deactivate above line and activate line below to display only event name
% \item[\key@{#1}]
  \mod@{#3} $\defi$ \cmtOpt@{#5} \paraSpc@
  \ifthenelse{\equal{#4}{}}{}{
    \item[\keyAlt@{#2}{extends}{refines}] #4 \paraSpc@
  }
  \begin{description} #6 \end{description}
}

% #1: Parameters definitions
\newcommand{\ANY}[1]{
  \item[\key@{any}] \paraSpc@ \itemSpc@
  \begin{description} #1 \end{description}
}

% #1: Identifier; #2: true if own, false if inherited; #3: Comment (optional)
\newcommand{\Param}[3]{
  \item \codeInh@{#2}{#1} \cmtOpt@{#3} \itemSpc@
}

%1: true if the event has parameters; #2: Guards definitions
\newcommand{\GUARDS}[2]{
  \item[\keyAlt@{#1}{where}{when}] \paraSpc@ \itemSpc@
  \begin{description} #2 \end{description}
}

% #1: Label; #2: true if theorem; #3: Predicate;
% #4: true if own, false if inherited; #5: Comment (optional)
\newcommand{\Guard}[5]{
  \item \lbl@{#1}: \modOpt@{#2}{theorem} \codeInh@{#4}{#3} \cmtOpt@{#5} \itemSpc@
}

% #1: Witnesses definitions
\newcommand{\WITNESSES}[1]{
  \item[\key@{with}] \paraSpc@ \itemSpc@
  \begin{description} #1 \end{description}
}

% #1: Label; #3: Predicate; #3: Comment (optional)
\newcommand{\Witness}[3]{
  \item \lbl@{#1}: \code@{#2} \cmtOpt@{#3} \itemSpc@
}

%1: true if the event has guards; #2: Actions definitions
\newcommand{\ACTIONS}[2]{
  \item[\keyAlt@{#1}{then}{begin}] \paraSpc@ \itemSpc@
  \begin{description} #2 \end{description}
  \item[\key@{end}] \paraSpc@
}

% #1: Label; #2: Predicate; #3: true if own, false if inherited; #4: Comment (optional)
\newcommand{\Action}[4]{
  \item \lbl@{#1}: \codeInh@{#3}{#2} \cmtOpt@{#4} \itemSpc@
}

% Skip action
\newcommand{\Skip}{
  \item \key@{\textit{skip}} \itemSpc@
}

%----------------------------------------------------------------------------
% General commands for both CONTEXT and MACHINE
%----------------------------------------------------------------------------

% End of MACHINE or CONTEXT
\newcommand{\END}{
  \item[\key@{END}] \hspace*{\fill} \end{description}
}

% Missing in bsymb.sty version 1.9
\newcommand{\converse}{^{-1}}

%----------------------------------------------------------------------------