% control-trans.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
Join (member_) =
PRE
   member_ : MEMBERID &
   member_ /: member
THEN
   member := member \/ { member_ }
END;
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=dash]
// Dash
trans join {
  when !(in_m in members)
  do members' = members + in_m
}
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{0.50\textwidth}
\begin{lstlisting}[style=tla]
\* TLA+
Join(member) ==
  /\ member \in MemberID
  /\ member \notin members
  /\ members' = members \union {member}
  /\ UNCHANGED << books, loans, reservations >>
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=eventb]
// Event-B
Join:  // not extended ordinary
  ANY
    member
  WHERE
    member : MemberID not theorem   // grd1
    member /: members not theorem   // grd2
  THEN
    members := members \/ {member}  // act1
END
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=alloy]
// Alloy
// Lib is the snapshot sig
/*-------------------
   Join
-------------------*/
pred CanJoin[m: Member, L: Lib] {
  // m does not exist in the Library.
  no (m & L.members)
}

pred Join[m: Member, L, L': Lib] {
  ----Precondition-----
  CanJoin[m, L]
  -----Postcondition------
  // add the m in the set of members
  L'.members = L.members + m
  ------Nochanges-----
  NoChangebooks[L, L']
  NoChangeloan[L, L']
  NoChangeSeqBook[L, L']
  NochangeRenew[L, L']
}
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=pluscal]
\* PlusCal
process Join = "Join"
variable member \in MemberID
begin
  join:
    when member \notin members;
    members := members \union {member};
    goto join
end process
\end{lstlisting}

\begin{lstlisting}[style=asmetal]
// AsmetaL
rule r_Join($m in MemberID) =
  if (notin(members, $m)) then
    members := union(members, {$m})
  endif
\end{lstlisting}
\end{minipage}
%
\caption{Transitions (from the Library case study)}
\label{fig:control/trans}
\end{figure*}


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