sample-main.tex

\usepackage{verbatim}
\usepackage{mdframed}

\title{A Sample Document\\for the Usages of \textsf{lstEventB} Package}
\author{Thai Son Hoang\\ECS, University of Southampton\\\texttt{<T dot S dot Hoang at ecs dot soton dot ac dot uk>}}

\begin{document}
\maketitle
For convenient, we define macro \verb|\EventB| for \EventB. 

We start first with some inline \EventB code by embedding them using a pair of \verb$|$, for example \verb$|@grd1: SNSR = FALSE|$ gives |@grd1: SNSR = FALSE|. Any \EventB formulae including Unicode symbols will be typeset using the \verb|bsymb| package accordingly.

\begin{EventBNoShortInline}
  \begin{table}[!htbp]
    \centering
    \begin{tabular}{|l|l|l|}
      \hline
      ASCII & Symbols & Explanation \\
      \hline
      \verb$!:$ & \lstinline$!:$ & Set membership \\
      \verb$/:$ & \lstinline$/:$ & Set non-membership \\
      \verb$<:$ & \lstinline$<:$ & Subset \\
      \verb$/<:$ & \lstinline$/<:$ & Not a subset \\
      \verb$<<:$ & \lstinline$<<:$ & Proper subset \\
      \verb$/<<:$ & \lstinline$/<<:$ & Not a proper subset \\
      \verb$!finite$ & \lstinline$!finite$ & Finite \\
      \verb$!partition$ & \lstinline$!partition$ & Partition \\
      \hline
    \end{tabular}
    \caption{Set predicates}
  \end{table}
  
  
  \begin{table}[!htbp]
    \centering
    \begin{tabular}{|l|l|l|}
      \hline
      ASCII & Symbols & Explanation \\
      \hline
      \verb$!BOOL$ & \lstinline$!BOOL$ & BOOL set \\
      \verb$!TRUE$ & \lstinline$!TRUE$ & TRUE \\
      \verb$!FALSE$ & \lstinline$!FALSE$ & FALSE \\
      \verb$!bool$ & \lstinline$!bool$ & bool predicate \\
      \hline
    \end{tabular}
    \caption{BOOL and bool}
  \end{table}
  
  \begin{table}[!htbp]
    \centering
    \begin{tabular}{|l|l|l|}
      \hline
      ASCII & Symbols & Explanation \\
      \hline
      \verb$!INT$ & \lstinline$!INT$ & Set of integer numbers \\
      \verb$!NAT$ & \lstinline$!NAT$ & Set of natural numbers \\
      \verb$!NAT1$ & \lstinline$!NAT1$ & Set of positive natural numbers \\
      \verb$!min$ & \lstinline$!min$ & Mininum \\
      \verb$!max$ & \lstinline$!max$ & Maximum \\
      \verb$-$ & \lstinline$-$ & Difference \\
      \verb$*$ & \lstinline$*$ & Product \\
      \verb$!/$ & \lstinline$!/$ & Quotient \\
      \verb$!mod$ & \lstinline$!mod$ & Remainder \\
      \verb$..$ & \lstinline$..$ & Interval  \\
      \hline
    \end{tabular}
    \caption{Numbers}
  \end{table}
  
  \begin{table}[!htbp]
    \centering
    \begin{tabular}{|l|l|l|}
      \hline
      ASCII & Symbols & Explanation \\
      \hline
      \verb$>$ & \lstinline$>$ & Greater \\
      \verb$<$ & \lstinline$<$ & Less \\
      \verb$>=$ & \lstinline$>=$ & Greater or equal \\
      \verb$<=$ & \lstinline$<=$ & Less or equal \\
      \hline
    \end{tabular}
    \caption{Number predicates}
  \end{table}
  
  \begin{table}[!htbp]
    \centering
    \begin{tabular}{|l|l|l|}
      \hline
      ASCII & Symbols & Explanation \\
      \hline
      \verb$<->$ & \lstinline$<->$ & Relations \\
      \verb$!dom$ & \lstinline$!dom$ & Domain \\
      \verb$!ran$ & \lstinline$!ran$ & Range \\
      \verb$<<->$ & \lstinline$<<->$ & Total relations \\
      \verb$<->>$ & \lstinline$<<->$ & Surjective relations \\
      \verb$<<->>$ & \lstinline$<<->>$ & Total surjective relations \\
      \verb$!circ$ & \lstinline$!circ$ & Backward composition \\
      \verb$!id$ & \lstinline$!id$ & Identity \\
      \verb$<|$ & \lstinline$<|$ & Domain restriction \\
      \verb$<<|$ & \lstinline$<<|$ & Domain subtraction \\
      \verb$|>$ & \lstinline$|>$ & Range restriction \\
      \verb$|>>$ & \lstinline$|>>$ & Range subtraction \\
      \verb$~$ & \lstinline$~$ & Inverse \\
      \verb$<+$ & \lstinline$<+$ & Overriding \\
      \verb$><$ & \lstinline$><$ & Direct product \\
      \verb$||$ & \lstinline$||$ & Parallel product \\
      \verb$!prj1$ & \lstinline$!prj1$ & First projection \\
      \verb$!prj2$ & \lstinline$!prj2$ & Second projection \\
      \hline
    \end{tabular}
    \caption{Relations}
  \end{table}
  
  \begin{table}[!htbp]
    \centering
    \begin{tabular}{|l|l|l|}
      \hline
      ASCII & Symbols & Explanation \\
      \hline
      \verb$+->$ & \lstinline$+->$ & Partial functions \\
      \verb$-->$ & \lstinline$-->$ & Total functions \\
      \verb$>+>$ & \lstinline$>+>$ & Partial injections \\
      \verb$>->$ & \lstinline$>->$ & Total injections \\
      \verb$+>>$ & \lstinline$+>>$ & Partial surjections \\
      \verb$->>$ & \lstinline$->>$ & Total surjections \\
      \verb$>->>$ & \lstinline$>->>$ & Bijections \\
      \verb$%$ & \lstinline$%$ & Lambda abstraction \\
      \hline
    \end{tabular}
    \caption{Functions}
  \end{table}
  
  \begin{table}[!htbp]
    \centering
    \begin{tabular}{|l|l|l|}
      \hline
      ASCII & Symbols & Explanation \\
      \hline
      \verb$:=$ & \lstinline$:=$ & Becomes equal to \\
      \verb$::$ & \lstinline$::$ & Choice from a set  \\
      \verb$:|$ & \lstinline$:|$ & Choice by predicate \\
      \hline
    \end{tabular}
    \caption{Functions}
  \end{table}
\end{EventBNoShortInline}

More complete piece of code (including the Unicode symbols) can be typeset using the \verb|EventBcode| environment. Below is the typesetting of an \EventB machine.
\begin{EventBcode}
machine Sensor_m0_SNSR
variables
	SNSR
invariants
	theorem @thm0_1: SNSR ∈ BOOL
events

	INITIALISATION
	begin
		@act1: SNSR ≔ FALSE
	end

	SNSR_on
	when
		@grd1: SNSR = FALSE
	then
		@act1: SNSR ≔ TRUE
	end

	SNSR_off
	when
		@grd1: SNSR = TRUE
	then
		@act1: SNSR ≔ FALSE
	end

end
\end{EventBcode}

One can change the different colour options.  For example, \verb|\EventBSetKeywordColour{blue!50!black}| will change the keyword colour to dark blue. (This has effects only when 
\begin{EventBcode}
machine Sensor_m0_SNSR
variables
	SNSR
invariants
	theorem @thm0_1: SNSR ∈ BOOL
\end{EventBcode}

One can includes external file containing \EventB code using the \verb|\EventBinputlisting| command.  For example the following is the result of including the code in the file \verb|Sensor_m1_DEP.bumx| using \verb|\EventBinputlisting{Sensor_m1_DEP.bumx}|.
\EventBinputlisting{Sensor_m1_DEP.bumx}

More specifically, one can specify more details on the inclusion, e.g., the ranges, as the following example\\
\verb|\EventBinputlisting[firstline=16,lastline=20]{Sensor_m2_snsr.bumx}|
gives
\EventBinputlisting[firstline=16,lastline=20]{Sensor_m2_snsr.bumx}

\EventBinputlisting{Sensor_m3_Ctrl.bumx}
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "sample-lstEventB"
%%% End: