%-------------------------------------------------------------------
% This is b2latex.sty, generated by B2Latex plugin on Rodin
% Author: K. DAMCHOOM, kd06r@ecs.soton.ac.uk
% Copyright(c)2008 ECS @ University of Southampton
%-------------------------------------------------------------------
% 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.2,0}  %color of formulas, black
\definecolor{xcodecolor}{rgb}{0,0,0}  %color of extended formulas, black
\definecolor{cmtcolor}{rgb}{0,0,0}  %color of comments, black
%-------------------------------------------------------------------
\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
%-------------------------------------------------------------------

% 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)
\newcommand{\Item}[1]{ \item[\textcolor{codecolor}{$\tt#1$}] \itemSpc }
\newcommand{\ItemX}[1]{ \item[\textcolor{xcodecolor}{$\it#1$}] \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
\newcommand{\nItem}[2]{ \item[\textcolor{labelcolor}{$\tt #1:$}] \textcolor{codecolor}{$\tt #2$} \itemSpc } % opt1
\newcommand{\nItemX}[2]{ \item[\textcolor{labelcolor}{$\tt #1:$}] \textcolor{xcodecolor}{$\it #2$} \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]{ \hspace*{\fill}\\\textcolor{cmtcolor}{ #1}} %opt1 
%\newcommand{\cmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt2

% - Back Comment, for variables, sets and constants
\newcommand{\bcmt}[1]{~~~ \textcolor{cmtcolor}{#1}} %opt1 
%\newcommand{\bcmt}[1]{~~~ $/\ast$ #1 $\ast/$} %opt2
% Select opt3 or opt4 (including asterisks) if you want to display this kind of comments
% on the newline like the newline comment
%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ #1} %opt3 
%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt4

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