m3_m3-ctr-plf.tex

\noindent \ref{m3:ctr:plf} [p] \textbf{event}
\begin{block}
\item \textbf{during}
\begin{block}
\item[ \eqref{default} ]$\false$ %
\end{block}
\item \textbf{begin}
\begin{block}
\item[ \eqref{SKIP:in} ]$in' = in$ %
\item[ \eqref{SKIP:loc} ]$loc' = loc$ %
\item[ \eqref{m3:cp:act0} ]$osgn' = osgn \bunion \{ p \} $ %
\end{block}
\item \textbf{end} \\
\end{block}