% data-records.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.49\textwidth}
\begin{lstlisting}[style=b]
// B
MACHINE rectest
VARIABLES vrec, vbar
INVARIANT
  vrec : struct(foo : INTEGER, bar : BOOL) &
  vbar : BOOL
INITIALISATION
  vrec := rec(foo : 9, bar : FALSE) ||
  vbar := TRUE
OPERATIONS
  setvbar = vbar := vrec'bar
END
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=tla]
\* TLA+
------------ MODULE rectest ------------
EXTENDS Integers
VARIABLES vrec, vbar

Init ==
  /\ vrec = [vrec |-> 9, bar |-> FALSE]
  /\ vbar = TRUE

setvbar ==
  /\ vbar' = vrec.bar
  /\ UNCHANGED vrec

TypeOK ==
  /\ vrec \in [foo : Int, bar : BOOLEAN]
  /\ vbar \in BOOLEAN

Spec ==
  /\ Init
  /\ [][setvbar]_<<vrec, vbar>>
  /\ []TypeOK
========================================
\end{lstlisting}
\end{minipage}
%
\caption{Records in \B{} and \tla}
\label{fig:data/records}
\end{figure*}


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