% control-tr.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=tla]
\* TLA+
Next ==
  \/ \E b \in BookID:
      \/ Acquire(b)
      \/ Discard(b)
      \/ Return(b)
  \/ \E m \in MemberID:
      \/ Join(m)
      \/ Leave(m)
  \/ \E m \in MemberID, b \in BookID:
      \/ Cancel(m, b)
      \/ Lend(m, b)
      \/ Renew(m, b)
      \/ Reserve(m, b)
      \/ Take(m, b)
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=alloy]
// Alloy
pred TransLCR[m: Member]
{
  all l: Lib - LibOrd/last |
    LCR[m, l, l.LibOrd/next]
}
pred LCR[m: Member, L, L': Lib]
{
  some b: Book |
    Cancel[m, b, L, L']
    or Return[m, b, L, L']
    // For test switch Leave and BuggyLeave
    or Leave[m, L, L']
    // or BuggyLeave[L, L']
}
\end{lstlisting}
\end{minipage}

\centering
\begin{minipage}[t]{0.69\textwidth}
\begin{lstlisting}[style=asmetal]
// AsmetaL
main rule r_Main =
  choose $b in BookID, $m in MemberID, $rule in RuleId with true do
    switch($rule)
      case ACQUIRE:
        r_Acquire[$b]
      case CANCEL:
        r_Cancel[$m, $b]
      case DISCARD:
        r_Discard[$b]
      case JOIN:
        r_Join[$m]
      case LEAVE:
        r_Leave[$m]
      case LEND:
        r_Lend[$m, $b]
      case RENEW:
        r_Renew[$m, $b]
      case RESERVE:
        r_Reserve[$m, $b]
      case RETURN:
        r_Return[$b]
      case TAKE:
        r_Take[$m, $b]
      endswitch
\end{lstlisting}
\end{minipage}
%
\caption{Explicit transition relation (from the Library case study)}
\label{fig:control/tr}
\end{figure*}


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