m3_m0-leave.tex

\noindent \ref{m0:leave} [t] \textbf{event}
\begin{block}
\item \textbf{during}
\begin{block}
\item[ \eqref{lv:c0} ]$t \in in $ %
\item[ \eqref{lv:c1} ]$loc.t = ext $ %
\end{block}
\item \textbf{when}
\begin{block}
\item[ \eqref{lv:grd0} ]$t \in in $ %
\item[ \eqref{lv:grd1} ]$loc.t = ext $ %
\end{block}
\item \textbf{begin}
\begin{block}
\item[ \eqref{lv:a0} ]$in' = in \setminus \{ t \} $ %
\item[ \eqref{lv:a2} ]$loc' = \{ t \} \domsub loc $ %
\item[ \eqref{m3:ext:act0} ]$isgn' = isgn$ %
\item[ \eqref{m3:ext:act1} ]$osgn' = osgn$ %
\end{block}
\item \textbf{end} \\
\end{block}