This annex present the complete machines of the mine pump example described in section \ref{12_06_Decomposition_according_to_Agents}.

\lstset{
frame=lines,
numbers=none,
captionpos=t, 
caption=Mine pump example: Initial context,
label=lst_EVENT_B_MinePump_Example_InitialContext_ANX
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\CONTEXT{MineContext}
\SETS
	\begin{description}
		\Item{ ONOFF }
		\Item{ LEVEL }
		\Item{ MINE\_SET }
	\end{description}
\CONSTANTS
	\begin{description}
		\Item{ ON }
		\Item{ OFF }
		\Item{ LOW }
		\Item{ MEDIUM }
		\Item{ HIGH }
		\Item{ M }
	\end{description}
\AXIOMS
	\begin{description}
		\nItemX{ axm1 }{ partition(ONOFF, \{ ON\} , \{ OFF\} ) }
		\nItemX{ axm2 }{ partition(LEVEL, \{ LOW\} , \{ MEDIUM\} , \{ HIGH\} ) }
		\nItemX{ axm3 }{ partition(MINE\_SET, \{ M\} ) }
	\end{description}
\END
\end{description}
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: Initial machine,
label=lst_EVENT_B_MinePump_Example_InitialMachine_ANX
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE }
		\Item{ pump }
		\Item{ bell }
		\Item{ methane }
		\Item{ waterLevel }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ inv1 }{ MINE \in  \pow(MINE\_SET) }
		\nItemX{ inv2 }{ pump \in  MINE \tfun  ONOFF }
		\nItemX{ inv3 }{ bell \in  MINE \tfun  BOOL }
		\nItemX{ inv4 }{ methane \in  MINE \tfun  BOOL }
		\nItemX{ inv5 }{ waterLevel \in  MINE \tfun  LEVEL }
		\nItemX{ inv6 }{ dom(pump) = MINE }
		\nItemX{ inv7 }{ dom(bell) = MINE }
		\nItemX{ inv8 }{ dom(methane) = MINE }
		\nItemX{ inv9 }{ dom(waterLevel) = MINE }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act1 }{ MINE :=  \emptyset  }
			\nItemX{ act2 }{ pump :=  \emptyset  }
			\nItemX{ act3 }{ bell :=  \emptyset  }
			\nItemX{ act4 }{ methane :=  \emptyset  }
			\nItemX{ act5 }{ waterLevel :=  \emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\ItemX{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ status \in  ONOFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateBell}
		\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 }{ bell(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateMethane}
		\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}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\ItemX{ level }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ level \in  LEVEL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel(m) :=  level }
			\end{description}
		\EndAct
		\end{description}
	\EVT {addMine}
		\begin{description}
		\WhenGrd
			\begin{description}
			\nItemX{ grd1 }{ MINE = \emptyset  }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ MINE :=  \{ M\}  }
			\nItemX{ act2 }{ pump(M) :=  OFF }
			\nItemX{ act3 }{ bell(M) :=  FALSE }
			\nItemX{ act4 }{ methane(M) :=  FALSE }
			\nItemX{ act5 }{ waterLevel(M) :=  LOW }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: PumpController machine,
label=lst_EVENT_B_MinePump_Example_PumpCtrlMachine_ANX
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{PumpController}
\REFINES{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE }
		\Item{ pump }
		\Item{ bell }
		\Item{ methane }
		\Item{ waterLevel }
	\end{description}
\EVENTS
	\INITIALISATION
		\\\textit{extended}
		\begin{description}
		\BeginAct
			\begin{description}
			\nItem{ act1 }{ MINE :=  \emptyset  }
			\nItem{ act2 }{ pump :=  \emptyset  }
			\nItem{ act3 }{ bell :=  \emptyset  }
			\nItem{ act4 }{ methane :=  \emptyset  }
			\nItem{ act5 }{ waterLevel :=  \emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {high\_water\_detected}
	\cmt{ Internal Event }
	\REF {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd2 }{ m \in  MINE }
			\nItemX{ grd1 }{ waterLevel(m) = HIGH }
			\nItemX{ grd3 }{ methane(m) = FALSE }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = ON }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  ON }
			\end{description}
		\EndAct
		\end{description}
	\EVT {low\_water\_detected}
	\cmt{ Internal Event }
	\REF {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = LOW }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = OFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  OFF }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateBell}
	\cmt{ External Event }
	\EXTD {updateBell}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ bell(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateMethane}
	\cmt{ External Event }
	\EXTD {updateMethane}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ methane(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateWaterLevel}
	\cmt{ External Event }
	\EXTD {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ level }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ level \in  LEVEL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ waterLevel(m) :=  level }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: WaterLevelSensor machine,
label=lst_EVENT_B_MinePump_Example_WaterLevelSensorMachine_ANX
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{WaterLevelSensor}
\REFINES{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE }
		\Item{ pump }
		\Item{ bell }
		\Item{ methane }
		\Item{ waterLevel }
	\end{description}
\EVENTS
	\INITIALISATION
		\\\textit{extended}
		\begin{description}
		\BeginAct
			\begin{description}
			\nItem{ act1 }{ MINE :=  \emptyset  }
			\nItem{ act2 }{ pump :=  \emptyset  }
			\nItem{ act3 }{ bell :=  \emptyset  }
			\nItem{ act4 }{ methane :=  \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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = MEDIUM }
			\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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = LOW }
			\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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = MEDIUM }
			\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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = HIGH }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel(m) :=  HIGH }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updatePump}
	\cmt{ External Event }
	\EXTD {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  ONOFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ pump(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateBell}
	\cmt{ External Event }
	\EXTD {updateBell}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ bell(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateMethane}
	\cmt{ External Event }
	\EXTD {updateMethane}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ methane(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: AlarmController machine,
label=lst_EVENT_B_MinePump_Example_AlarmControllerMachine_ANX
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{AlarmController}
\REFINES{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE }
		\Item{ pump }
		\Item{ bell }
		\Item{ methane }
		\Item{ waterLevel }
	\end{description}
\EVENTS
	\INITIALISATION
		\\\textit{extended}
		\begin{description}
		\BeginAct
			\begin{description}
			\nItem{ act1 }{ MINE :=  \emptyset  }
			\nItem{ act2 }{ pump :=  \emptyset  }
			\nItem{ act3 }{ bell :=  \emptyset  }
			\nItem{ act4 }{ methane :=  \emptyset  }
			\nItem{ act5 }{ waterLevel :=  \emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {methane\_detected}
	\cmt{ Internal Event }
	\REF {updateBell}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ methane(m) = TRUE }
			\nItemX{ grd3 }{ bell(m) = FALSE }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = TRUE }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ bell(m) :=  TRUE }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updatePump}
	\cmt{ External Event }
	\EXTD {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  ONOFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ pump(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateMethane}
	\cmt{ External Event }
	\EXTD {updateMethane}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ methane(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateWaterLevel}
	\cmt{ External Event }
	\EXTD {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ level }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ level \in  LEVEL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ waterLevel(m) :=  level }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: MethaneSensor machine,
label=lst_EVENT_B_MinePump_Example_MethaneSensorMachine_ANX
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{MethaneSensor}
\REFINES{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE }
		\Item{ pump }
		\Item{ bell }
		\Item{ methane }
		\Item{ waterLevel }
	\end{description}
\EVENTS
	\INITIALISATION
		\\\textit{extended}
		\begin{description}
		\BeginAct
			\begin{description}
			\nItem{ act1 }{ MINE :=  \emptyset  }
			\nItem{ act2 }{ pump :=  \emptyset  }
			\nItem{ act3 }{ bell :=  \emptyset  }
			\nItem{ act4 }{ methane :=  \emptyset  }
			\nItem{ act5 }{ waterLevel :=  \emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {methane\_leak}
	\cmt{ Internal Event }
	\REF {updateMethane}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = TRUE }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ methane(m) :=  TRUE }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updatePump}
	\cmt{ External Event }
	\EXTD {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  ONOFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ pump(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateBell}
	\cmt{ External Event }
	\EXTD {updateBell}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ status }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ status \in  BOOL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ bell(m) :=  status }
			\end{description}
		\EndAct
		\end{description}
	\EVT {updateWaterLevel}
	\cmt{ External Event }
	\EXTD {updateWaterLevel}
		\begin{description}
		\AnyPrm
			\begin{description}
			\Item{ m }
			\Item{ level }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItem{ grd1 }{ m \in  MINE }
			\nItem{ grd2 }{ level \in  LEVEL }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ waterLevel(m) :=  level }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\lstset{
frame=lines,
numbers=none,
captionpos=t,
caption=Mine pump example: re-composed machine,
label=lst_EVENT_B_MinePump_Example_MinePumpReunificationMachine_ANX
}
\begin{lstlisting}[escapechar=\%] 
% \begin{description}
\MACHINE{MinePumpReunification}
\REFINES{MinePump}
\SEES{MineContext}
\VARIABLES
	\begin{description}
		\Item{ MINE }
		\Item{ pump }
		\Item{ bell }
		\Item{ methane }
		\Item{ waterLevel }
	\end{description}
\INVARIANTS
	\begin{description}
		\nItemX{ inv1 }{ MINE \in  \pow(MINE\_SET) }
		\nItemX{ inv2 }{ pump \in  MINE \tfun  ONOFF }
		\nItemX{ inv3 }{ bell \in  MINE \tfun  BOOL }
		\nItemX{ inv4 }{ methane \in  MINE \tfun  BOOL }
		\nItemX{ inv5 }{ waterLevel \in  MINE \tfun  LEVEL }
	\end{description}
\EVENTS
	\INITIALISATION
		\begin{description}
		\BeginAct
			\begin{description}
			\nItemX{ act1 }{ MINE :=  \emptyset  }
			\nItemX{ act2 }{ pump :=  \emptyset  }
			\nItemX{ act3 }{ bell :=  \emptyset  }
			\nItemX{ act4 }{ methane :=  \emptyset  }
			\nItemX{ act5 }{ waterLevel :=  \emptyset  }
			\end{description}
		\EndAct
		\end{description}
	\EVT {methane\_detected}
	\cmt{ Internal Event }
	\REF {updateBell}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ methane(m) = TRUE }
			\nItemX{ grd3 }{ bell(m) = FALSE }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = TRUE }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ bell(m) :=  TRUE }
			\end{description}
		\EndAct
		\end{description}
	\EVT {methane\_leak}
	\cmt{ Internal Event }
	\REF {updateMethane}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = TRUE }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ methane(m) :=  TRUE }
			\end{description}
		\EndAct
		\end{description}
	\EVT {high\_water\_detected}
	\cmt{ Internal Event }
	\REF {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd2 }{ m \in  MINE }
			\nItemX{ grd1 }{ waterLevel(m) = HIGH }
			\nItemX{ grd3 }{ methane(m) = FALSE }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = ON }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  ON }
			\end{description}
		\EndAct
		\end{description}
	\EVT {low\_water\_detected}
	\cmt{ Internal Event }
	\REF {updatePump}
		\begin{description}
		\AnyPrm
			\begin{description}
			\ItemX{ m }
			\end{description}
		\WhereGrd
			\begin{description}
			\nItemX{ grd1 }{ m \in  MINE }
			\nItemX{ grd2 }{ waterLevel(m) = LOW }
			\end{description}
		\Witnesses
			\begin{description}
			\nItem{ status }{ status = OFF }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ pump(m) :=  OFF }
			\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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = MEDIUM }
			\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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = LOW }
			\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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = MEDIUM }
			\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}
		\Witnesses
			\begin{description}
			\nItem{ level }{ level = HIGH }
			\end{description}
		\ThenAct
			\begin{description}
			\nItemX{ act1 }{ waterLevel(m) :=  HIGH }
			\end{description}
		\EndAct
		\end{description}
	\EVT {addMine}
	\EXTD {addMine}
		\begin{description}
		\WhenGrd
			\begin{description}
			\nItem{ grd1 }{ MINE = \emptyset  }
			\end{description}
		\ThenAct
			\begin{description}
			\nItem{ act1 }{ MINE :=  \{ M\}  }
			\nItem{ act2 }{ pump(M) :=  OFF }
			\nItem{ act3 }{ bell(M) :=  FALSE }
			\nItem{ act4 }{ methane(M) :=  FALSE }
			\nItem{ act5 }{ waterLevel(M) :=  LOW }
			\end{description}
		\EndAct
		\end{description}
\END
\end{description} 
% 
\end{lstlisting}