% control-summary.tex --- control modelling summary table -*-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/>.


\resizebox{\textwidth}{!}{
  \centering
  \renewcommand{\arraystretch}{1.1}
  \footnotesize
  \begin{tabular}{|c|ccccccc|}
    \hline
    \diagbox[width=3cm,height=0.9cm]{Criteria}{Language}
    & \B
    & \eventb
    & \alloy
    & \dash
    & \tla
    & \pluscal
    & \asmetal
    \\ \hline
    Snapshot variables
    & \bcode{VARIABLES}         % \B
    & \eventbcode{VARIABLES}    % \eventb
    & varies                    % \alloy
    & in \dashcode{state}       % \dash
    & \tlacode{VARIABLES}       % \tla
    & \pluscalcode{variables}   % \pluscal
    & \asmcode{signature}       % \asmetal
    \\
    Initialization
    & {\footnotesize\bcode{INITIALISATION}}      % \B
    & {\footnotesize\eventbcode{INITIALISATION}} % \eventb
    & \alloycode{init}                           % \alloy
    & \dashcode{init}                            % \dash
    & \tlacode{Init}                             % \tla
    & \pluscalcode{variables}                    % \pluscal
    & \asmcode{default init}                     % \asmetal
    \\
    $TR$ representation
    & I                         % \B
    & I                         % \eventb
    & E                         % \alloy
    & I                         % \dash
    & ME                        % \tla
    & I                         % \pluscal
    & ME                        % \asmetal
    \\
    Frame problem
    & unchanged                 % \B
    & unchanged                 % \eventb
    & may change                % \alloy
    & \dashcode{env}            % \dash
    & \tlacode{UNCHANGED}       % \tla
    & unchanged                 % \pluscal
    & \asmcode{monitored}       % \asmetal
    \\
    \begin{tabular}[c]{@{}c@{}}Control state\\[-0.5em]hierarchy\end{tabular}
    & \md                       % \B
    & \md                       % \eventb
    & \md                       % \alloy
    & \checkmark                         % \dash
    & \md                       % \tla
    & \md                       % \pluscal
    & \md                       % \asmetal
    \\
    Invariants
    & \bcode{INVARIANT} {\scriptsize(V)}       % \B
    & \eventbcode{INVARIANTS} {\scriptsize(V)} % \eventb
    & \alloycode{fact} {\scriptsize(C)}        % \alloy
    & \dashcode{invariant} {\scriptsize(C)}    % \dash
    & S {\scriptsize(V)}                       % \tla
    & S {\scriptsize(V)}                       % \pluscal
    & \asmcode{invariant} {\scriptsize(V)}     % \asmetal
    \\
    Fairness
    & \md                                     % \B
    & \md                                     % \eventb
    & \md                                     % \alloy
    & \md                                     % \dash
    & \tlacode{WF}, \tlacode{SF}              % \tla
    & \pluscalcode{fair}, \pluscalcode{fair+} % \pluscal
    & \begin{tabular}[c]{@{}c@{}}\asmcode{JUSTICE},\\[-0.5em]\asmcode{COMPASSION}\end{tabular} % \asmetal
    \\
    Stuttering
    & E                         % \B
    & E                         % \eventb
    & E                         % \alloy
    & I(m) + E                  % \dash
    & I(a) + E                  % \tla
    & I(a) + E                  % \pluscal
    & I(m) + E                  % \asmetal
    \\
    \hline
  \end{tabular}
}


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