\documentclass[10pt,a4paper]{report}
\usepackage[top=3cm, bottom=2.5cm, left=3cm, right=2.5cm] {geometry}
\usepackage {bsymb,b2latex}
\usepackage{fancyhdr,lastpage,color}
\lhead{\rm An Event-B Specification of WaterLevelSensor\_refinement}
\rhead {\rm Page \thepage~of \pageref{LastPage}}
\lfoot{}\cfoot{}\rfoot{}
\pagestyle{fancy}
%---------------------------------------------------------
\begin{document}
\thispagestyle{empty}
\begin{description}
\BTitle{WaterLevelSensor\_refinement}{16 Apr 2010}{02:42:53 PM}
\MACHINE{WaterLevelSensor\_refinement}
\REFINES{WaterLevelSensor}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ waterLevel }
		\bcmt{ Shared variable, DO NOT REFINE }
		\Item{ MINE }
		\bcmt{ Shared variable, DO NOT REFINE }
	\end{description}
\EVENTS
	\INITIALISATION
		\\\textit{extended}
		\begin{description}
		\BeginAct
			\begin{description}
			\nItem{ act1 }{ MINE :=  \emptyset  }
			\nItem{ act5 }{ waterLevel :=  \emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {high\_to\_medium}
	\cmt{ Internal Event }
	\REF {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = HIGH }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel(m) :=  MEDIUM }
			\end{description}
		\EndAct
		\end{description}
	\EVT {medium\_to\_low}
	\cmt{ Internal Event }
	\REF {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = MEDIUM }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel(m) :=  LOW }
			\end{description}
		\EndAct
		\end{description}
	\EVT {low\_to\_medium}
	\cmt{ Internal Event }
	\REF {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = LOW }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel(m) :=  MEDIUM }
			\end{description}
		\EndAct
		\end{description}
	\EVT {medium\_to\_high}
	\cmt{ Internal Event }
	\REF {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = MEDIUM }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel(m) :=  HIGH }
			\end{description}
		\EndAct
		\end{description}
	\EVT {addMine}
	\cmt{ External event, DO NOT REFINE }
	\EXTD {addMine}
		\begin{description}
		\WhenGrd
			\begin{description}
			\nItem{ grd1 }{ MINE = \emptyset  }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ MINE :=  \{ M\}  }
			\nItem{ act5 }{ waterLevel(M) :=  LOW }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description}
\end{document}
