% recommendations.tex --- language choice recommendations -*-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{Recommendations}
\label{chp:recs}

Based on our experience modelling the case studies presented in
Chapter~\ref{chp:cs} across the languages, in this chapter we present
more general recommendations for the choice of declarative modelling
language depending on the characteristics of the system under
description.

For models where fine control over the \textbf{transition relation} of
the transition system by the modeller is desired, \alloy, \tla, and
\asmetal{} are the most suitable languages, as they use an explicit
representation for the transition relation.

For modelling control-oriented systems where the relevance of the
\textbf{transitions} and their being enabled can be captured using
(potentially hierarchical) \textbf{control states}, we believe \dash{}
is a great choice for the modelling language.  While our case studies
showed that these systems can be modelled in any of the languages we
studied, we found \dash's \textbf{control state hierarchy} and
\textbf{events} to enable the modeller to model control-oriented
systems in an abstract, concise, and convenient way.  Also, \dash's
per-\dashcode{state} \textbf{namespaces} allow separation of names,
while still allowing global communication between different states
through a clear interface of fully-qualified names.

A common source of mistakes and unexpected behaviour bugs in \alloy{}
models is the under-specification of behaviours, relating to the
\textbf{frame problem}.  In \alloy, any variable not constrained in a
transition may freely change from the source to the destination
snapshot.  This can result in the model exhibiting strange behaviours
that could be especially hard to debug.  \tla{}, also a highly
declarative language, addresses this problem by requiring that every
transition constrain every snapshot variable, either explicitly using
primed and unprimed names of variables, or denoting the unchanged
variables using the \tlacode{UNCHANGED} keyword.  For this reason, we
believe \tla{} is a better choice than \alloy{} for modelling larger
data-oriented models, as it eliminates an entire common, hard-to-debug
class of problems using static syntactic checks.

For models where a clear distinction between the system and its
surrounding environment is desired, \dash{} and \asmetal{} both
distinguish between \textbf{controlled} and \textbf{monitored}
variables.  \dash{} additionally supports environmental (monitored)
\textbf{events} as well, which are those that are fired exclusively by
the environment and not by any of the system's transitions.

For highly data-oriented systems, we found \B{} and \eventb's
extensive set of arrow \textbf{constructors} for various relational
and functional units of data to be powerful tools for writing terse
and concise descriptions of highly-constrained composite units of
data, both in \textbf{type signatures} and in formulas.  Although
\alloy/\dash{} using \textbf{multiplicities} and \tla/\pluscal{}
through the use of flexible and expressive \tla{} \textbf{expressions}
could describe the same set of constraints on data, \B/\eventb{} allow
this in a more convenient way.  We found \asmetal{} to be the least
declarative and least flexible in this regard.

As \B{} and \eventb{} are similar languages with the same roots, and
\eventb{} is a successor of \B, the choice between the two languages
may not be immediately obvious.  Compared to \B, \eventb{} is a
smaller and much simpler language.  While \B{} supports several kinds
of relationships between machines, in \eventb{} the only kinds of
relationships are a machine importing one or more contexts, and a
machine refining another machine.  Further, \B{} has \textbf{built-in}
constructors for sequences and trees while \eventb{} does not.  On the
other hand, \B{} only has one arrow \textbf{constructor} for declaring
a relation, whereas \eventb{} has three additional arrows for
constructing specific kinds of relations; namely total, surjective,
and total surjective relations.  Further, \eventb{} has support for
declaring \textbf{subtypes} and partitioning a set into multiple
disjoint subsets, whereas \B{} does not.

\pluscal{} brings to the table the power and expressiveness of \tla's
\textbf{expressions}, wrapped in a semantics geared more towards
modelling multi-process concurrent and parallel algorithms, with
additional \textbf{well-formedness} safeguards that make certain
classes of bugs unrepresentable in a valid model in the language.
\asmetal, too, has semantics for modelling multi-threaded systems.

With respect to modularity, \eventb, \dash, and \pluscal{} allow
\textbf{data decomposition} of a model across multiple files.  \B,
\alloy, \tla, and \asmetal{} additionally allow \textbf{control
  decomposition} of a model into subtransition systems across multiple
files.

Although we observed subtle and noteworthy differences across the
languages with respect to the \textbf{stuttering} criterion, it did
not seem to affect the modelling of our case studies noticeably.
Similarly, the representation of \textbf{snapshot variables},
\textbf{initialization}, \textbf{constants}, \textbf{scopes}, and
\textbf{syntax overloading} did not have a significant effect on our
process of modelling the case studies.  However, these criteria are
useful to acknowledge, helping the modeller see the differences
between the languages with respect to these criteria, when moving from
one modelling language to the next.


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