%-------------------------------------------------------------------
% 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 file is required for all latex files generated by the
% B2Latex plugin 0.5.x.
% Each command mentioned below, can be modified for your own style
% but command names are not allowed.
%
%-------------------------------------------------------------------
% Defined colors.
%-------------------------------------------------------------------
\usepackage{color}
\definecolor{keycolor}{rgb}{0,0,0.7}  %color of key words, blue is the default
\definecolor{labelcolor}{rgb}{0,0.4,0.8}  %color of labels, cyan
\definecolor{codecolor}{rgb}{0,0,0}  %color of formulas, black
\definecolor{ccodecolor}{rgb}{0,0.2,0}  %color of inherited formulas, green
\definecolor{cmtcolor}{rgb}{0,0,0}  %color of comments, black
\definecolor{xcolor}{rgb}{1,0,0}  %x

%-------------------------------------------------------------------
\newcommand{\paraSpc} {\hspace*{\fill} \setlength{\parskip}{-2pt}} % reduce space between paras
%-------------------------------------------------------------------
\newcommand{\itemSpc} {\setlength{\itemsep}{-0pt}} % reduce space between para items
%-------------------------------------------------------------------
% Special commands for MACHINE 
%-------------------------------------------------------------------
\newcommand{\MACHINE}[1] { \item[\textcolor{keycolor}{MACHINE }] #1 \paraSpc }

\newcommand{\REFINES}[1]{ \item[\textcolor{keycolor}{REFINES }] #1 \paraSpc }

\newcommand{\SEES}[1]{ \item[\textcolor{keycolor}{SEES }] #1 \paraSpc }

\newcommand{\VARIABLES}{\item[\textcolor{keycolor}{VARIABLES}] \paraSpc }

\newcommand{\INVARIANTS}{  \item[\textcolor{keycolor}{INVARIANTS}] \paraSpc }

\newcommand{\VARIANT}{ \item[\textcolor{keycolor}{VARIANT}] \paraSpc }

\newcommand{\EVENTS}{  \item[\textcolor{keycolor}{EVENTS}] \paraSpc }

\newcommand{\INITIALISATION}{  \item[\textcolor{keycolor}{Initialisation}] \paraSpc }

\newcommand{\EVT}[1]{  \item[\textcolor{keycolor}{Event }] \textit{#1} $\defi$ \paraSpc } % opt1
% Option: deactivate above command and reactivate 
% the command below to display only event name
%\newcommand{\EVT}[1]{  \item[\textit{#1}] $\defi$ \paraSpc } % opt2

\newcommand{\REF}[1]{ \item[\textcolor{keycolor}{refines}] \textit{#1} \paraSpc }

\newcommand{\EXTD}[1]{ \item[\textcolor{keycolor}{extends}] \textit{#1} \paraSpc }

\newcommand{\Status}[1]{ \item[\textcolor{keycolor}{Status}] #1 \paraSpc }

\newcommand{\AnyPrm}{ \item[\textcolor{keycolor}{any}] \paraSpc \itemSpc }

\newcommand{\WhereGrd}{ \item[\textcolor{keycolor}{where}] \paraSpc \itemSpc }

\newcommand{\WhenGrd}{ \item[\textcolor{keycolor}{when}] \paraSpc \itemSpc }

\newcommand{\Witnesses}{ \item[\textcolor{keycolor}{with}] \paraSpc \itemSpc }

\newcommand{\ThenAct}{ \item[\textcolor{keycolor}{then}] \paraSpc \itemSpc }

\newcommand{\BeginAct}{ \item[\textcolor{keycolor}{begin}] \paraSpc \itemSpc }

\newcommand{\EndAct}{ \item[\textcolor{keycolor}{end}] \paraSpc }

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

\newcommand{\CONTEXT}[1]{  \item[\textcolor{keycolor}{CONTEXT }] #1 \paraSpc }

\newcommand{\EXTENDS}[1]{ \item[\textcolor{keycolor}{EXTENDS }] #1 \paraSpc }

\newcommand{\SETS}{ \item[\textcolor{keycolor}{SETS}] \paraSpc }

\newcommand{\CONSTANTS}{ \item[\textcolor{keycolor}{CONSTANTS}] \paraSpc }

\newcommand{\THEOREMS}{ \item[\textcolor{keycolor}{THEOREMS}] \paraSpc }

\newcommand{\AXIOMS}{ \item[\textcolor{keycolor}{AXIOMS}] \paraSpc }

%-------------------------------------------------------------------
% General commands used in both machines and contexts
%-------------------------------------------------------------------

\newcommand{\converse}{^{-1}} %converse
\newcommand{\hsp}[1]{\hspace*{#1 cm}}

% Specification Title
\newcommand{\BTitle}[3]{
\item[\fbox{\parbox{6in}{\centering{~\\An Event-B Specification of #1
\\Creation Date: #2 @ #3\\}}}]
}
% End of MACHINE or CONTEXT
\newcommand{\END}{ \item[\textcolor{keycolor}{END}] \hspace*{\fill} }

% Printing non-labelled elements
% (i.e. variables, sets and constants)

%concrete non-labelled elements
\newcommand{\Item}[1]{\item \parbox[t]{\textwidth}{{\color{codecolor}{$#1$}}}\itemSpc}

%inherited non-labelled elements
\newcommand{\ItemX}[1]{\item \parbox[t]{\textwidth}{{\color{ccodecolor}{$#1$}}}\itemSpc}

%concrete commented non-labelled elements
\newcommand{\ItemY}[2]{\item \parbox[t]{\textwidth}{{\color{codecolor}{$#1$}}~~~{\color{cmtcolor}{#2}}}\itemSpc}

%inherited commented non-labelled elements
\newcommand{\ItemXY}[2]{\item \parbox[t]{\textwidth}{{\color{ccodecolor}{$#1$}}~~~{\color{cmtcolor}{#2}}}\itemSpc}

% Printing an element with label name
% (i.e. invariants, theorems, axioms, witnesses and actions)
% parameter #1 is a label name and #2 is its content
%concrete labelled elements
\newcommand{\nItem}[2]{ \item \parbox[t]{\textwidth}{{\color{labelcolor}{\small{\texttt{#1}}}}:~{\color{codecolor}{$#2$}}} \itemSpc} % opt1\itemSpc
% inherited labelled elements
\newcommand{\nItemX}[2]{ \item \parbox[t]{\textwidth}{{\color{labelcolor}{\small{\texttt{#1}}}}:~{\color{ccodecolor}{$#2$}}} \itemSpc} % opt1

%concrete commented labelled element
\newcommand{\nItemY}[3]{ \item \parbox[t]{\textwidth}{{\color{labelcolor}{\small{\texttt{#1}}}}:~{\color{codecolor}{$#2$}}~~~{\color{cmtcolor}{#3}}} \itemSpc} % opt1
%inherited commented labelled element
\newcommand{\nItemXY}[3]{ \item \parbox[t]{\textwidth}{{\color{labelcolor}{\small{\texttt{#1}}}}:~{\color{ccodecolor}{$#2$}}~~~{\color{cmtcolor}{#3}}} \itemSpc} % opt1

% Below is an alternative command for printing with no label
%\newcommand{\nItem}[2]{ \item[] $#2$} % opt2

% Commentations, reselect the second option for displaying asterisks
% - Newline comment 
\newcommand{\cmt}[1]{ \textcolor{cmtcolor}{ #1}\itemSpc} %opt1 
%\newcommand{\cmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt2

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