% control-incon-b-eventb-deadlock.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.33\textwidth}
\begin{lstlisting}[style=b]
// B
MACHINE example
SETS
  A = {a1, a2}
VARIABLES
  a
INVARIANT
  a: A
INITIALISATION
  a := a1
OPERATIONS
  %*\colorbox{orange!40}{contra\_pre =}*)
  PRE
    FALSE = TRUE // problem
  THEN
    a := a2
  END;
  %*\colorbox{orange!40}{contra\_post =}*)
  PRE
    a = a1
  THEN
    a :: {} // problem
  END
END
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.33\textwidth}
\begin{lstlisting}[style=eventb]
// Event-B
CONTEXT
  c0
SETS
  A
CONSTANTS
  a1
  a2
AXIOMS
  partition(A, {a1}, {a2})
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.33\textwidth}
\begin{lstlisting}[style=eventb]
// Event-B (continued)
MACHINE
  m0
SEES
  c0
VARIABLES
  a
INVARIANTS
  a : A
EVENTS
  INITIALISATION:
  THEN
    a := a1
  END
  %*\colorbox{orange!40}{contra\_pre:}*)
  WHERE
    FALSE = TRUE // problem
  THEN
    a := a2
  END
  %*\colorbox{orange!40}{contra\_post:}*)
  WHERE
    a = a1
  THEN
    a :: {} // problem
  END
\end{lstlisting}
\end{minipage}
\caption{A deadlocked transition system in \B{} and \eventb}
\label{fig:control/incon-b-eventb-deadlock}
\end{figure*}


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