% conclusion.tex --- concluding remarks of the thesis -*-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/>.


\chapter{Conclusion}
\label{chp:conclusion}

This thesis presents
\begin{itemize}
\item a set of criteria to compare declarative modelling languages;
\item a diverse set of case studies on the data- vs. control-oriented
  characterization spectrum;
\item the comparison of the selected declarative modelling languages
  (\B, \eventb, \alloy, \dash, \tla, \pluscal, and \asmetal) based on
  these criteria by carrying out the case studies; and
\item our recommendations for the choice of modelling language based
  on the characteristics of the transition system under description,
  rooted in our observations of the differences and similarities
  between the languages with respect to our comparison criteria from
  the several case studies we carried out.
\end{itemize}

We categorize our comparison criteria into three main categories of
control modelling, data modelling, and modularity; discussed in detail
in Chapter~\ref{chp:control}, Chapter~\ref{chp:data}, and
Chapter~\ref{chp:mod} respectively, and summarized in
Table~\ref{tab:control/summary}, Table~\ref{tab:data/summary}, and
Table~\ref{tab:mod/summary} respectively, repeated below.  Further, we
compare the languages according to these criteria using several case
studies presented in Chapter~\ref{chp:cs}, and present recommendations
for the choice of declarative modelling language in
Chapter~\ref{chp:recs} language based on our experience carrying out
the case studies.

\begin{table*}[!h]
  \centering
  \captionsetup{font=small}
  \renewcommand\thetable{\ref{tab:control/summary}}
  \caption{Summary of control aspects of languages}
  \input{table/control-summary}
  \vspace*{1em}
  \renewcommand\thetable{\ref{tab:data/summary}}
  \caption{Summary of data aspects of languages}
  \input{table/data-summary}
  \vspace*{1em}
  \renewcommand\thetable{\ref{tab:mod/summary}}
  \caption{Summary of modularity aspects of languages}
  \input{table/mod-summary}
\end{table*}
\addtocounter{table}{-1}
\pagebreak

If we were creating an \emph{ideal} declarative modelling language, it
would include the following features and characteristics:
\begin{itemize}
\item a more declarative rather than imperative \textbf{expression}
  style, so as to stay true to the declarative behavioural modelling
  paradigm;
\item a wide range of \textbf{constructors} for composite units of
  data, as well as \textbf{multiplicities} for the constructors, with
  constructors for commonly used data units such as total, partial,
  and surjective functions built as syntactic sugar on top of
  multiplicities; as well as support for declaring \textbf{subtypes};
\item implicit representation for the \textbf{transition relation} by
  default for convenience, along with options to supplement or tweak
  the transition relation by more knowledgeable modellers;
\item improved tool support for helping the modeller find the sources
  of \textbf{inconsistency} in their model;
\item notion of \textbf{control state hierarchy} or similar constructs
  to decompose a transition system from a control modelling point of
  view into \textbf{subtransition systems}, each having their own
  (uniquely addressable) \textbf{namespace};
\item \textbf{typechecking} done as a separate pass, with typing
  constraints restricting the reachable snapshot space for improving
  performance, as opposed to treating typing constraints as properties
  checked with other invariants during the main analysis;
\item dealing with the \textbf{frame problem} in a way that is both
  convenient and avoids the issue of under-specification as seen in
  \alloy{} models, by either adding implicit constraints that keep
  unconstrained variables in a transition unchanged (as \dash{} does),
  or by requiring that every variable either be constrained or marked
  as unchanged using a special keyword (as \tla{} does); and
\item a flexible module system for data decomposition of models across
  multiple files, with each file hosting one or more
  \textbf{parameterized} modules that support selective
  \textbf{import} and \textbf{export} of identifiers.
\end{itemize}

\dash{} already has several of the above characteristics and features,
and we believe it has potential to become even closer to our described
ideal language by implementing the missing features and enhancements
from the above list.


In future work, we would like to extend our comparison to include
other similar languages and also extend our comparison criteria to
include an examination of tool support, which would address issues
such as performance, robustness, and ease of understanding
counterexamples.


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