% case-studies.tex --- discussion of our case studies -*-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{Case Studies}
\label{chp:cs}

In this chapter we present several case studies across the data-
vs. control-oriented spectrum that we carried out to help us compare
the languages with respect to our developed comparison criteria.  We
dedicate a section to each case study, in which we examine the models
of that case study in each language, mentioning the noteworthy
characteristics and the differences between them based on the criteria
in the control and data modelling chapters.  When discussing a
particular criterion, we put the criterion's name in \textbf{bold} in
the sentence.  Our case studies were not large enough to exercise the
differences presented in the modularity chapter.  We conclude each
section with our recommendations as to which language(s) are better
suited for modelling that particular case study.

Table~\ref{tab:cs/loc} shows the sizes of each model of each system
across the languages.  The entry in row $i$ column $j$ is the number
of lines of code for the model of the case study $i$ in the language
$j$.  The models for our case studies can be obtained from
<\url{https://bndl.org/mmath}> or
<\url{https://github.com/WatForm/models}>.

\begin{table}[h]
  \centering
  \caption{Lines of code for each case study across the languages}
  \label{tab:cs/loc}
  \input{table/cs-loc}
\end{table}


\section{EHealth}
\label{sec:cs/ehealth}

The first case study tackled in this thesis is the EHealth (Electronic
Health) system, originally done in \tla{} by Professor Jonathan
S. Ostroff~\cite{ostroff2017}.  The goal of the EHealth system is to
make sure that medications prescribed to patients are safe, by keeping
track of dangerous interactions between the medications recorded in
the system.  The system allows a transition adding a medication to a
patient's prescription if and only if it does not interact dangerously
with any of the other medications previously prescribed to that
patient.

The EHealth system falls on the very data-oriented end of the data-
vs. control-oriented characterization spectrum due to its use of rich
\textbf{primitives} (such as sets and tuples) and
\textbf{constructors} (such as relations and functions), and having no
need for fine control of when a transition is relevant beyond the
preconditions of each action.  It consists of the following
components:
\begin{itemize}
\item two sets representing all patients and medications in the
  universe;
\item four snapshot variables representing sets of patients,
  medications, interactions, and prescriptions registered in the
  system; where the variable for interactions maps each medication to
  a set of medications with which it has undesired interactions, and
  the variable for prescriptions maps each patient to a set of
  medications prescribed to that patient; and
\item transitions for adding patients and medications, and for adding
  and removing interactions and prescriptions.
\end{itemize}

We consider the following three safety properties for the EHealth
system:
\begin{itemize}
\item Symmetry of interactions: medication $m_1$ has an undesired
  interaction with a medication $m_2$ if and only if $m_2$ has an
  undesired interaction with $m_1$.
\item Irreflexivity of interactions: no medication has an undesired
  interaction with itself.
\item Safety of prescriptions: for all pairs of medications $m_1$ and
  $m_2$ and patient $p$, if $m_1$ and $m_2$ are prescribed to $p$ then
  $m_1$ and $m_2$ do not have an undesired interaction.
\end{itemize}

The transitions for adding an interaction and adding a prescription
must have appropriate preconditions to ensure that the above safety
properties are always satisfied.  Namely, prescription of a mediation
for a patient must only be allowed if the newly prescribed medication
does not have an undesired interaction with any of the patient's
existing prescribed medications.  Further, addition of a pair of
medications as having undesired interaction must only be allowed if
the two medications are different, and that they are not both
prescribed to any patient already.

The \tla{} model of the EHealth system is used as reference for
modelling the system in the other languages studied in this work.  I
had written the \tla{} version, as a completed extension of the
snippets in Prof. Ostroff's technical report~\cite{ostroff2017}, based
on the descriptions there.  As \tla{} does not have
\textbf{constructors} for partial functions, the model uses relations
for representing the prescriptions and interactions data.  Although we
wrote the transitions such that the relations represent partial
functions, we did not impose any additional constraints enforcing
this.

The \B{} and \dash{} models of the EHealth system were written by Ali
Abbassi and Jose Serna respectively.  Compared to \tla{} where there
are no \textbf{type signatures}, \B{} and \dash{} have type signatures
and \textbf{typechecking}.

Similar to the \B{} EHealth model, the \eventb{} model also has
\textbf{type signatures} with automatic \textbf{typechecking}.  In
contrast to the \B{} model, the \eventb{} version correctly uses type
signatures that are consistent with the use of data in the model.  The
\eventb{} model uses the \textbf{constructor} a partial function
representation for prescriptions and interactions data over only the
set of people and medications that have been added to the system.
This representation establishes the \textbf{invariants} in the initial
snapshot and preserves them in future snapshots.

The notable difference between the \dash{} EHealth model and the
reference \tla{} version is the use of \dash's \textbf{monitored
  variables} for the input variable declarations, by marking the input
patient and input medications snapshot variables with the
\dashcode{env} keyword.

The first notable difference between the \alloy{} and \tla{} models of
the EHealth system is that in the \alloy{} model, we represent the
input variables as snapshot variables prefixed with
``\alloycode{in_}'' that are never constrained in the destination
snapshot.  Due to the nature of the \textbf{frame problem} in \alloy,
this effectively makes these variables \textbf{monitored variables}.
Although one could use a similar approach in \tla, it makes little
sense to do so, because in \tla{} every snapshot variable must be
constrained in every transition, and making the input variables part
of the snapshot would make the transitions needlessly more verbose.
In fact, this is the reason why all of our \alloy{} models for the
case studies are the largest, because in \alloy{} all (non-monitored)
snapshot variables that are to remain unchanged by a transition must
be constrained by that transition.  The second difference between the
two models is that in the \alloy{} model, the predicate for every
transition requires the source and destination snapshot of the
transition as arguments.  However, in the \tla{} model, the arguments
to each snapshot are only the input variables, as \tla{} has built-in
support for source and destination snapshots using unprimed and primed
variable names, and the packaging of the \textbf{snapshot} is
implicit; whereas in \alloy, unprimed and primed variables do not have
any significant meaning in the language, and the packaging of the
snapshot is an explicit signature.

The \pluscal{} model of the EHealth system closely resembles the
\tla{} version, with many common/overlapping \tla{} expressions
between the two models.  Where the \tla{} model used a \tla{} action
(definition) directly for defining each transition, in the \pluscal{}
version each \pluscalcode{process} corresponds to one transition.
Since the \pluscalcode{process}es each contain a single \pluscal{}
label, the translation of the \pluscal{} model back to \tla{} results
in one \tla{} transition per each \pluscal{} \pluscalcode{process}.

The \asmetal{} EHealth model, like the reference \tla{} model, uses a
relation representation for the prescriptions and interactions data
because of \asmetal's lack of a partial function \textbf{constructor}.
This model is one of two \asmetal{} models among our case studies for
which we were able to use the AsmetaSMV model checker, because as
previously mentioned, AsmetaSMV currently only supports a limited
subset of the \asmetal{} language, and in this model we were able to
confine ourselves to using the limited subset of the language.  For
instance, use of \asmcode{Powerset} in \textbf{type signatures} for
declaring set-valued snapshot variables is not supported by the model
checker, so we did not use it in this model.  To work around the
limitation, we used membership predicates for representing membership
in the sets and functions in the type signatures of the snapshot
variables, as shown in Figure~\ref{fig:cs/ehealth/pluscal-mem-pred}.
\input{figure/cs-ehealth-pluscal-mem-pred}

For the EHealth case study, we found all languages and their tooling
to be adequate and useful for modelling and debugging the system, as
there is little structure in the control aspects of the transition
system, and the \textbf{primitives} and \textbf{constructors} used in
the example are fairly standard across declarative modelling
languages.  For the \asmetal{} EHealth model, although the need to use
a membership predicate representation for sets, so that we could use
the AsmetaSMV model checker, did not pose a serious issue in our
modelling and verification process, we did find it to be an annoyance
and deviation from the reference model nonetheless.  More importantly,
\asmetal{} does not have a \textbf{constructor} for partial functions.
Further, while writing the \alloy{} model, we found ourselves running
into strange behaviours with our model, which we eventually noticed
was due to under-specification in some of our transition definitions,
relating to the \textbf{frame problem}, where in \alloy{} any variable
not constrained in a transition may freely change from the source to
the destination snapshot.  This may be a common mistake by modellers
of varying levels of experience, and may be hard to debug due to it
causing unexpected behaviour in various parts of the model.  As such,
we would be less inclined to recommend \alloy{} for modelling this
example.


\section{Digital Watch}
\label{sec:cs/digital-watch}

The second case study in this thesis is the digital watch example, an
adaptation of Harel's model~\cite{DBLP:journals/scp/Harel87}.  The
digital watch system consists of a digital display and four buttons
$a$, $b$, $c$, and $d$.  The watch has several modes/states of
operation that may be accessed using specific sequences of button
presses.  The digital watch system has a large number of
\textbf{control states} and many \textbf{events} triggering
transitions between them, and depends on control state hierarchy to
decompose these into related parts.  Considering this, and the model's
limited use of \textbf{primitives} and \textbf{constructors}, the
digital watch example falls on the very control-oriented end of the
data- vs. control-oriented characterization spectrum.  For the digital
watch system, we consider the following reachability property: from
any snapshot, when $a$ is pressed, it is possible to get to a snapshot
in which in the next snapshot the watch will be in the Time state.

The reference model for the digital watch system is written in \dash{}
by Jose Serna~\cite{DBLP:conf/re/AbbassiBDS18}.  The model makes
extensive use of \dash's \dashcode{state} construct to hierarchically
decompose the watch's behaviour.  The model's \textbf{control state
  hierarchy} consists of two concurrent regions, one representing the
state of the watch's display light, and the other representing the
current active display.  It also uses \dash's environmental
(\textbf{monitored}) \textbf{events} for representing the button
presses of the watch and passage of time, to enable transitions.  The
above reachability property does not always hold in the \dash{} model
and is not an invariant of the system, as expected.

The \B{} and \tla{} models of the digital watch system were written by
Ali Abbassi and myself respectively.  Since \textbf{control state
  hierarchy} and \textbf{events} are not supported by any of the
modelling languages studied in this work besides \dash, we model these
features using other constructs available in each language.  For
control state hierarchy, we model all transitions flatly (\emph{i.e.}
no hierarchy), which required extra care to ensure that the
preconditions of the transitions of the flat model are written
correctly, so that each transition in the flat model is only enabled
if and only if its corresponding transition in the hierarchical model
is enabled.  This involves making sure that the hierarchical and
concurrent states of the reference model are faithfully represented in
the non-hierarchical versions.  We use one variable for representing
each concurrent region of the reference model, ensuring that the
concurrent regions can change independently of each other.  For
\textbf{events}, we model each using a combination of a variable
keeping the triggered state of the event, and a transition (or pair of
transitions) to change that variable.  We allow events to persist
arbitrarily long into the future.
% big step?
The advantages of these approaches include the fact that the flat
model closely resembles the original hierarchical model.  The
disadvantages include that extra care needs to be taken to make sure
that the preconditions for each transition are set up correctly to
faithfully match the behaviour of the transition in the hierarchical
model as closely as possible.  In the absence of \dash's
per-\dashcode{state} \textbf{namespaces}, we use a naming convention
for the names of transitions to highlight the state of the reference
model each transition belongs to.  The above descriptions apply to the
remainder of the digital watch models in all of the languages (besides
\dash).

The behaviour of the \B{} model by Abbassi does not fully match the
earlier descriptions, particularly with respect to \textbf{events}.
In Abbassi's model, the transitions modifying the display state also
change the triggered state of the events.  However, these two belong
in separate concurrent regions, and doing so effectively ties together
the two concurrent regions of the reference model.  This results in a
special-case behaviour not necessarily guaranteed by the original
model.

One difference between the \tla{} and \eventb{} models of the digital
watch system and the rest of the models is that for the
pressed/released state of the four buttons, we used a total function
that maps each button to a Boolean value, instead of four separate
Boolean variables.  This allows for a more compact representation of
\textbf{events}, with only one or two transitions that could change
the state of any of the events, as opposed to requiring one or two
transitions per each event.

In the \asmetal{} digital watch model, we represent \textbf{events} as
\textbf{monitored variables} (using the \asmcode{monitored} keyword)
which may change freely from one snapshot to the next.  This
eliminates the need to include transitions for toggling the
variable(s) representing the triggered state of the events.  As
discussed in Chapter~\ref{chp:control}, \asmetal{} does not support
defining the \textbf{transition relation} as a disjunction of multiple
transitions.  To write a transition relation that would take a
randomly-chosen transition each time, we have to declare an enumerated
set with each element corresponding to one transition, use the
\asmcode{choose} rule in the definition of the transition relation to
choose an element from that set, and use a \asmcode{switch} with a
\asmcode{case} for each transition, executing the transition
corresponding to the chosen element of the enumerated set.  This is
especially cumbersome and error-prone in a model such as the digital
watch system with many transitions, as the modeller may forget to
update the \asmcode{switch} cases when adding or removing transitions.
The \asmetal{} digital watch model is the second of the two \asmetal{}
models among our case studies for which we was able to use the
AsmetaSMV model checker, finding a satisfying instance for the
reachability CTL property.

The \pluscal{} digital watch model closely resembles the \tla{}
version, with many common \tla{} expressions between the two models.
These include the reachability property written as a \tla{}
expression.  Where the \tla{} model used a \tla{} action (definition)
directly for defining each transition, in the \pluscal{} version each
\pluscalcode{process} corresponds to one transition.  Since the
\pluscalcode{process}es each contain a single \pluscal{} label, the
translation of the \pluscal{} model back to \tla{} results in one
\tla{} transition per each \pluscal{} \pluscalcode{process}.

For the digital watch case study, we found \dash's unique
\textbf{control state hierarchy} and \textbf{events} constructs to be
powerful and convenient abstractions for modelling the various
states/modes of the control-oriented digital watch system.  We thus
recommend \dash{} as the most suitable language for this example.


\section{Musical Chairs}
\label{sec:cs/musical-chairs}

The musical chairs case study (originally in~\cite{Nissanke_1999})
resides near the middle of the data- vs. control-oriented
characterization spectrum.  The musical chairs example is a game
consisting of a number of players and chairs.  At any time during the
game, there is always exactly one less chair than there are players.
In each round, the players circle the chairs while music plays.  The
music is then stopped abruptly, and the players have to scramble to
sit on a chair.  The one player who did not manage to sit down is
eliminated, and one of the chairs is also eliminated.  The music then
resumes, and the next round begins.  This process is repeated until
only one player remains, dubbed the winner.

The snapshot variables in a musical chairs model consist of two sets
for active players and active chairs, and a mapping from chairs to
players for keeping track of the occupied chairs.  Further, the
current mode of the game (players are sitting, walking, \emph{etc.})
is represented either as an enumerated set or using control states.
The status of music (playing or paused) is represented either using
events for control states, or as a snapshot variable and transition(s)
changing it.

For the musical chairs case study, we consider the following safety
and liveness properties:
\begin{itemize}
\item The number of players is always one greater than the number of
  chairs.
\item It is possible that a specific player named Alice wins.
\item The game will always eventually be in the ``sitting'' state.
\item The number of active players always eventually reaches one and
  remains at one.
\end{itemize}

The reference model for the musical chairs example is written in
\dash{} by Jose Serna.  The model uses \dash's \textbf{control state
  hierarchy} for representing the different modes of the game.
Further, two environmental (\textbf{monitored}) \textbf{events}
\dashcode{MusicStops} and \dashcode{MusicStarts} are used to model the
abrupt stopping and starting of music.  The above four properties were
verified to hold for the \dash{} musical chairs model.

The \dash{} model of the musical chairs example used as the reference
for the other models in this work was itself modelled after an
\alloy{} musical chairs model~\cite{farheen2018} by Sabria Farheen.  A
notable difference between this \alloy{} model and the \dash{} model
of this system is the absence of \textbf{control states} and
\textbf{events} in \alloy.  Thus, the current mode of the game is
represented using a \textbf{snapshot variable} with its value a member
of an enumerated set, and the starting and stopping of music are
modelled as transitions that directly change the snapshot variables,
including the mode of the game.  The above four properties were
included and verified to hold for the \alloy{} musical chairs model as
well.

Similar to the \alloy{} musical chairs model, the \B{} musical chairs
model~\cite{DBLP:conf/re/AbbassiBDS18} by Ali Abbassi uses a snapshot
variable for representing the mode of the game along with two snapshot
variables keeping the sets of active players and active chairs, and an
occupancy mapping between the two.  There are some notable differences
between the two models.  Namely, the \B{} version uses the
\textbf{constructor} of a total function in the \textbf{type
  signature} of the occupancy mapping, and has two extra variables
keeping the player and chair to be eliminated at the end of the
current round.  Further, an \bcode{Assign} \textbf{constant} predicate
is defined and used to constrain the occupancy mapping according to
the given sets of chairs and players.  Also, there is no snapshot
variable keeping the status of music explicitly, and there are no
separate transitions dedicated to starting and stopping of music.
Instead, the effects of starting and stopping the music are carried
out in the main transitions of the system.  This choice of
representation makes the \B{} musical chairs model more different than
the models of this system in the other languages, since starting and
stopping of music is not a standalone \textbf{event} in this model,
and is \emph{always} accompanied by a change/progress in the game.
These changes are \emph{not} inherently necessary, and it is possible
to model the system in \B{} without them.

The differences between the \tla{} and \dash{} musical chairs models
stem from the absence of \textbf{control states} and \textbf{events}
in \tla.  As with the previous \tla{} models, we used a snapshot
variable for tracking the current state of the game, corresponding to
\dash's use of \textbf{control state hierarchy}.  This makes the
\tla{} model more similar to the \alloy{} version.  However, in
contrast to the \alloy{} model, for the \tla{} model we used a Boolean
variable for modelling the status of the music, and used a separate
transition \tlacode{ChangeMusicPlaying} for changing the status of
music.  For this reason, along with the fact that we are checking
liveness properties for the system, we impose fairness conditions on
the transitions.  As such, we added weak fairness (justice) on the
\tlacode{ChangeMusicPlaying} transition and strong fairness
(compassion) on the rest of the transitions in the model, so that the
firing of the music change transition would not starve the main
transitions.

The \textbf{expressions} of the \asmetal{} musical chairs model are
less declarative and more imperative than our other musical chairs
models, because in \asmetal{} we cannot constrain the destination
snapshot value of the occupancy function in a declarative manner, as
we would in the other languages.  We could use \asmetal's set
comprehension notation if the occupancy mapping was a relation; but we
cannot use a formula or constructor to further constrain that set of
pairs to be a function in a declarative way.  Instead, for filling up
the occupancy function when the music stops, we have to use a helper
transition to update the occupancy mapping for each chair one by one
using a \asmcode{forall} rule over the active chairs and a nested
\asmcode{choose} rule over the active players (excluding the loser of
the round).  A reasonable idea may be to keep the \textbf{type
  signature} of the occupancy function as
\mbox{\asmcode{Powerset(Prod(Chair, Player))}}, but this will not work
because gradually updating the occupancy mapping using the
\asmcode{union} function is seen as assigning multiple different
values to the same snapshot variable, and thus an inconsistent update.
Therefore we have to change the \textbf{type signature} to
\asmcode{Chair -> Player}.  We will not be able to easily extract all
the information we need from a variable with this type signature; for
instance we need to introduce a separate variable to keep track of the
number of occupied chairs.  Due to these limitations, the \asmetal{}
musical chairs model has tedious imperative-style operations for
updating the function-valued snapshot variables.

The \pluscal{} musical chairs model for the most part resembles the
\tla{} version, with many common \tla{} expressions between the two
models.  Aside from the inherent differences between \pluscal{} and
\tla{} in terms of defining transitions, the two models also differ in
how they constrain the occupancy function: Assignment to
\textbf{snapshot variables} in \pluscal{} is done only using the
\pluscalcode{:=} assignment operator and the constraints need to be
described all at once, whereas in \tla's declarative approach, the
modeller describes how each snapshot variable changes, using one or
more conjuncts.  Also related, in regular \tla{} \textbf{expressions}
we can always refer to the source snapshot value of a variable in a
transition using its unprimed name, whereas we cannot do so in
\pluscal{} if the variable is assigned to in the current transition.
In \pluscal, we can declare a variable local to the \textbf{namespace}
of that \pluscalcode{process} and initialize it with the source
snapshot value of that variable, and use the local variable where
needed in the process (transition) body.

The \eventb{} musical chairs model uses the language's rich arrow
\textbf{constructors} for various functional and relational units of
data in \textbf{type signatures} as well as snapshot variable
assignments.  These arrows, when combined with the $:\!|$
nondeterministic assignment operator, are a powerful way of writing
terse and concise descriptions of functions.  We declare the occupancy
mapping to be a partial injection from chairs to players, and in the
\eventbcode{Sit} transition we assign to the occupancy function a
total injection from the sets of active players to active chairs,
enforcing the two criteria that each chair can have only one player
sitting on it, and each player may only sit on one chair.

For the musical chairs case study, we found \dash's \textbf{control
  state hierarchy} and \textbf{events} to lend themselves well to
modelling this system.  The control states and their hierarchy are
used to concisely and precisely represent the current state/mode of
the game, and \dash's environmental (monitored) events are a natural
candidate for modelling the starting and stopping of music.  Since
these features are unique to \dash, we believe they give \dash{} an
advantage over the other languages.  After \dash, we found \B{} and
\eventb's extensive set of arrow \textbf{constructors} to be
convenient and powerful tools for writing concise \textbf{type
  signatures} and constrains on functional and relational data units.


\section{Library Management}
\label{sec:cs/library}

The library management case study (originally by Frappier
\emph{et~al.}  in~\cite{DBLP:journals/sosym/FraikinFL05,
  DBLP:conf/icfem/FrappierFCCO10}) resides at the very data-oriented
end of our data- vs. control-oriented characterization spectrum.  The
library management information system has a set of members and a set
of books available in the library.  Members can join and leave the
library, and books may be acquired or discarded by the library.  Each
member can borrow a certain maximum number of books and return any of
them when they wish.  Members can also reserve a book if it has
already been lent to another member.  Doing so will add the member to
a wait list for the book, and they can pick up the book when it
becomes available to them.  They can also cancel their reservation at
any time if they wish to.  Members may renew any of their borrowed
books if no other member has entered the reservation waiting list for
that book.  A member may only leave the library (relinquish their
membership) when they are not borrowing or reserving any of the
library's books, and a book may only be discarded by the library if it
is not loaned to or reserved by any members.

The snapshot variables in the library management system consist of two
sets for acquired books and registered members, and two mappings, one
for keeping track of the books loaned to members, and the other for
tracking the reservations placed for the currently-unavailable books.
This mapping should store the order in which reservations were placed,
so as to allow a pickup only by the member who placed the current
oldest reservation for that book.

The reference model for the library management case study is in \B{}
by Frappier \emph{et~al.}~\cite{DBLP:conf/icfem/FrappierFCCO10}.  The
model uses the \textbf{constructor} of a partial function from books
to members for keeping track of the lent books, and a total function
from books to an injective sequence of members for tracking the
reservations.  A number of safety and liveness properties are included
in the reference \B{} model, such as:
\begin{itemize}
\item A book may be reserved only if it has been lent or already
  reserved by another member.
\item A book cannot be lent to a member if it is reserved.
\item A member is allowed to pick up a reservation only if their
  reservation is the current oldest.
\item Ultimately, a member can leave the library. (CTL property, not
  expressible in LTL)
\end{itemize}

In addition to the \B{} library management model used as reference for
our subsequent models, the above paper by Frappier \emph{et~al.} also
contains an \alloy{} model of the system.  This model, though written
well before Farheen wrote her style guidelines~\cite{farheen2018},
adheres to several of Farheen's recommendations promoting structure,
including decomposing each transition definition into two separate
predicates, for preconditions over the variables in the source
snapshot and postconditions over the variables in the source and
destination snapshots, respectively.  With respect to the
\textbf{frame problem} in \alloy, the modellers also took the extra
step to put the no-change formula for each snapshot variable into a
separate predicate, and use those predicates in the transition
definitions instead of repeating the constraints.  We believe this may
be excessive, given the simplicity and triviality of such constraints.

The \eventb{} library management model is in many ways similar to the
reference \B{} model, considering the closeness of the two languages.
A notable difference between the two is the absence of a sequence
\textbf{constructor} in \eventb.  As such, we had to use a partial
injective function from the set of natural numbers to members to model
the injective sequence of members from the reference \B{} model.
\eventb's lack of built-in sequences and operations on them was
particularly inconvenient when writing the \eventbcode{Reserve}
transition, where we need to update the reservation mapping for the
given book and insert the new member with the correct index in the
book's reservation function.

The \tla{} and \pluscal{} models of the library management system are
similar to the reference \B{} model in their use of a partial function
for representing the loans mapping from books to members.  They differ
from the \B{} model in that the \tla{} and \pluscal{} models do not
have \textbf{type signatures} and \textbf{constructors}, and use a
formula definition in the typing constraint to express that
\tlacode{loans} should be a partial function.  However, since all
\tla{} functions are by default total, it may not be obvious to a
modeller how to specify a partial function.  To declare a partial
function, we first add a helper definition ~\tlacode{PFun(S, T) ==
  UNION \{[s -> T] : s \\in SUBSET S\}}~ describing all partial
functions from \tlacode{S} to \tlacode{T}, where the domain could be
any subset of \tlacode{S}.  We can then use this predicate to write a
constraint such as ~\tlacode{loans \\in PFun(books, members)},~ making
\tlacode{loans} a partial function from \tlacode{books} to
\tlacode{members}.  There are other possible representations and
constraints for \tlacode{loans}, such as \tlacode{[books -> SUBSET
    members]} and \tlacode{[books -> members \\union NULL]}, but aside
from diverging from the reference specification, the other
disadvantages of using these include adding unnecessary verbosity to
the model and requiring special treatment of the \tlacode{NULL}
constant throughout the model, respectively.

Modelling the library management system in \pluscal{} and checking it
using the \tlc{} model checker helped expose a bug in one of the
properties from the reference \B{} model, due to incorrect assumptions
about operator precedence and associativity in \B{} along with using
$=$ instead of $\neq$.

With respect to the criterion of syntax of \textbf{expressions}, the
\asmetal{} library management model is more verbose compared to our
other models of this system, because in \asmetal{} most operators have
long-form textual names.  However, in terms of transitions and
\textbf{type signatures} it is very similar to our other library
management models.  Since \asmetal{} transitions are always enabled
and there is no keyword for checking whether a transition is enabled,
we factored out the conditions of the top-level \asmcode{if} rule for
each transition into separate \asmcode{derived} functions.  We then
used these functions in the properties to check when each transition
can be taken.

The \dash{} model of the library management system is fairly similar
to the reference \B{} model.  We were able to translate and check the
properties from the original \B{} model to \dash, as they all happened
to lie in the set of properties expressible in both LTL and CTL.
Additionally, as \dash's tool support supports CTL model checking, we
were able to express in \dash{} one of the CTL properties that was
commented out in the original model and not expressible in LTL.

For the library management case study, we found the \texttt{Cancel}
and \texttt{Reserve} operations to be the most challenging to model
correctly across the languages.  This is because these operations
require correctly updating or overriding the entry corresponding to a
book in the reservations mapping, where each entry itself is an
ordered collection of members.  This has to be done while preserving
the structural correctness of the underlying data unit.  This was
hardest to do in \eventb{}, \tla/\pluscal, and \asmetal.  For \eventb,
the absence of a built-in sequence \textbf{constructor} and supporting
operations was what made this challenging.  For \tla/\pluscal, even
though \tla{} has built-in sequences, we found the available
operations for correctly modifying sequences to be lacking for our
purposes in the \textbf{expressions}.  Thus, the challenge was writing
correct custom definitions for operations on functions and sequences.
We found that \asmetal's more imperative-style \textbf{expressions}
make modelling this system more challenging.  Namely, the lack of
certain declarative operations and the difficulty of writing a
\textbf{transition relation} that would take a randomly-chosen
transition, described earlier.  As such, we recommend \B, \dash, or
\alloy{} for modelling this system.  We would recommend exercising
caution while using \alloy, due to the dangers of under-specification
relating to the \textbf{frame problem}.


\section{Railway Scheduling Deadlock Freedom}
\label{sec:cs/railway}

The railway scheduling deadlock freedom (railway for short) case study
originally by Mazzanti \emph{et~al.}
in~\cite{DBLP:journals/sttt/MazzantiFS18} resides near the middle of
the data- vs. control-oriented characterization spectrum.  The railway
system is a model of a yard consisting of eight trains and their
missions.  The yard contains a number of critical sections of railway
tracks that the scheduling algorithm must ensure are never saturated,
which would cause a deadlock in the system where no train could
proceed.  Briefly, this is done by keeping track of the number of
trains currently present in each critical section, and making sure
that number is always below a certain maximum that would not cause the
system to reach a deadlock.  For the railway case study, the property
we are interested in is whether all of the trains always eventually
reach their final destination, \emph{i.e.} the last station on their
mission.  For a model to satisfy this property, it must be accompanied
with appropriate fairness constraints.

The railway system was originally modelled in UMC, Promela/SPIN,
NuSMV, mCRL2, CPN Tools, FDR4, and CADP.  Thus, for our first model of
this system that we wrote (in \B), we based our work mostly on the
descriptions in the original paper, occasionally comparing our model
against the paper's accompanying NuSMV and Promela models for
clarification.  For the subsequent models of the system, we used our
\B{} model as the reference.

The \B{} and \eventb{} railway models use \textbf{type signatures} to
specify what the precise ranges of the valid natural numbers of the
model's \textbf{primitives} are.  Compared to the models accompanying
the original paper, our \B{} and \eventb{} models use a more compact
representation for the train missions and critical section
constraints.  Instead of declaring eight separate snapshot variables
one for each train, we use the \textbf{constructor} for a total
function with the domain \bcode{0..7}.  This allows accessing the
missions and constraints using the index for each train, alleviating
the need for writing eight separate \bcode{move_train} transitions,
one for moving each train.  Instead, the \B{} and \eventb{} models
each have only one transition for moving all of the trains, which
indexes into the relevant snapshot variables using the currently
chosen train \bcode{ct} as the index.  The chosen train index,
represented by the \bcode{ct} snapshot variable, is updated in a
round-robin fashion each time the \bcode{choose_train} transition is
executed.

The \asmetal{} model of the railway system is similar to the reference
\B{} version.  The notable difference is \asmetal's distinction
between \textbf{controlled} and \textbf{monitored} variables.  We
designate the snapshot variable for the currently chosen train as a
\asmcode{monitored} variable, eliminating the need for having a
\asmcode{choose_train} transition.

The \alloy{} railway model differs from the reference \B{} model in a
number of ways.  These differences stem from the fact that \alloy's
\textbf{built-in} integers are highly inefficient in analysis (it is
not a modelling language problem; see
Section~\ref{sec:data/primitives} and Section~\ref{sec:data/scopes}),
and increases in \textbf{scope} of integers results in them quickly
becoming a performance bottleneck during the analysis.  As such,
instead of using integers for modelling trains and stations, we use an
enumerated set for each, allowing us to avoid increasing the scope of
integers.  The downside of this approach is that it makes writing the
model more tedious, and drastically increases the line count for the
\alloy{} model, as we can no longer use only one transition capable of
moving any of the trains, and have to write one transition per each
train.

The \pluscal{} and \tla{} models of the railway system differ from our
reference \B{} model due to the absence of \textbf{constructors} and
\textbf{type signatures} in \tla{} and \pluscal.  The \pluscal{} and
\tla{} models are very similar to each other.  Both models have two
transitions, one for moving any train, and another for choosing the
train to be moved, with strong fairness imposed on the former and weak
fairness on the latter.  This helps make sure the transition for
changing trains does not starve the transition for moving a train.

The \dash{} railway model is similar to the \alloy{} model, differing
from the reference \B{} model in their use of an enumerated set
representation instead of integers for the train stations.  Aside from
the inherent differences between \dash{} and \alloy, the two models
differ in their use of \alloy's more recent features in its
\textbf{expressions} language.  Namely, \dash{} does not yet support
\alloy's \alloycode{let} expressions and the \alloycode{enum}
short-hand for declaring an enumerated set.  The other main difference
between the two models is that in the \dash{} model, we use the
\dashcode{env} keyword for the chosen train snapshot variable to mark
it as a \textbf{monitored} variable, allowing the environment to
choose which train to move next.  This lets us eliminate the
\dashcode{choose_train} transition in favour of a more general
train-choosing mechanism.  However, similar to the \alloy{} model, the
\dash{} railway model is noticeably larger than the other models of
the railway system, as we have to write one transition per each train,
for the same reasons as the \alloy{} model, explained earlier.

For the railway scheduling deadlock freedom case study, the
limitations of integers in \alloy{} really shows during analysis, and
needs to be worked around if possible.  For the \alloy{} and \dash{}
railway models, we kept the \textbf{scope} of integers at a minimum by
using enumerated sets instead of integers for representing the 27
train stations.  We believe that \B, \eventb, \tla, \pluscal, and
\asmetal{} are better equipped to handle this model's use of integers.
\dash{} and \pluscal{} in particular distinguish between controlled
and \textbf{monitored} variables, allowing the modeller to denote the
snapshot variable for the currently chosen train as a monitored
variable changed by the environment.  This eliminates the need for a
transition for changing the variable.


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