% control-incon-dash-contra-postcond.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{lstlisting}[style=dash]
abstract sig A {}
one sig a1, a2, a3 extends A {}

conc state Example {
  v: one A
  trans a1_to_a2 {
    when { v = a1 }
    do { v' = a2 }
  }
  trans %*\colorbox{orange!40}{a2\_to\_a3}*) {
    when { v = a2 }
    // contradictory postcondition:
    do {
      v' = a2
      v' = a3
    }
  }
  init { v = a1 }
}
\end{lstlisting}
\caption{\dash{} model with a contradictory transition postcondition}
\label{fig:control/incon-dash-contra-postcond}
\end{figure*}


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