\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 PumpController}
\rhead {\rm Page \thepage~of \pageref{LastPage}}
\lfoot{}\cfoot{}\rfoot{}
\pagestyle{fancy}
%---------------------------------------------------------
\begin{document}
\thispagestyle{empty}
\begin{description}
\BTitle{PumpController}{16 Apr 2010}{02:22:03 PM}
\MACHINE{PumpController}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ methane }
		\bcmt{ Shared variable, DO NOT REFINE }
		\Item{ waterLevel }
		\bcmt{ Shared variable, DO NOT REFINE }
		\Item{ pump }
		\bcmt{ Private variable }
		\Item{ MINE }
		\bcmt{ Shared variable, DO NOT REFINE }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ MinePump\_inv1 }{ MINE \in  \pow(MINE\_SET) }
		\nItemX{ MinePump\_inv2 }{ pump \in  MINE \tfun  ONOFF }
		\nItemX{ MinePump\_inv4 }{ methane \in  MINE \tfun  BOOL }
		\nItemX{ MinePump\_inv5 }{ waterLevel \in  MINE \tfun  LEVEL }
		\nItemX{ MinePump\_inv6 }{ dom(pump) = MINE }
		\nItemX{ MinePump\_inv8 }{ dom(methane) = MINE }
		\nItemX{ MinePump\_inv9 }{ dom(waterLevel) = MINE }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act1 }{ MINE :=  \emptyset  }
			\nItemX{ act2 }{ pump :=  \emptyset  }
			\nItemX{ act4 }{ methane :=  \emptyset  }
			\nItemX{ act5 }{ waterLevel :=  \emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ pump(m) = ON \lor  pump(m) = OFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump :|  (pump(m) = OFF \land  pump'=(pump \ovl  \{ m \mapsto  ON\} ) )
		\\\hspace*{1,6 cm}  \lor  (pump(m) = ON \land  pump'=(pump \ovl  \{ m \mapsto  OFF\} )) }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateMethane}
	\cmt{ External event, DO NOT REFINE }
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\ItemX{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ methane(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateWaterLevel}
	\cmt{ External event, DO NOT REFINE }
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = LOW \lor 
		\\\hspace*{1,2 cm}  waterLevel(m) = MEDIUM \lor 
		\\\hspace*{1,2 cm}  waterLevel(m) = HIGH }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel :|  
		\\\hspace*{1,2 cm}  ( waterLevel(m) = HIGH \land  waterLevel'=(waterLevel \ovl  \{ m \mapsto  MEDIUM\} ))
		\\\hspace*{1,2 cm}  \lor  ( waterLevel(m) = MEDIUM \land  waterLevel'=(waterLevel \ovl  \{ m \mapsto  LOW\} ))
		\\\hspace*{1,2 cm}  \lor  ( waterLevel(m) = MEDIUM \land  waterLevel'=(waterLevel \ovl  \{ m \mapsto  HIGH\} ))
		\\\hspace*{1,2 cm}  \lor  ( waterLevel(m) = LOW \land  waterLevel'=(waterLevel \ovl  \{ m \mapsto  MEDIUM\} )) }
			\end{description}
		\EndAct
		\end{description}
	\EVT {addMine}
	\cmt{ External event, DO NOT REFINE }
		\begin{description}
		\WhenGrd
			\begin{description}
			\nItemX{ grd1 }{ MINE = \emptyset  }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ MINE :=  \{ M\}  }
			\nItemX{ act2 }{ pump(M) :=  OFF }
			\nItemX{ act4 }{ methane(M) :=  FALSE }
			\nItemX{ act5 }{ waterLevel(M) :=  LOW }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description}
\end{document}
