% control-init.tex -*-latex-*-

% Copyright (C) 2020 Amin Bandali <bandali@uwaterloo.ca>

% This file is part of Amin Bandali's MMath thesis.

% This thesis is free software: you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation, either version 3 of the License, or
% (at your option) any later version.

% This thesis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this thesis.  If not, see <https://www.gnu.org/licenses/>.


\begin{figure*}
%
\begin{minipage}[t]{0.32\textwidth}
\begin{lstlisting}[style=b]
// B
INITIALISATION
  loan := {} ||
  book := {} ||
  member := {} ||
  reservation := {}
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.32\textwidth}
\begin{lstlisting}[style=dash]
// Dash
conc state Library {
  ...
  init {
    no members
    no books
    no loans
    no reservations
  }
}
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.32\textwidth}
\begin{lstlisting}[style=tla]
\* TLA+
Init ==
  /\ members = {}
  /\ books = {}
  /\ loans = <<>>
  /\ reservations = <<>>
  \* <<>> is the empty sequence/function
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{0.32\textwidth}
\begin{lstlisting}[style=eventb]
// Event-B
INITIALISATION
THEN
  loans, members, books, reservations := {}, {}, {}, {}  // act1
END
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.34\textwidth}
\begin{lstlisting}[style=alloy]
// Alloy
// Lib is the snapshot sig
pred Init [L: Lib] {
  no L.books
  no L.members
  no L.loan
  no L.membersReservingOneBook
  no L.Renew
}
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.33\textwidth}
\begin{lstlisting}[style=pluscal]
\* PlusCal
variables loans = <<>>,
          members = {},
          books = {},
          reservations = <<>>;
\end{lstlisting}
\end{minipage}

\centering
\begin{minipage}[t]{0.33\textwidth}
\begin{lstlisting}[style=asmetal]
// AsmetaL
default init s0:
  function members = {}
  function books = {}
  function loans = {}
  function reservations = {}
\end{lstlisting}
\end{minipage}
%
\caption{Initialization (from the Library case study)}
\label{fig:control/init}
\end{figure*}


%% Local Variables:
%% tex-main-file: "../bandali-mmath-thesis.tex"
%% End:
