% data.tex --- data modelling aspects of languages -*-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{Data Modelling}
\label{chp:data}

In this chapter, we discuss in depth the description of the data
aspects of models in each of the declarative modelling languages
examined in this thesis.  This data is constrained in the guards and
actions of transitions and in the invariants of the model.  We first
lay out the terminology we use in this chapter in
Section~\ref{sec:data/terminology}.  In
Section~\ref{sec:data/primitives} and Section~\ref{sec:data/cons-mult}
we discuss the primitives and constructors of composite units of data
in each language respectively.  In Section~\ref{sec:data/expr} we
discuss the expression syntax of each language and notable differences
between them.  Section~\ref{sec:data/events} discusses the notion of
events and how they can be modelled in modelling languages that do not
have that notion.  Section~\ref{sec:data/constants} discusses the
declaration of constants across the languages.
Section~\ref{sec:data/wf-typechecking} discuses well-formedness
conditions and typechecking of type signatures in each language.  In
Section~\ref{sec:data/scopes} we look at how the sizes of the sets
used in the models is set in each programming language.  Finally, in
Section~\ref{sec:data/miss-feats} we mention some missing features and
constructs that are absent in all the languages we studied.
Table~\ref{tab:data/summary} summarizes the differences in the data
aspects of the selected declarative modelling languages with respect
to modelling transition systems.

\begin{table}[htbp]
  \centering
  \caption{Summary of data aspects of languages}
  \label{tab:data/summary}
  \input{table/data-summary}
  \begin{minipage}{0.9\textwidth}
    \footnotesize
    \vspace{0.5em}\textit{Legend:}\vspace{0.25em}

    $\mathbb{Z}$:~Integers, $\mathbb{N}$:~Naturals,
    $\mathbb{N}_1$:~Naturals excluding zero, $\mathbb{R}$:~Reals,
    $\mathbb{C}$:~Complex numbers, $\mathbb{B}$:~Booleans.

    \textbf{fun}:~function, \textbf{rel}:~relation,
    \textbf{rec}:~record, \textbf{seq}:~sequence,
    \textbf{ord}:~ordering, \textbf{str}:~string,
    \textbf{char}:~character.
  \end{minipage}
\end{table}


\setcounter{section}{-1}
\section{Terminology}           % section zero
\label{sec:data/terminology}

The following are the terminology we use to describe the
data-related characteristics of declarative modelling languages.

\begin{itemize}
\item \textbf{Primitives:} are the smallest unit of data in a
  language, usually consisting of scalars and sets.
\item \textbf{Constructors:} are operators that create
  \textbf{composite units of data} from primitives or other composite
  data units.  For example, functions, relations, and records are
  constructors.  Constructors include \textbf{multiplicities}, which
  impose constraints that limit the values in the composite data being
  constructed.
\item \textbf{Built-ins:} of a language are the names of particular
  primitives or particular composite data units that are part of the
  syntax of the language or part of its standard libraries, and are
  available to the modeller without declaration in the model.
\item \textbf{Standard library:} of a language is the collection of
  one or more modules that are distributed with the tool support for
  the language, and include the built-ins and utility functions that
  may or may not be hard-coded and/or built into the language.
\item \textbf{Event:} denotes an occurrence at a moment in time.  In
  some languages, an event may be used as a precondition of a
  transition.  Events are often helpful in describing the abstract
  behaviour of reactive systems.
\item \textbf{Constant:} is a mapping from a name to a value, either a
  primitive or a composite data unit.  In contrast to a snapshot
  variable, a constant retains its value throughout all of the
  transitions of the transition system.  Not all of the languages
  distinguish between variables and constants.
\item \textbf{Type signature:} is syntax in a language to denote the
  kind of object contained in a snapshot variable, constant, or
  quantified variable as either a primitive or a composite data unit.
\item \textbf{Typechecking:} refers to checking that the constraints
  expressed in the type signatures are consistent with the use of the
  data in the formulas.
\item \textbf{Subtype:} is the name of a subset of values of another
  set that can be used in a type signature.
\item \textbf{Scope:} is the size of a set of objects; \emph{i.e.}
  the total number of distinct elements it contains.
\end{itemize}


\section{Primitives}
\label{sec:data/primitives}

In this section, we examine the primitives of each language.
Primitives are the smallest unit of data in a language, and usually
consist of scalars and sets.  In declarative modelling languages,
similar to programming languages, scalars are objects like numbers,
Booleans, strings, or a user-declared object.  A set is an unordered
collection of distinct objects, and is itself an object as well.  Sets
are a critically important part of declarative modelling languages,
and are the fundamental building blocks for more complex units of
data.  We also examine whether each language supports subtypes,
indicating whether or not it is possible to declare a set that is a
subset of another set and can be used in a type signature.
%% Natural numbers can be axiomatized using sets and functions
%% according to the Peano axioms, as shown in the \tlacode{Peano}
%% \tla{} module from~\cite{DBLP:books/aw/Lamport2002}.

\input{figure/data-primitives}

The primitives of \B{} consist of scalars and sets.  In \B, sets are
declared in the \bcode{SETS} section of the machine, and are of two
kinds: enumerated and deferred.  An enumerated set is one where its
elements are listed in the declaration of the set, whereas the
declaration of a deferred set does not include a list of its elements.
\B{} does not support subtypes, but they can be modelled using
membership predicates.  For example, a parent set \bcode{A} is
declared on line~\ref{lbl:data/b-parent}, and a constant predicate
\bcode{isC} is declared and constrained on
lines~\ref{lbl:data/b-const1} and \ref{lbl:data/b-const2} to model the
subtyping.  \bcode{isC} must be used as a precondition for any use of
the \bcode{R1} relation.  To declare a snapshot variable to be a
scalar from a given set, we add a type signature using the `\bcode{:}'
set element operator and the name of the set, as on
line~\ref{lbl:data/b-scalar} of the \B{} code block in
Figure~\ref{fig:data/primitives}.  To declare a snapshot variable
whose value is a set of elements from a given set, we use the
\bcode{POW} operator (for powerset) in the type signature, as on
line~\ref{lbl:data/b-pow}.

The primitives of \eventb{} consist of scalars and sets.  Sets are
declared in the \eventbcode{SETS} section of a \emph{context},
separate from the \emph{machine} definition.  There are two kinds of
sets in \eventb: carrier and enumerated.  A carrier set can be
declared simply by adding its name to the \eventbcode{SETS} section of
the context.  To declare an enumerated set, in addition to adding its
name to the \eventbcode{SETS} section, we list its elements under the
\eventbcode{AXIOMS} section, using the \eventbcode{partition}
operator.  The first argument to \eventbcode{partition} is the name of
the set, and subsequent arguments are disjoint sets of elements, as on
line~\ref{lbl:data/eventb-part} of the \eventb{} code block in
Figure~\ref{fig:data/primitives}.  Declaring a subtype in \eventb{} is
also done using the \eventbcode{partition} operator by providing the
name of the parent set as the first argument, and the names of the
children as subsequent arguments, as on
line~\ref{lbl:data/eventb-part-subtype}.  To declare a snapshot
variable to be a scalar from a given set, we add a type signature
using the `\eventbcode{:}' set element operator and the name of the
set, as on line~\ref{lbl:data/eventb-scalar}.  To declare a snapshot
variable whose value is a set of elements from a given set, we use the
\eventbcode{POW} operator (for powerset) in the type signature, as on
line~\ref{lbl:data/eventb-pow}.

The primitives of \alloy{} consist only of sets, and there are no
scalars in \alloy.  A ``scalar'' in \alloy{} is represented using a
singleton set.  For instance, \alloycode{5} is really syntactic sugar
for the singleton set \alloycode{\{5\}}.  Sets are declared using the
\alloycode{sig} keyword (for signature).  If formulas are added as
`signature facts' immediately following a signature, they are
implicitly quantified over the elements of the signature.  Subset
signatures can be declared using the \alloycode{in} keyword.  Note
that multiple subsets declared using \alloycode{in} may not
necessarily be disjoint.  To declare disjoint subsets of a set, the
\alloycode{extends} keyword can be used, as on
line~\ref{lbl:data/alloy-subtype} of Figure~\ref{fig:data/primitives}.
Enumerated sets can be declared using the \alloycode{enum} keyword, as
on line~\ref{lbl:data/alloy-enum}, which is syntactic sugar for
declaring a parent \alloycode{abstract sig}, and declaring its
elements as \alloycode{one sig} singleton sets, each of which
\alloycode{extends} the parent set.  To declare a snapshot variable
whose value is an element of a given set, we use the \alloycode{one}
multiplicity keyword in the type signature, as on
line~\ref{lbl:data/alloy-v2}.  To declare a snapshot variable whose
value should be a set of elements from a given set, we use the
\alloycode{set} multiplicity, as on lines~\ref{lbl:data/alloy-v1} and
\ref{lbl:data/alloy-evs}.  \dash's \dashcode{state} syntax is
translated to an \alloy{} signature, and the above statements about
\alloy{} apply to \dash{} as well.

The absence of real scalars in \alloy{} has various implications.  On
the one hand, everything being sets implies having a simpler,
non-overloaded set of operators that can readily be applied to various
objects in the language.  On the other hand, it means there are some
unusual characteristics of the language.  For instance, in \alloy{}
Boolean values are not scalars, and even though formulas have Boolean
values, variables never do~\cite[p.~137]{Jackson:2012:SAL:2141100}.
The reason for the absence of Boolean-valued expressions is that their
presence would render an expression like \alloycode{not p} ambiguous
when \alloycode{p} contains zero or more than one Booleans.  Instead,
Boolean-like valuations can be mimicked using the \alloycode{Boolean}
set from the \alloycode{util/Boolean} module of \alloy's standard
library.

The primitives of \tla{} and \pluscal{} consist of scalars and sets.
Sets can be declared either as constants in the \tlacode{CONSTANTS}
section of a module, or as a predicate definition whose right-hand
side is a set-valued constant expression.  To declare a set to be a
subset of another set, we can use the \tlacode{SUBSET} keyword.  To
declare a snapshot variable whose value is an element from a given
set, we add a type signature using the `\tlacode{\\in}' set membership
operator and the name of the set, as on line~\ref{lbl:data/tla-scalar}
of the \tla{} code block in Figure~\ref{fig:data/primitives}.  To
declare a snapshot variable to be a scalar from a given set, we can
either use the powerset keyword \tlacode{SUBSET} along with the set
membership operator `\tlacode{\\in}', or just use `\tlacode{\\subseteq}'.
Line~\ref{lbl:data/tla-subset} shows an example of the former.

In \asmetal, the primitives are scalars and sets.  Sets are declared
using the \asmcode{abstract domain} keywords, as on
lines~\ref{lbl:data/asmetal-A} and \ref{lbl:data/asmetal-B} of the
\asmetal{} code block in Figure~\ref{fig:data/primitives}.  To declare
elements for a set, one can either change the set declaration from
\asmcode{abstract domain} to \asmcode{enum domain} and list the
enumeration elements as on line~\ref{lbl:data/asmetal-event}, or
declare the elements using the \asmcode{static} keyword, as on
lines~\ref{lbl:data/asmetal-c1} and \ref{lbl:data/asmetal-c2}.  In
\asmetal, a subtype is declared using the \asmcode{subsetof} keyword,
as on line~\ref{lbl:data/asmetal-subsetof}.  To declare a snapshot
variable to be a scalar from a given set, we add a type signature with
the name of the set, as on line~\ref{lbl:data/asmetal-v2}.  To declare
a snapshot variable whose value is a set of elements from a given set,
we use the \asmcode{Powerset} keyword, as on
lines~\ref{lbl:data/asmetal-evs} and \ref{lbl:data/asmetal-v1}.

Each language consists of some built-in sets and scalars that are
elements of those sets.  In \B{} and \eventb, the built-ins are
Booleans, naturals, and integers.  \B{} additionally has strings.
\tla{} and \pluscal{} have Booleans, naturals, integers, reals, and
strings.  In \asmetal, the built-ins are Booleans, naturals, integers,
reals, complex numbers, characters, and strings.  \alloy{} and \dash{}
have integers and Booleans, but the names typically used for scalars
in these sets are actually singleton sets.  \alloy{} also has strings,
but currently the only elements in the set of strings are the string
literals used in the current model, and the analyzer cannot find
arbitrary instances for strings like it can do for other sets.


\section{Constructors and Multiplicities}
\label{sec:data/cons-mult}

In this section, we examine constructors and multiplicities across the
languages.  Constructors are operators that create composite units of
data from primitives or other composite data units.  Multiplicities in
a constructor impose constraints that limit the values in the
composite data.  Constructors appear in type signatures.  We also
discuss how formulas can be used to constrain composite units of data
in many languages, but we do not consider these formulas to be
constructors because they are not part of a type signature, and a
formula can do much more than constrain the form of one kind of data.
Figure~\ref{fig:data/cons-mult} helps compare the languages with
respect to constructors and multiplicities using an equivalent
snapshot declaration across the languages.

\input{figure/data-cons-mult}
\input{figure/data-records}

The composite units of data in \B{} are functions, relations, and
records, each with various pre-defined operations available to the
modeller.  Functions can be created using the ``arrow'' operators
built into the \B{} language.  These arrow operators are: $\pfun$
(partial functions), $\tfun$ (total functions), $\pinj$ (partial
injections), $\tinj$ (total injections), $\psur$ (partial
surjections), $\tsur$ (total surjections), and $\tbij$ (total
bijections).  Relations can be created using the $\rel$ arrow
operator.  The \B{} code block in Figure~\ref{fig:data/cons-mult}
shows examples of using some of these operators.
Line~\ref{lbl:data/b-f1} shows a total function \bcode{f1}, and
line~\ref{lbl:data/b-f2} shows a surjective function \bcode{f2}.
\bcode{R1} on line~\ref{lbl:data/b-R1} is a binary relation, with the
additional 1-to-2 constraint imposed in a formula on
lines~\ref{lbl:data/b-mult-start}\nd\ref{lbl:data/b-mult-end}.
\bcode{s1} is declared to be a sequence of \bcode{A}'s, as on
line~\ref{lbl:data/b-s1}.  Since functions and relations in \B{} are
both represented as sets of pairs, they can also be created using the
set literal notation along with the $\mapsto$ (``maplet'') pair constructor.
In addition to functions and relations, \B{} also has records with
named fields, as shown in the \B{} code block of
Figure~\ref{fig:data/records}.  The \bcode{struct} operator denotes
the set of records matching the given field signatures, and is used in
the type signature when declaring a new record.  A new instance of a
record can be created using the \bcode{rec} operator.  Built-in
constructors in \B{} include (zero-indexed) sequences and trees.

\eventb's composite units of data are functions and relations.
\eventb, similar to \B, has various arrow operators for constructing
functions and relations.  In addition to all of \B's functions and
relations arrows mentioned above, \eventb{} has three additional
arrows for constructing specific kinds of relations.  Namely, $\trel$
(total relations), $\srel$ (surjective relations), and $\strel$ (total
surjective relations).  In Figure~\ref{fig:data/cons-mult},
line~\ref{lbl:data/eventb-f1} shows a total function \eventbcode{f1},
and line~\ref{lbl:data/eventb-f2} shows a surjective function
\eventbcode{f2}.  \eventbcode{R1} on line~\ref{lbl:data/eventb-R1} is
a binary relation, with the additional 1-to-2 constraint imposed on
lines \ref{lbl:data/eventb-R1-start}\nd\ref{lbl:data/eventb-R1-end}.
Since \eventb{} does not have a built-in sequence constructor, we can
use a partial function from \eventbcode{NAT} to \eventbcode{A} to
represent \eventbcode{s1} as a sequence of \eventbcode{A}'s, as on
line~\ref{lbl:data/eventb-s1}.

\tla{} does not have type signatures, and thus no constructors; but
composite units of data can be specified using \tla{} formulas.  The
composite data units in \tla{} are functions and relations.  \tla{}
also supports records, which are built on top of functions.  The
\tla{} code block of Figure~\ref{fig:data/records} shows an example of
declaring and using \tla{} records.
Lines~\ref{lbl:data/tla-ops-start}\nd\ref{lbl:data/tla-ops-end}
showcase formulas that constrain data to be of a certain composite
form.  For instance, we define \tlacode{SurFun(a, b)} to return the
set of all surjective functions from \tlacode{a} to \tlacode{b},
\tlacode{f1} is required to be a total function from \tlacode{A} to
\tlacode{B} (line~\ref{lbl:data/tla-f1}), \tlacode{f2} a surjective
function from \tlacode{A} to \tlacode{B} (line~\ref{lbl:data/tla-f2}),
\tlacode{R1} a binary relation between \tlacode{C} and \tlacode{B}
(line~\ref{lbl:data/tla-R1}) and constrained to be a 1-to-2 relation
(line~\ref{lbl:data/tla-R1-1to2}), and \tlacode{s1} a sequence of
\tlacode{A}'s (line~\ref{lbl:data/tla-s1}).

\asmetal's primary composite data unit is relations, created using the
\asmcode{Powerset} and \asmcode{Prod} constructors for creating sets
and tuples respectively.  Although \asmetal{} has a dedicated function
constructor arrow that can be used in type signatures, it is not
always be the best representation for a function, since the possible
operations on a function are limited.
Lines~\ref{lbl:data/asmetal-fr-start}\nd\ref{lbl:data/asmetal-fr-end}
show the declaration of three relations, which are constrained by the
invariants on lines~\ref{lbl:data/asmetal-inv-start} \nd
\ref{lbl:data/asmetal-inv-end}.  The \asmcode{f1} total function from
\asmcode{A} to \asmcode{B} is defined as a set of pairs, where the set
elements satisfy the constraint laid out in \asmcode{isfun}: the set
of elements from \asmcode{f1}'s domain that map to two different
elements in \asmcode{f1}'s range must be empty.  The surjective
function \asmcode{f2} from \asmcode{A} to \asmcode{B} is defined as a
set of pairs, where the set elements satisfy the constraint laid out
in \asmcode{issurfun}: first, \asmcode{f2} must already be a function;
and additionally, \asmcode{f2}'s codomain must match the set of
elements mapped to by \asmcode{f2} (\emph{i.e.} every element of
\asmcode{f2}'s codomain must be mapped to by an element in
\asmcode{f2}'s domain).  The 1-to-2 binary relation \asmcode{r1} from
\asmcode{C} to \asmcode{B} is defined as a set of pairs, where the set
elements satisfy the constraint laid out in \asmcode{is1to2}: each
element of \asmcode{r1}'s domain must map to two different elements
from its range.  Lastly, \asmcode{s1} is declared to be a sequence of
\asmcode{A}'s.

\alloy's composite unit of data is relations, created using the
`\alloycode{->}' arrow constructor.  As relations are ubiquitously
used in \alloy{} models, \alloy{} provides convenient dot join
`\alloycode{.}' and box join `\alloycode{[]}'
operators~\cite[p.~57-62]{Jackson:2012:SAL:2141100}, which resemble
record field access and array indexing respectively.  Somewhat hidden
to users of \alloy{} is that \alloy{} does not actually have record
objects; and though signatures and their fields mimic records and
record fields, signatures are actually sets (\emph{i.e.} unary
relations) and signature fields are top-level identifiers themselves,
each a relation mapping their parent signature to the field's value
from the set declared in the field's type signature.  This can be
confusing to new users trying to understand the output of the analysis
(\emph{e.g.}  counterexamples for model checking), when a variable
name is actually a relation.

\alloy{} provides a range of \textbf{multiplicity constraints} within
its type signatures.  A multiplicity constraint is a constraint
limiting the number of elements in the range associated with elements
in the domain.  \alloy{} has four multiplicity keywords, \textbf{set}
(any number), \textbf{lone} (zero or one), \textbf{one} (exactly one),
and \textbf{some} (one or more).  When the type signature is a set
(\emph{i.e.} unary relation), it can be prefixed with a multiplicity
keyword as in ~\alloycode{x: m e},~ where \alloycode{x} is the set
being constrained, \alloycode{m} is the multiplicity keyword, and
\alloycode{e} is the set-valued bounding expression.  The default
multiplicity for a set-valued type signature is \emph{one}.  Thus, if
the multiplicity keyword \alloycode{m} is omitted, ~\alloycode{x: e}~
makes \alloycode{x} a `scalar' (\emph{i.e.} a singleton set).  Here is
the meaning of the other multiplicities on sets:
\begin{table}[h]
  \centering
  \label{tab:data/cons-mult/set}
  \input{table/data-cons-mult-set}
\end{table}
\vspace*{-0.75em}

When the type signature is a relation (of arity greater than one), it
\emph{cannot} be prefixed with a multiplicity keyword.  Multiplicity
keywords may appear around the `\alloycode{->}' arrow constructor, as
in ~\alloycode{x: e1 m->n e2}, where \alloycode{m} and \alloycode{n}
are multiplicity keywords, and \alloycode{e1} and \alloycode{e2} are
sets.  The expression ~\alloycode{x: e1 m->n e2}~ means the relation
\alloycode{x} is constrained to map each member of \alloycode{e1} to
\alloycode{n} members of \alloycode{e2}, and to map \alloycode{m}
members of \alloycode{e1} to each member of \alloycode{e2}.
\alloycode{e1} and \alloycode{e2} need not be sets (unary relations)
or even named relations; and they may be any arbitrary expressions.
The above description is generalized by replacing `member' with
`tuple'.  Below are examples of some commonly-used multiplicities on
relations:
\begin{table}[h]
  \centering
  \label{tab:data/cons-mult/rel}
  \input{table/data-cons-mult-rel}
\end{table}
\vspace*{-0.75em}

\dash{} has the same constructors and multiplicities as \alloy.

Having considered constructors across the languages, we now briefly
touch on the names of built-ins in each language.  \B's built-ins
include sequences and trees.  \alloy's built-ins include a constructor
that imposes linear total order on other sets, (zero-indexed)
sequences, strings, and graphs.  \dash{} shares \alloy's built-ins.
\tla's built-ins include composite data units like records, bags, and
(one-indexed) sequences, from \tla's standard modules.  Recent \tlc{}
versions override the definitions from most of these standard modules
in the host language (Java) for improved efficiency.  \pluscal{}
shares \tla's built-ins.  \asmetal's
\texttt{StandardLibrary.asm}~\cite{standardlibraryasm} contains a
large number of built-ins such as bags, maps, products (tuples or
pairs), and (zero-indexed) sequences.


\section{Expressions}
\label{sec:data/expr}

In this section, we discuss briefly the syntax of each language for
writing formulas, and the operators and constructs provided in each
language for writing expressions.  Since all of the languages are
based on first-order logic and set theory, their expressions are
reasonably similar in succinctness.  They all provide operations to
create and modify primitives and composite data units, such as sets,
relations, and functions.  In the following, we discuss only the
interesting differences in the expression syntax of each language.

The expressions of \B{} and \eventb{} have a more imperative style
than declarative, in that initialization and changing of variables are
primarily done using the `$:=$' assignment operator.  Additionally,
both languages have a nondeterministic assignment operator `$:\in$' for
setting the value of a variable to a nondeterministically-chosen
element from a set.  However, as declarative modelling languages, both
\B{} and \eventb{} support changing a variable in a declarative style
using the `$:\!(\,)$' and `$:\!|$' operators respectively, for when a
regular assignment is not flexible enough and we would like to
declaratively constrain the value of a variable.  In \B, assignments
statements are combined using the `\bcode{||}' and `\bcode{;}'
operators, for parallel and sequential assignments respectively.
Since both relations and functions in \B{} and \eventb{} are
represented as sets of pairs, in addition to the arrow operators
described earlier they can also be created using the set literal
notation along with the `$\mapsto$' (``maplet'') pair constructor.

\alloy{} and \dash{} have expression languages that include set
operators mixed with first-order logic.  Models typically make
extensive use of the join operator because every unit of data is a
relation.

\tla{} has a small number of essential operators for conveniently
working with sets and functions, \tla{} also has the a
\tlacode{CHOOSE} operator, \tlacode{IF..THEN..ELSE} expressions,
\tlacode{CASE} expressions, \tlacode{LET..IN} expressions, and
\tlacode{LAMBDA}.  Even though \tla{} is a very small language, one
can easily define new custom operators .  For instance, on
line~\ref{lbl:data/tla-range} of Figure~\ref{fig:data/cons-mult} we
define the \tlacode{Range} operator which is absent in \tla, to return
the range of a function.  \tla{} uniquely supports recursive and
higher-order operators, which take other operators as arguments.

The \asmetal{} language rarely uses symbols and most operators have
long-form textual names.  \asmetal's built-in units of data are
opaque, in that operations defined on primitives cannot be applied to
composite data units.  This means that the operations on the built-in
composite data units are limited by what is currently implemented in
the tool support for the language.  As of now, in \asmetal{} sets are
the most flexible/featureful construct in the language, and the
modeller may need to fall back to using them as the underlying
representation of a data unit if the built-in data unit provided by
the language does not include the operations they need.  For instance,
few operations are available for the built-in function constructor in
\asmetal.  Since an \asmetal{} function cannot be treated as a set of
tuples, the set operations are not defined on functions.  As such,
when more flexibility is needed, \emph{e.g.} for writing formulas for
dealing with a function as a whole, the built-in function constructor
cannot be used, and instead the more flexible `set of pairs'
representation must be used.


\section{Events}
\label{sec:data/events}

An event denotes an occurrence at a moment in time, such as a button
being pressed or a card swiped.  An event may be used as a
precondition of a transition.  Among the declarative modelling
languages studied in this work, events are a feature unique to \dash.
A statechart event in \dash{} can be added to a snapshot using the
\dashcode{event} keyword, as on lines~\ref{lbl:data/dash-ev1} and
\ref{lbl:data/dash-ev2}.  The semantics of events in \dash{} is that
they persist as long as transitions are enabled, allowing multiple
transitions to be taken in response to an input from the environment.

To model events in languages other than \dash{} which do not have a
notion of events built into them, we use regular snapshot variables.
There are several possible approaches for keeping track of the
triggered state of the events of a model.  One approach is to use one
snapshot variable for each event, with the value of each variable
drawn from a two-element set, for whether or not the event is
currently triggered.  A language's built-in Boolean set or another
two-element set with more descriptively-named elements are good
candidates for the type signature of this snapshot variable.  Another
approach is to declare an enumerated set with one element per event.
Then, declare one set-valued snapshot variable whose value is a subset
of the enumerated set of events, with each currently triggered event
being a member of this set.  Constraints must be added to specify the
desired semantics of events, such as whether the event persists.
Figure~\ref{fig:data/primitives} shows exemplars using this approach
across the languages (besides \dash, which has built-in support for
events).


\section{Constants}
\label{sec:data/constants}

A constant is a mapping from a name to a value, either a primitive or
a composite data unit.  Constants retain their value throughout all of
the transitions of the transition system.
Figure~\ref{fig:data/primitives} shows examples of declaration of
constants across the languages.  In \B, constants are declared under
the \bcode{CONSTANTS} section of a machine, and are further
constrained in the \bcode{PROPERTIES} section.  In \eventb{} constants
are declared under the \eventbcode{CONSTANTS} sections of a context,
and are further constrained in the \eventbcode{AXIOMS} section of the
context.  The \B{} and \eventb{} code blocks in
Figure~\ref{fig:data/primitives} show examples of this.  In \asmetal,
constants are declared under the \asmcode{signature} section after
snapshot variables, using the keyword \asmcode{static}, as shown on
lines~\ref{lbl:data/asmetal-c1} and \ref{lbl:data/asmetal-c2} of the
\asmetal{} code block in Figure~\ref{fig:data/primitives}.  A
constant may be assigned a specific value under the
\asmcode{definitions} section, as on
line~\ref{lbl:data/asmetal-c2-def}.

\alloy{} and \dash{} do not have a keyword or construct for constants.
Thus, a ``constant'' is declared like a regular variable as a field of
a signature, and must be constrained to have the same value in all
snapshots.  To avoid confusing constants with snapshot variables, we
declare them in a separate signature, conventionally named
\alloycode{Const}.  In \alloy, further constraints, such as having the
constant be a certain literal value, can be imposed using either a
fact or a predicate.  In \dash, these constraints are added in an
\dashcode{invariant} block inside a \dashcode{state}.
Lines~\ref{lbl:data/alloy-const-start}\nd\ref{lbl:data/alloy-const-end}
and \ref{lbl:data/dash-const-start}\nd\ref{lbl:data/dash-const-end} of
the \alloy{} and \dash{} code blocks of
Figure~\ref{fig:data/primitives} show examples of constant
declarations in \alloy{} and \dash; and lines
\ref{lbl:data/alloy-const-fact} and \ref{lbl:data/dash-const-inv} of
the \alloy{} and \dash{} code blocks show an example of a constraint
being imposed on the constant \alloycode{c2} using a signature fact
and an invariant in \alloy{} and \dash{} respectively.

In \tla{} and \pluscal, constants are declared under the
\tlacode{CONSTANTS} section of the module.  For model checking with
\tlc, every constant must be constrained in the ``Model Overview''
page of the model in the \tla{} toolbox.  A constant can be
constrained using either an ``ordinary assignment'' (any valid \tla{}
expression that can be assigned to a variable), or can be constrained
to be a ``model value'' or a ``set of model values''.  In \tlc{}
terminology, a ``model value'' is a unique value equal only to itself.
Alternatively, if we use a predicate definition like \tlacode{c2 ==
  3}, we will not have to declare \tlacode{c2} as a constant under
\tlacode{CONSTANTS}, and every mention of \tlacode{c2} is replaced
with \tlacode{3} during analysis.  This works in both \tla{} and
\pluscal, and is similar to the practice of defining constants and
magic values in C programs using preprocessor macros.  Note that this
approach only yields a constant when the right-hand side expression is
a constant expression, such as an integer literal, and for instance
\tlacode{c2 == CHOOSE cc \\in Integer: TRUE} would \emph{not} result in
\tlacode{c2} being a constant, since \tlacode{CHOOSE} is not
guaranteed to always return the same value each time it is evaluated.
The \tla{} and \pluscal{} code blocks of
Figure~\ref{fig:data/primitives} show an example of the former and
latter method respectively.


\section{Well-formedness and Typechecking}
\label{sec:data/wf-typechecking}

Well-formedness is a condition under which a formula or expression is
valid in a formal language, and has a well-defined meaning.  In this
section, we investigate the notions of well-formedness across the
seven declarative modelling languages, and the constructs in each
language that help make it easier for modellers to find or avoid
mistakes in their models, such as use of type signatures and
typechecking.  In this section, we focus on static well-formedness
checking techniques, which include parsing and typechecking.  All the
languages studied in this work do basic forms of syntax checking when
parsing input models.

Typechecking is the process of checking whether the use of data in the
formulas conforms to the constraints expressed in the type signatures.
With respect to typechecking, the following two questions arise:
\emph{First}, does a language have type signatures?  The answer is
that \B, \eventb, \alloy, \dash, and \asmetal{} do have type
signatures, and \tla{} and \pluscal{} do not.  \emph{Second}, does a
language with type signatures have a separate typechecking pass from
other forms of analysis?  The answer to this question is yes; all of
the languages we studied that have type signatures also have a
typechecking pass separate from the main analysis (\emph{e.g.} model
checking).

In \tla, there are few well-formedness checks beyond the basic syntax
checking done by the parser.  \tla{} does not have type signatures, so
variable and constant declarations only consist of names.  Any typing
constraints must be stated with other invariants and are properties
checked to hold in every snapshot of the transition system during the
main analysis.  An example of such typing constraints is the
\tlacode{TypeOK} predicate defined on lines
\ref{lbl:data/tla-typeok-start}\nd\ref{lbl:data/tla-typeok-end} of
Figure~\ref{fig:data/cons-mult}.  In our experience, having to
manually add typing invariants in the absence of a typechecker can be
error-prone and can hinder the debugging experience, as the errors
arising from the violation of these typing constraints can result in
cryptic error messages.

Compared to \tla, \pluscal{} has a number of safeguards in place that
make certain classes of bugs syntactically invalid, thus allowing the
parser to catch them when the modeller asks for the \tla{} translation
of their \pluscal{} model~\cite{DBLP:conf/ictac/Lamport09}.  Examples
include mistakes such as multiple assignments to the same variable in
a transition, and having unreachable statements.  These are eliminated
by \pluscal's notion of \emph{labels}, and where they may or must
appear in the transition definition.  For the above two examples, the
former is prevented due to the rule that a variable may only be
assigned to once between any two labels in a \pluscal{} process, and
the latter is eliminated by the requirement that a label must be added
for any statement that follows a \pluscalcode{goto} or
\pluscalcode{return} statement.  For \pluscal{} models, typing
constraints can be added using the same approach as \tla{} described
earlier.

In \alloy, the only well-formedness checking is a kind of
typechecking.  Type signatures constrain the model's reachable
snapshot space.  There are two kinds of type errors in
\alloy~\cite{Jackson:2012:SAL:2141100, DBLP:conf/sigsoft/EdwardsJT04}:
\begin{enumerate}[noitemsep,topsep=2pt]
\item since \alloy's logic assumes each relation has one fixed arity,
  an expression resulting in relations of mixed arity is illegal; and
\item an expression that can be shown to be redundant itself or
  contain a redundant sub-expression, based on the declarations alone,
  is ill-typed.  A common example of this is an expression that is
  redundant due to being equal to the empty relation.
\end{enumerate}

The current implementation of \dash{} performs several well-formedness
checks in addition to \alloy's.  Currently, typechecking in \dash{} is
not as thorough as in \alloy, and some type errors will only be caught
in the generated \alloy{} model.  \dash's well-formedness checks are
as follows~\cite{serna2019}:
\begin{itemize}[noitemsep,topsep=2pt]
\item Every top level \dashcode{state} must be declared as
  \dashcode{conc} (error).
\item If a model has state hierarchy then there must be one default
  child state defined (error).
\item Either all children states at the same level of the hierarchy
  are concurrent or none at all (error).
%% \item Escaped content is not validated (warning).
\item Only snapshot variable declarations can be primed (error).
\item Monitored (\dashcode{env}ironmental) events cannot be generated
  in a transition (warning).
\item Monitored (\dashcode{env}ironmental) variables cannot be primed
  (error).
\item A transition action must constrain the next value of
  (non-\dashcode{env}) variables (error).
\item Elements in a state should have different name (not currently
  enforced).
\end{itemize}

Besides well-definedness conditions, \B{} and \eventb{} also use
typechecking to statically catch type errors like assigning a value
from a set to a variable with a type signature declaring a
different/incompatible set, and applying a function to an argument not
matching its type signature.  To ensure that models only contain
well-defined formulas, \B{} and \eventb{} rely on well-definedness
proof obligations.  These are formulas corresponding to conditions
that are expected to hold when performing certain actions, such as
integer division and function application, in order for the action to
be well-defined.  For example, division by zero is not well-defined,
and neither is applying a function to an element outside its domain.
In a theorem proving setting, these well-definedness conditions have
to be proven, along with other proof obligations.  In a model checking
or animation setting, ProB performs well-definedness checking during
constraint solving, model checking, or animating.  In \B, type
signatures are declared in the \bcode{INVARIANT} section along with
other invariants.  Similarly, type signatures in \eventb{} are
declared in the \eventbcode{INVARIANTS} section along with the other
invariants of the machine.

Type signatures in \asmetal{} are included along with each variable
declaration.  Further, the \asmetal{} grammar uses various syntactic
rules to distinguish between language elements:
\begin{itemize}[noitemsep,topsep=2pt]
\item name of (local) variables must start with a dollar sign
  (\asmcode{$});
\item enumerated set elements must start with two upper-case letters,
  followed by zero or more upper-case letters, underscores, or digits;
\item domain (set) names must start with an upper-case letter;
\item rule names must start with a lower-case `\asmcode{r}', followed
  by an underscore (\emph{i.e.} ``\asmcode{r_}'');
\item function names (including snapshot variables) must start with a
  lower-case letter, but \emph{not} start with the string
  ``\asmcode{r_}'' (to avoid confusion with rule names);
\item invariant names must start with the letters ``\asmcode{inv}''
  followed by an underscore (\emph{i.e.} ``\asmcode{inv_}''); and
\item natural numbers must have a `\asmcode{n}' suffix (\emph{e.g.}
  \asmcode{14n} is the natural literal for the number fourteen), and
  integers must not have a suffix (\emph{e.g.} \asmcode{13} is the
  integer literal for the number thirteen).
\end{itemize}

These syntactic rules allow the Asmeta parser to detect a variety of
errors statically during parsing, including some type errors that
would normally be caught by a typechecker rather than a parser.  For
example, (mis)using an integer where a natural number is expected, or
confusing an enumerated set element with the parent set or a variable.
The Asmeta typechecker in turn helps catch other ill-typed formulas
and errors like trying to calculate the sum of one and the empty set
(\asmcode{\{\} + 1}), or assigning a set to a variable previously
declared to be a string.


\section{Scopes}
\label{sec:data/scopes}

In this section, we look at the constructs in each of the declarative
modelling languages and/or their tool support provide for setting the
scope (size) of each of the sets used in the model.  None of the
languages studied in this work require specifying the scopes as part
of the model.  However, some of the languages allow the definition of
scopes to be part of the model.

In \asmetal, there is no default set size, and user-defined domains
and their elements must be explicitly stated if needed.  For instance,
a signature like ~\asmcode{abstract domain A}~ is sufficient for
declaring a new set \asmcode{A} and using it in the model, including
with a \asmcode{choose} rule.  However, the Asmeta Animator and
Simulator currently enter an infinite loop if we try to animate or
simulate a model without scopes for all sets.  To use the abstract
domain, we have to declare its elements.  For example,
~\asmcode{static a1: A} declares an element \asmcode{a1} in
\asmcode{A}, which is required to be distinct from another element
~\asmcode{static a2: A}~ in \asmcode{A}.  Alternatively, we could
either declare a new concrete domain that is a \asmcode{subsetof} the
abstract domain and specify elements for it and use it instead of
using \asmcode{A} directly; or, change \asmcode{A} into an enumerated
domain like ~\asmcode{enum domain A = \{AA1 | AA2\}}~.

For \B, the ProB animator and model checker requires that all deferred
sets to be given a finite cardinality.  This is done by adding to the
\bcode{PROPERTIES} section a \bcode{card(SETNAME) = n} predicate for
each deferred set \bcode{SETNAME}, or by adding to the
\bcode{DEFINITIONS} section a definition \bcode{scope_SETNAME ==
  m..n}; or alternatively \bcode{scope_SETNAME == n}, equivalent to
\bcode{1..n}.  For sets with no specified cardinality, a
\bcode{DEFAULT_SETSIZE=2} will be used.  To limit the scope of
implementable integers (\bcode{INT}) and naturals (\bcode{NAT} and
\bcode{NAT1}), we can add the definitions \bcode{SET_PREF_MININT == x}
and \bcode{SET_PREF_MAXINT == y} in the \bcode{DEFINITIONS} section to
set \bcode{MININT} to \bcode{x} and \bcode{MAXINT} to \bcode{y}, which
default to \bcode{-1} and \bcode{3} respectively.

As ProB integrates into Rodin (the tool support for \eventb), the
above descriptions about adding scopes to \B{} models mostly apply to
\eventb{} models as well.  The difference is that \eventb{} does not
have a \bcode{DEFINITIONS} section like \B{} does; so the only method
for setting specific sizes for carrier sets is by adding a
\eventbcode{card(SETNAME) = n} axiom for each carrier set
\eventbcode{SETNAME}.  The default set size, the default values of
\texttt{MININT} and \texttt{MAXINT}, and other ProB preferences may be
changed from the Rodin tool by going to the \texttt{Window} menu,
selecting \texttt{Preferences}, and clicking on \texttt{ProB} in the
left pane.

In \tla, the size of sets may be specified under the \tlacode{ASSUME}
section of a model using the \tlacode{Card} operator.  The cardinality
of the largest set that the \tlc{} model checker can handle is
\texttt{1000000} by default.  This can be changed using the
\texttt{-maxSetSize x} command-line option to set the value to
\texttt{x}, if using \tlc{} from the command-line.  When using the
\tla{} toolbox, the value can be changed by opening the \texttt{Model
  Overview}, clicking on \texttt{Additional TLC Options}, expanding
the \texttt{Parameters} section, and changing the option there.  The
upper bound for this option is Java's \texttt{Integer.MAX\_VALUE}.
The largest value for \tla's \tlacode{Int} and \tlacode{Nat} sets is
\texttt{Integer.MAX\_VALUE}, and the smallest value for \tlacode{Int}
is \texttt{Integer.MIN\_VALUE}.

In \alloy{} and \dash, scopes are upper bounds or exact sizes of sets,
and are specified for each \alloycode{run} or \alloycode{check}
command.  All top-level signatures have a default scope of
\alloycode{3}.  The two exceptions to this rule are the two special
\alloycode{Int} and \alloycode{seq} signatures, both of which have a
default scope of \alloycode{4}.  \alloycode{Int}'s scope is the
maximum bit-width for integers.  For example, a scope of \alloycode{6}
allows \alloycode{Int} to range from \alloycode{-32} to
\alloycode{+31}.  For \alloycode{seq}, the assigned scope is the
length of the largest allowed sequence.  For example, a scope of
\alloycode{5} on \alloycode{seq} allows sequences of up to
\alloycode{5} elements.  Given a predicate \alloycode{x} and an
assertion \alloycode{y}, in its simplest but still useful form, a
command may look like ~\alloycode{run x}~ or ~\alloycode{check y},~
where no scope is specified and thus the above default scopes will be
used.  Note that this does not apply to the special signatures
\alloycode{Int} and \alloycode{seq}, and their scopes only change when
set explicitly, as explained below.  The following explanations apply
to both \alloycode{run} and \alloycode{check} commands, but we will
use \alloycode{run} in our examples.  Given the signatures
\alloycode{A}, \alloycode{B}, and \alloycode{C}, ~\alloycode{run x for
  5}~ sets the upper bound scope for \alloycode{A}, \alloycode{B}, and
\alloycode{C} to \alloycode{5}.  To use a different scope for some
signatures, we use the \alloycode{but} keyword: ~\alloycode{run x for
  5 but 4 B}~ sets the upper bound for every signature to
\alloycode{5}, except for \alloycode{B}, which is given an upper bound
of \alloycode{4}.  To force an exact scope for a specific signature,
we can use the \alloycode{exactly} keyword: ~\alloycode{run x for 5
  but 4 B, exactly 6 A}~ sets an upper bound of \alloycode{5} for all
signatures, except for \alloycode{B} which is given an upper bound of
\alloycode{4}, and \alloycode{A} which is forced to have an exact size
of \alloycode{6}.  We do not have to set a default scope for all
signatures in a command, as long as we explicitly specify the scope
for each signature or if \alloy{} can infer it implicitly.  For
details about the cases where \alloy{} can calculate the scopes
implicitly, see~\cite[p.~283]{Jackson:2012:SAL:2141100}.


\section{Missing Features}
\label{sec:data/miss-feats}

None of the languages explicitly support operators for dynamic
allocation of parts of the state (\emph{i.e.} ``\texttt{new}'' as in
Spin~\cite{DBLP:books/daglib/0020982}).  Further, none of the
languages have a ``message passing channel'' feature like Spin does,
and such a construct must be modelled using snapshot variables and
techniques ensuring correct synchronization.  Also, none of the
languages have a built-in construct for time; but it can be modelled
using techniques such as the ``explicit-time'' approach explained
in~\cite{DBLP:conf/charme/Lamport05, DBLP:conf/compsac/ZhangGS10},
wherein the current time is represented as the current value of a
snapshot variable, and the passage of time is modelled using a
transition that increments the value of that variable.


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