%-------------------------------------------------------------------
% 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
% Each command mentioned below, can be modified for your own style
% but command names are not allowed.
%
%-------------------------------------------------------------------
% Special commands for MACHINE 
%-------------------------------------------------------------------
\newcommand{\MACHINE}[1] { \item[MACHINE ] #1 \hspace*{\fill}}

\newcommand{\REFINES}[1]{ \item[REFINES] #1 \hspace*{\fill} }

\newcommand{\SEES}[1]{ \item[SEES] #1 \hspace*{\fill} }

\newcommand{\VARIABLES}{\item[VARIABLES] \hspace*{\fill}}

\newcommand{\INVARIANTS}{  \item[INVARIANTS] \hspace*{\fill} }

\newcommand{\VARIANT}{ \item[VARIANT] \hspace*{\fill} }

\newcommand{\EVENTS}{  \item[EVENTS] \hspace*{\fill} }

\newcommand{\INITIALISATION}{  \item[Initialisation] \hspace*{\fill} }

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

\newcommand{\REF}[1]{ \item[refines] \textit{#1} \hspace*{\fill} }

\newcommand{\EXTD}[1]{ \item[extends] \textit{#1} \hspace*{\fill} }

\newcommand{\Status}[1]{ \item[Status] #1 \hspace*{\fill} }

\newcommand{\AnyPrm}{ \item[any] \hspace*{\fill} }

\newcommand{\WhereGrd}{ \item[where] \hspace*{\fill} }

\newcommand{\WhenGrd}{ \item[when] \hspace*{\fill} }

\newcommand{\Witnesses}{ \item[with] \hspace*{\fill} }

\newcommand{\ThenAct}{ \item[then] \hspace*{\fill} }

\newcommand{\BeginAct}{ \item[begin] \hspace*{\fill} }

\newcommand{\EndAct}{ \item[end] \hspace*{\fill} }

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

\newcommand{\CONTEXT}[1]{  \item[CONTEXT ] #1 \hspace*{\fill} }

\newcommand{\EXTENDS}[1]{ \item[EXTENDS ] #1 \hspace*{\fill} }

\newcommand{\SETS}{ \item[SETS] \hspace*{\fill} }

\newcommand{\CONSTANTS}{ \item[CONSTANTS] \hspace*{\fill} }

\newcommand{\THEOREMS}{ \item[THEOREMS] \hspace*{\fill} }

\newcommand{\AXIOMS}{ \item[AXIOMS] \hspace*{\fill} }

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

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

% Printing non-labelled elements
% (i.e. variables, sets and constants)
\newcommand{\Item}[1]{ \item[$\textit{#1}$]}

% 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[$\textit{#1}:$] $#2$} % 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}\\ #1} %opt1 
%\newcommand{\cmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt2

% - Back Comment, for variables, sets and constants
\newcommand{\bcmt}[1]{~~~ #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

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