% control-snapshot.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
ABSTRACT_VARIABLES
  loan,
  member,
  book,
  reservation
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.32\textwidth}
\begin{lstlisting}[style=dash]
// Dash
conc state Library {
    env in_m: lone MemberID
    env in_b: lone BookID
    members: set MemberID
    books: set BookID
    loans: books one -> one (members)
    reservations: books one -> one (seq members)
  ...
}
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.32\textwidth}
\begin{lstlisting}[style=tla]
\* TLA+
VARIABLES members, books, loans, reservations
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{0.32\textwidth}
\begin{lstlisting}[style=eventb]
// Event-B
VARIABLES
  loans
  members
  books
  reservations
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.34\textwidth}
\begin{lstlisting}[style=alloy]
// Alloy
sig Lib {
  members:set Member,
  books: set Book ,
  loan: books -> members,
  membersReservingOneBook: seq members -> books,
  Renew: books -> members
}
\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.66\textwidth}
\begin{lstlisting}[style=asmetal]
// AsmetaL
signature:
  ...
  controlled members: Powerset(MemberID)
  controlled books: Powerset(BookID)
  controlled loans: Powerset(Prod(BookID, Powerset(MemberID)))
  controlled reservations: Powerset(Prod(BookID, Seq(MemberID)))
  ...
\end{lstlisting}
\end{minipage}
%
\caption{Snapshots and variables (from the Library case study)}
\label{fig:control/snapshot}
\end{figure*}


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