% control.tex --- control 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{Control Modelling}
\label{chp:control}

In this chapter, we discuss in depth the control aspects and the
structure of transition systems as modelled in each of our selected
modelling languages.  Each section starts with a brief summary of the
characteristics of the languages with respect to the section's
comparison criterion, followed by detailed discussion of the criterion
across the languages.  Table~\ref{tab:control/summary} summarizes the
differences in the structure of transition systems as modelled in each
of our selected declarative modelling languages.  Another important
element in modelling is understanding how inconsistencies appear in
each language.  While inconsistencies in models may appear in all
languages, we discuss some of the details and ramifications of these
inconsistencies in Section~\ref{sec:control/incon}.

As a reminder, the main concern of this thesis is comparison of the
selected modelling languages for modelling transition systems, even
though some of these languages may be used for more general-purpose
modelling.  Namely, the \pluscal{} algorithm language is a language
designed for formal specification of algorithms as a counterpoint to
pseudo-code, and \alloy{} is a declarative specification language
capable of modelling complex structural and behavioural constraints of
software systems.  For our purposes, we do not consider checked
properties to be a part of the model.

\begin{table}[h]
  \centering
  \caption{Summary of control aspects of languages}
  \label{tab:control/summary}
  \input{table/control-summary}
  \raggedright
  \footnotesize
  \vspace{0.25em} \textit{Legend:} \\ \textbf{TR}: Transition
  Relation.  \textbf{E}: Explicit.  \textbf{ME}: Mostly Explicit.
  \textbf{I}: Implicit.  \textbf{S}: Described in \tlc{} model
  settings.  \textbf{C}: Constraints on snapshot space.  \textbf{V}:
  Verified to hold.  \textbf{I(a)}: Implicit with all variables
  unchanged.  \textbf{I(m)}: Implicit with monitored variables
  unchanged.
\end{table}


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

As choice of terminology varies from one language to the next, we
first define some standard terminology that we will use throughout
this chapter when comparing the seven languages.  We will use the
words \emph{implicit} and \emph{explicit} carefully when referring to
language constructs in this chapter: we say a construct is
\emph{explicit} in a language if the language has a textual
representation corresponding to that construct; and otherwise we say
it is \emph{implicit}, which may potentially be built/calculated by
the tool support behind the scenes.

\begin{itemize}
\item \textbf{Snapshot}: is a mapping of variables to values.
\item \textbf{Snapshot space}: is the set of all possible snapshots of
  a transition system, \emph{i.e.} the cross product of variable
  values.
\item \textbf{Transition System}: a transition system $TS$ is a tuple
  $(S, TR, I)$ where $S$ is a set of snapshots, $TR \subseteq S \times S$ a
  transition relation, and $I \subseteq S$ a set of initial snapshots.  A
  model in a declarative modelling language defines a transition
  system that starts in an initial snapshot $s_0 \in I$ and progresses
  from a snapshot $s$ to the next snapshot $s'$ for $(s, s') \in TR$.
\item \textbf{Labelled control state}: is a distinguished set of
  variables with a finite set of values, that are used to control when
  a transition can be taken.  Languages with labelled control states
  can have \textbf{control state hierarchy} and concurrency.
\item \textbf{Transition}: a transition relation may be composed of a
  set of transitions, each $T \subseteq TR \subseteq S \times S$ with potentially multiple
  $(s, s')$ mappings from source snapshot $s$ to destination snapshot
  $s'$.  When a transition is defined using declarative constraints,
  it represents a set of pairs; hence our use of $T \subseteq TR$ (as opposed
  to $T \in TR$) above.
\item \textbf{Trace}: is an execution path, consisting of a series of
  steps, where a \textbf{step} is a pair $(s, s')$ of snapshots where
  $(s, s') \in TR$.
\item \textbf{Monitored variable}: also referred to as an
  environmental variable, is one that can be only observed by the
  model but not changed by it \md they are only changed by the
  environment.  Monitored variables are commonly used for modelling
  environmental phenomena such as temperature as obtained from a
  sensor.  Conversely, a \textbf{controlled variable} (a
  non-environmental variable) is one that may be both observed and
  changed by the model.
\item \textbf{Frame problem}: refers to the issue of how snapshot
  variables that are not explicitly changed in a transition may or may
  not change from one snapshot to the next.  The frame problem is
  particularly an issue in declarative languages that rely on logical
  constraints on variables for describing the changed and unchanged
  variables in a transition.  Since in all studied languages only one
  transition is taken per step, the frame problem can be discussed at
  the transition level (Section~\ref{sec:control/trans}).  If in a
  language more than one transition may be taken in a step, the frame
  problem would need to be discussed in the context of the transition
  relation as well.
\item \textbf{Invariant}: of a transition system is a formula that is
  true in all snapshots.
\item \textbf{Fairness constraint}: is a condition on the traces of a
  transition system model.
\item \textbf{Stuttering step}: is often used to allow a change in the
  external environment.  The exact semantics of stuttering steps \md
  when they might occur, and which variables they allow to change and
  which ones they keep unchanged \md may differ between two
  declarative modelling languages, and from one model to the next.  A
  declarative modelling language may have an implicit notion of
  stuttering, in which case it will also have accompanying semantics
  as to when stuttering steps may occur: whether stuttering steps have
  a lower `priority' and may occur only when no other transitions are
  enabled, or if they have the same priority as other transitions and
  may occur even when one or more other transitions are enabled.  In a
  language with implicit stuttering, if it differentiates between
  monitored and controlled variables then usually its stuttering steps
  will allow monitored variables to change while keeping controlled
  variables unchanged, otherwise its stuttering steps will keep all
  variables unchanged (each stuttering step is a self-loop from a
  snapshot back onto itself).  In languages without implicit
  stuttering, a stuttering step must be modelled using an explicit
  transition definition, and the modeller may decide which variables
  may change and which are kept unchanged.  Explicitly-added
  stuttering steps (as transition definitions) always have the same
  priority as other transitions.  Adding stuttering steps is one way
  of ensuring the totality of a transition relation.
\end{itemize}


\section{Snapshot and Snapshot Space}
\label{sec:control/snapshot}

A snapshot is a mapping from variables to values.  The first criterion
we will compare across the languages is representation of snapshots
and variables of a transition system in each language.  Note that the
more data-oriented aspects of snapshots and the snapshot space are
discussed in Chapter~\ref{chp:data}.

In \B, \eventb, \tla, \pluscal, and \asmetal{} a model has a clause
for declaring variables, in \dash{} variables are declared at the top
of the main snapshot block, and in \alloy{} the declaration location
of variables varies depending on the choice of snapshot
representation.  Figure~\ref{fig:control/snapshot} has exemplars
showing snapshot declarations across the languages.

\begin{itemize}
\item In \B, the variables are declared in the \bcode{VARIABLES}
  clause of the machine.
\item In \eventb, the variables are declared in the
  \eventbcode{VARIABLES} part of the machine.
\item \alloy{} is a more general-purpose modelling language not
  dedicated specifically to modelling transition systems, and does not
  have an explicit construct/keyword for declaring a snapshot or its
  variables.  Thus, the choice of snapshot representation is with the
  modeller.  A common paradigm for representing snapshots in \alloy{}
  is using a \alloycode{State} signature, with its fields
  corresponding to variables.
  See~\cite{DBLP:conf/sqamia/SullivanWKM17} for other techniques for
  snapshot modelling in \alloy.
\item In \dash, a snapshot is explicitly declared using the
  \dashcode{state} keyword, and variables are usually declared at the
  top of each \dashcode{state} block.  As \dash{} supports labelled
  control state hierarchies, snapshot definitions can be distributed
  through nested \dashcode{state} blocks.  Also, \dash{} has explicit
  syntax for marking a variable as part of the environment, using the
  \dashcode{env} keyword.
\item In \tla, the variables are declared using \tlacode{VARIABLES}.
\item In \pluscal, global variables are declared using the
  \pluscalcode{variables} keyword in an algorithm.
\item In \asmetal, variables are declared in a \asmcode{signature}
  block.  Variables fall into two general categories of
  \asmcode{static} constants \md which do not change during a
  machine's run \md and \asmcode{dynamic} variables \md which may be
  changed by an agent's actions or updates.  Dynamic variables are the
  snapshot variables, and are further classified into
  \asmcode{monitored} and \asmcode{controlled}.
\end{itemize}

\input{figure/control-snapshot}


\section{Initialization}
\label{sec:control/init}

This section discusses how to specify the value of the variables for
the initial snapshot(s) of the transition system in each language.
All the studied languages distinguish syntactically variable
initialization from variable declaration, except for \pluscal{} which
not only allows but recommends specifying the initial value of each
variable together with its declaration.  Further, all the languages
except \asmetal{} support some form of nondeterministic assignment for
initialization of variables.  Figure~\ref{fig:control/init}'s
exemplars demonstrate initialization across languages.

\begin{itemize}
\item In \B, the \bcode{INITIALISATION} clause is used to assign
  values to variables for the initial snapshot(s).  The
  \bcode{INITIALISATION} keyword is followed by one or more
  \emph{substitutions} (\emph{i.e.} assignments; see Chapter~6
  of~\cite{b-manref}), using any of the `$:=$' (becomes equal
  substitution), `$:\in$' (becomes part of substitution), and
  `$:\!(\,)$' (becomes such that substitution) operators.  The `$:=$'
  operator is used similar to variable assignment in typical
  programming languages, whereas `$:\in$' assigns a randomly-chosen
  element from the given set to the variable, and with `$:\!(\,)$' the
  modeller can write a declarative formula constraining the value of
  the variable.
\item In \eventb, the \eventbcode{INITIALISATION} clause is used to
  assign values to variables for the initial snapshot(s), with actions
  using any of the `$:=$' (deterministic assignment), `$:\in$'
  (nondeterministic assignment of a set member to a variable), and
  `$:\!|$' (nondeterministic assignment to a variable using a
  before-after predicate) operators (see Section~3.3.8
  of~\cite{rodin-handbook}).  The `$:=$' operator is used similar to
  variable assignment in typical programming languages, whereas `$:\in$'
  assigns a randomly-chosen element from a set to the variable, and
  with `$:\!|$' the modeller can write a declarative formula
  constraining the value of the variable.
\item \alloy{} does not have an explicit construct/keyword for
  initializing variables.  Commonly, a predicate, conventionally named
  \alloycode{init}, is used to constrain the variable values for the
  initial snapshot(s).  Any \alloy{} expression over the variables may
  be used to constrain each variable.
\item In \dash, an \dashcode{init} block is used within a
  \dashcode{conc state} (concurrent state) to declare the values of
  the variables in the initial snapshot(s).  Any \alloy{} expression
  may be used for constraining the variables.
\item In \tla, a predicate, conventionally named \tlacode{Init}, is
  used to describe the values of variables in the initial snapshot(s).
  Any \tla{} formula may be used to constrain the values of the
  variables in the \tlacode{Init} predicate.  Note that there is
  nothing special about the name \tlacode{Init}, and any other name
  may be used, since it is not a built-in keyword.
\item In the \pluscal{} algorithm language, the initial values of the
  variables are often specified along with their declaration in the
  \pluscalcode{variables} part of the algorithm.  Typical \tla{}
  formulas may be used for constraining the variables.
\item In \asmetal, the initial values of the variables are given in a
  ~\asmcode{default init}~ block, using the `\asmcode{=}' operator.
  \asmetal{} does not support any form of nondeterministic variable
  initialization.
\end{itemize}

\input{figure/control-init}


\section{Transition Relation}
\label{sec:control/tr}

This section describes how each language allows a modeller to create a
transition relation, $TR$, of a transition system.  We describe the
languages with respect to this criterion, ranging from those wherein
the representation of $TR$ is the most explicit, to those where it is
the least explicit.  For each language, we examine its constructs for
defining a transition relation, and how stuttering steps are
represented in the language.  In the next section,
Section~\ref{sec:control/trans}, we will examine each language's
constructs for defining transitions that are composed together to form
$TR$.

Of the languages studied in this thesis, \alloy, \tla, and \asmetal{}
require a more explicit representation of a transition relation, where
$TR$ is defined mostly in the model text.  Figure~\ref{fig:control/tr}
shows exemplars defining a transition relation in each of these three
languages.  Because $TR$ is described via a set of constraints, and
not imperative definitions, a declarative modelling language may allow
expressing inconsistent transition relations.

In \alloy, the transition relation, $TR$, is defined completely
explicitly, and its form can vary greatly depending on how the
snapshot, variables, and transitions are defined.  For instance, with
a \alloycode{State} signature as the snapshot representation and its
fields as variables, $TR$ can be decomposed into predicates that can
be viewed as transitions.  In Section~\ref{sec:control/trans}, we will
discuss conventions used for defining transitions in \alloy.
Stuttering in \alloy{} may be modelled explicitly, by writing a
transition that constrains some or all of the variables to remain
unchanged.

In \tla, the transition relation is defined mostly explicitly.  By
convention, the transition relation is a predicate \tlacode{Next}
defined as the disjunction of all of the model's transition
predicates, which is the method best supported by \tlc, the
accompanying model checker for \tla.  Though in \tla{} one could write
models not using disjunctions to join the transition predicates,
\tlc{} is not optimized to handle such models as well, because it
rewrites the transition relation as a disjunction of as many simple
subactions as possible~\cite{DBLP:conf/charme/YuML99}.  If $TR$ is not
a disjunction, two possible issues arise: First, from a debugging
perspective, the visualizer will \emph{not} show $TR$ as a composition
of smaller transition predicates, thereby making it harder to reason
about the model and its behaviour.  Second, from a model checking
performance perspective, \tlc{} spawns a worker thread for each
subaction to explore the snapshot space, but because $TR$ was
\emph{not} broken down into smaller subactions, \tlc{} may not spawn
an optimum number of worker threads.  For predicates taking one or
more arguments, existential quantification over the corresponding
set(s) may be used to bind an element from that set and pass to the
predicate.  \tla{} has implicit stuttering, and stuttering steps may
occur between any two transitions, including when the system has not
reached a deadlock.  This implicit addition of stuttering to $TR$ does
not change the meaning of a model, since all \TLA{} formulas are
invariant under stuttering (\emph{i.e.}  adding or removing stuttering
steps does not affect whether or not a behaviour satisfies a temporal
formula).

In \asmetal, the transition relation $TR$ is defined mostly explicitly
using a special \asmcode{rule} named \asmcode{r_Main}, the \emph{main
rule}.  The main rule is by convention broken down into smaller rules,
each a transition.  The main rule specifies when and how each
transition will be called.  \asmetal{} is more of an imperative-style
language (though it does include various declarative, constraint-like
expressions and rules, which is why we chose to include it in our set
of languages), and does not support defining the transition relation
as a disjunction of multiple transitions like the other languages with
explicit $TR$ representation do.  Thus, 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 can be cumbersome and error-prone in a model with a large
number of transitions, since the modeller may forget to update the
\asmcode{switch} cases when adding or removing transitions.
Stuttering in \asmetal{} can be added explicitly, using the
\asmcode{skip} rule, as well as occurring implicitly in the case of a
deadlock, which happens when the update set corresponding to a
transition is empty (\emph{i.e.} no variable assignments in the
transition) or when the update set is inconsistent (\emph{i.e.} there
are conflicting assignments to the same variable, one form of which is
simultaneous assignment to the same variable in a \asmcode{par}allel
block, as shown on Figure~\ref{fig:control/incon-upd-asmetal}).
Implicit stuttering in an \asm{} allows changes to the monitored
variables by the environment, so as to enable potential further
progress of the transition system~\cite{DBLP:conf/sam/Sherratt12}.
This stuttering behaviour added implicitly to $TR$ also ensures that
$TR$ is total.

\input{figure/control-incon-upd-asmetal}
\input{figure/control-tr}

The remaining languages \md \B, \eventb, \pluscal, and \dash \md each
have an explicit construct for defining transitions, which are
implicitly composed together to form a transition relation.  In each
language, only one transition is allowed to be taken in each step, and
all different interleavings of the transitions are considered for
modelling concurrency.

The transition relation in \B, \eventb, and \pluscal{} is implicitly
formed as follows: at any step, any transition whose precondition is
satisfied (\emph{i.e.} is enabled) may be chosen to be taken.  There
is no requirement on the preconditions of the transitions to be
non-overlapping, and more than one transition may be enabled at the
same time, resulting in a branch in the snapshot space graph.  In the
remainder of this section, we will refer to this formation of $TR$ as
$TR_{IMP}$.

In \B, the transition relation is implicitly formed, per $TR_{IMP}$,
and is a composition of transitions, referred to as operations in \B,
which may have zero or more preconditions, and one or more
substitutions from which postconditions may be derived.  A stuttering
step in \B{} must be represented explicitly, using the \bcode{skip}
generalized substitution \md also referred to as the identity
substitution \md which takes no action.

In \eventb, the transition relation is formed implicitly, per
$TR_{IMP}$, and consists of transitions, referred to as events in
\eventb, which may have zero or more preconditions, and one or more
actions from which postconditions may be derived.  In \eventb, a
stuttering step must be denoted explicitly, using a \eventbcode{skip}
event, which is a transition that is always enabled (its guard is
\eventbcode{TRUE}) and does nothing (it has no actions).

In \pluscal, the transition relation is formed implicitly, per
$TR_{IMP}$, wherein the transitions are implicitly disjoined together,
A stuttering step in a \pluscal{} algorithm may be represented
explicitly in a \pluscalcode{process}, using the \pluscalcode{skip}
atomic instruction, or implicitly, between any two \pluscal{} steps
(defined in Section~\ref{sec:control/trans} below).  Since \pluscal{}
specifications are ultimately translated to \tla{} and checked by
\tlc, one may opt to not use the automatically generated transition
relation and write their own.  In the next section, for \pluscal{} we
will look at how transitions are created from the
\pluscalcode{process} descriptions.

In \dash, the transition relation is formed implicitly following the
semantics of concurrent, hierarchical state machines.  For a
transition to be taken, the snapshot must include the source state of
the transition, and transitions exiting states at a higher level in
the hierarchy have priority over lower states.  Particularly distinct
from the other languages is the concurrent and hierarchical states
found in a \dash{} model.  Because of this concurrency, \dash{} makes
the distinction between big steps and small steps in the transition
relation, as shown in Figure~\ref{fig:control/dash-steps}.  Big steps
consist of multiple small steps, which are each one transition.  In a
big step, at most one transition per concurrent region can be taken.
Monitored (\dashcode{env}ironmental) events can change only at big
step boundaries (called a stable snapshot), so the occurrence of a
monitored event can trigger multiple transitions as long as the
transitions are in different concurrent regions.  Events generated by
one transition can trigger other transitions (in different concurrent
regions) within the same big step.  Implicit stuttering in \dash{}
happens only at the big step boundaries, when no more transitions may
be taken.  For stuttering when one or more transitions are enabled, an
explicit stuttering transition must be used.

\input{figure/control-dash-steps}


\section{Transitions}
\label{sec:control/trans}

This section describes how each language can represent a transition
$T$ of a transition system.  As we are working with declarative
modelling languages, each transition describes a set of pairs $(s, s')
\in T$.  To create a transition $T \subseteq TR \subseteq S \times S$ we may use two-snapshot
predicates, assignment operators, or both; depending on the language.
A predicate corresponding to a transition $T$ describing a set of
pairs $(s, s') \in T$ can be broken down into $pre_T$ on the source
snapshot and $post_T$ on the source and destination snapshots,
combined using some logical connective $\qqm$, as shown in
Figure~\ref{fig:control/trans/t}.  The transition may only be taken
when $pre_T$ is true.  Each of $pre_T$ and $post_T$ may in turn
consist of one or more explicit language constructs.
\input{figure/control-trans-t}
The preconditions $pre_T$ of the transition may consist of guards
$guard_T$, a source labelled control state $src_T$, and triggering
event $evt_T$; and the postconditions $post_T$ may consist of actions
$act_T$, destination control state $dest_T$, and generated events
$genevt_T$, constraining the snapshot and variables after the
transition is taken.  We will describe the languages in increasing
order of explicit language constructs for describing a transition.
Figure~\ref{fig:control/trans} shows exemplars for declaring transitions
in each language.

\alloy{} does not have a special construct for defining transitions.
Commonly, a transition is modelled as a predicate \md defined using
the \alloycode{pred} keyword \md over unprimed and primed variables,
constraining the value of the variables in the source and destination
snapshots.  Unlike the other languages, primed variables do not carry
any special meaning in \alloy, and are used as a common modelling
convention.  Though a transition may be represented using a single
predicate, Farheen's guidelines~\cite{farheen2018} separate a
transition definition into two separate predicates \md one for
preconditions over the variables in the source snapshot, and another
for postconditions over the variables in the source and destination
snapshots \md to promote structure.  Commonly, the pre and post
predicates for each transition are conjoined together to form the main
transition predicate (\emph{i.e.} $\qqm$ in
Figure~\ref{fig:control/trans/t} would be $\wedge$), and the transition
predicates are then disjoined together to form the transition
relation.  This is referred to as the \emph{disjunctive modelling
  method} in Farheen's guidelines.  The guidelines recommend this
method for decomposing the transition relation and transitions of a
transition system because using this method, adding a transition does
not change the behaviour of other existing transitions, and is thus
more likely to produce a transition relation expected by the modeller.
With respect to the frame problem, in \alloy{} any variable not
constrained in a transition predicate may change nondeterministically
from the source to the destination snapshot, and there is no
distinction between monitored and controlled variables.

In \tla, a transition (an \emph{action} in \tla{} terminology) is a
two-snapshot predicate over unprimed and primed versions of all
variables, constraining each variable in the source and destination
snapshots.  Similarly to \alloy, in \tla{} a transition may be further
broken down into separate pre and post parts for clarity.  The
preconditions of a transition are commonly a series of one or more
conjoined formulas over unprimed variables in the source snapshot and
optionally over the transition arguments if any, and the
postconditions or actions of a transition are conjoined formulas over
primed and unprimed variables, constraining each variable in the
destination snapshot.  The pre and postconditions are often conjoined
together, \emph{i.e.} $\qqm$ in Figure~\ref{fig:control/trans/t} would
be $\wedge$.  With regards to the frame problem, \tla{} requires that all
transitions constrain the value of every variable, either by
constraints on the primed and unprimed variables or by marking them
with the \tlacode{UNCHANGED} keyword.  \tla{} does not make a
distinction between monitored and controlled variables.

\asmetal{} does not have any construct for decomposing a transition
into separate pre and post parts; and a transition definition consists
only of an action \md a \asmcode{rule} in \asmetal{} terminology.  An
action may be one of several rules, producing a set of assignments to
\asmcode{controlled} variables.  The transition rule may be a simple
rule such as the \asmcode{skip} rule or the update rule (\emph{i.e.}
variable assignment, using the \asmcode{:=} operator), or a more
complex rule such as \asmcode{par}allel or \asmcode{seq}uential block,
\asmcode{if}, \asmcode{case}, \asmcode{forall}, \asmcode{choose},
\emph{etc.}, which enables composition and combinations of other rules
together.  A transition in \asmetal{} does not have preconditions on
when it may be taken, and conditional rules such as \asmcode{if} and
\asmcode{case} are used to constrain the action(s) of the transition.
These differ from preconditions in that their use does not impact
whether or not a transition is enabled (in \asmetal, all transitions
of a model are always enabled).  In \asmetal, for $(s, s') \in T$ the
transformation of $s$ to $s'$ is defined as the effect of applying as
an atomic step the result of a consistent update set (one with no
conflicting variable assignments) on $s$.  With respect to the frame
problem, any controlled variable not assigned to in a transition is
unchanged by that transition, and retains its value from the source
snapshot.

In \B, a transition is referred to as an \emph{operation}, each
consisting of one or more actions \md called a \emph{generalized
substitution} \md which may take several forms (see Chapter~6
of~\cite{b-manref} for an exhaustive list of the forms).  An action
may be a compound substitution \md such as a block substitution
(\bcode{BEGIN S END}) or a preconditioned substitution (\bcode{PRE P
  THEN S END}) with precondition \bcode{P} required to be true before
calling the operation (otherwise the operation will not be enabled and
cannot be executed) and \bcode{S} the body of the substitution \md or
a simple one like `$:=$' (becomes equal), `$:\in$' (becomes part of), or
`$:\!(\,)$' (becomes such that).  The simpler substitutions can either
be the entire body of a substitution, or be used in one of the
compound substitutions like the ones mentioned above.  Note that
`$:=$' and `$:\in$' are used similar to assignment in typical
programming languages, whereas with `$:\!(\,)$' the modeller may refer
to the value of the variable before substitution (in the source
snapshot) using the \bcode{$0} suffix.  For example, \bcode{x$0} would
refer to the value of \bcode{x} in the source snapshot, and \bcode{x}
to its value in the destination snapshot.  With respect to the frame
problem, in \B{} any variable not assigned to in a substitution
retains its value and is unchanged by that transition.  \B{} does not
distinguish between monitored and controlled variables.

In \eventb, a transition is referred to as an \emph{event}, and is a
simplification of a \B{} \emph{operation}.  In contrast to \B, in
\eventb{} a transition has only one general form, consisting of one or
more of the following parts: parameters, guards, and actions.  A
\emph{guard}, defined in the \eventbcode{WHERE} clause of the
transition and the only form of precondition in \eventb, is the
precondition required to be true for the transition to be enabled.  A
transition may have an arbitrary number of \emph{parameter}s.  Like a
snapshot variable, each parameter has a type \md which must be
declared as a guard of that transition \md and a unique name.  An
\emph{action}, consisting of an assignment, describes how the source
and destination snapshots relate, and is a simplification of \B's
generalized substitutions.  Each action has a label, used for
identifying and/or referring to that action.  Labels are used
throughout \eventb{} tool support, and are useful for identifying the
role/kind of a construct involved in a machine or proof about the
machine.  By convention, an action label starts with the \emph{act}
prefix, and a guard label starts with the \emph{grd} prefix.  An
\eventb{} assignment operator is either deterministic or
nondeterministic.  The `$:=$' operator is for deterministic assignment
of the right-hand side value to the left-hand side variable, `$:\in$'
for nondeterministic assignment of an element of the right-hand side
set to the left-hand side variable, and `$:\!|$' for
(nondeterministically) constraining the value of the left-hand side
variable with the before-after predicate (a two-snapshot predicate
over unprimed and primed variable names) given on the right-hand side.
Similarly to \B, `$:=$' and `$:\in$' are used without primed variables,
and `$:\!|$' is used with primed version of variables referring to
their value in the destination snapshot.  Regarding the frame problem,
similarly to \B, in \eventb{} any variable not assigned to using an
assignment operator is unchanged by the transition and retains its
value.  No distinction is made between monitored and controlled
variables in \eventb.

In \pluscal, we can leverage the language's constructs for expressing
concurrency and nondeterminism to model a transition system in the
form of an algorithm.  Similar to a programming language, \pluscal{}
has a control flow semantics that defines the meaning for the
algorithm text and how it may be executed.  When modelling a
transition system in \pluscal, a single-\emph{step}
\pluscalcode{process} will be a transition in the resulting transition
system.  The preconditions of a transition are specified using an
\pluscalcode{await} (or \pluscalcode{when}) statement which acts like
a guard, allowing the process body to be executed only when the guard
expression evaluates to \pluscalcode{TRUE}.  In \pluscal, a single
\emph{step}, referred to as an atomic action, corresponds to the
execution of the statements contained between one \emph{label} and the
next.  A label is an identifier marking a location in a \pluscal{}
algorithm, similar to a label in a traditional programming language
like C.  An algorithm has a program counter pointing to the current
label being executed, and may be thought of as corresponding to
non-hierarchical control states.  Since normally the body of a
\pluscal{} process is executed only once, whereas a transition in a
transition system may be taken any number of times as long as it is
enabled, we add a \pluscalcode{goto} statement at the very end of each
process to jump back to the label at the very beginning of that
process, allowing the process to be taken again.  In addition to
global (\pluscalcode{algorithm}-wide) variables, each \pluscal{}
\pluscalcode{process} may have local variables declared using the
\pluscalcode{variables} keyword.  A local or global variable \emph{x}
can be initialized to \emph{expr} using a declaration of the form
\pluscalcode{variable\ }\emph{x}\pluscalcode{\ =\ }\emph{expr}.  In
process body, variables may be assigned to using the \pluscalcode{:=}
operator, and will otherwise retain their value from the source
snapshot.  \pluscal{} does not distinguish between monitored and
controlled variables.

\dash{} is the language with the most language constructs for
modelling a transition of a transition system studied in this thesis.
A transition in \dash{} is defined using the \dashcode{trans} keyword,
optionally consisting of the parts described below.  The preconditions
of a \dash{} transition may be divided into three parts:

\begin{enumerate}
\item The guard condition of the transition, denoted using the
  \dashcode{when} keyword, which is an \alloy{} expression over the
  snapshot variables that when true the transition would be enabled.
\item The source labelled control state of the transition, denoted
  using the \dashcode{from} keyword.  Since \dash{} has explicit
  control state representation using \dashcode{state} blocks, labelled
  control state blocks may be nested to form a \textsc{control state
    hierarchy}, useful for grouping related states together.  In the
  absence of an explicit \dashcode{from} part, the most immediate
  state containing the transition definition will be used as the
  source labelled control state of that transition.
\item The event triggering the transition, denoted using the
  \dashcode{on} keyword, for triggering the transition whenever a
  certain event is fired.  Events are useful for modelling broadcast
  communication and cascading effects.  The (optional) \dashcode{on}
  part indicates the name of the event triggering the transition.
\end{enumerate}

The postconditions of a \dash{} transition may be divided into three
parts:

\begin{enumerate}
\item The actions of the transition, denoted using the \dashcode{do}
  keyword, are two-snapshot \alloy{} expressions over unprimed and
  primed variables describing the value of each variable in the
  destination snapshot, modelling the effects of executing the
  transition.
\item The destination labelled control state of the transition,
  denoted using the \dashcode{goto} keyword.  In the absence of an
  explicit \dashcode{goto} part, the most immediate state containing
  the transition definition will be used as the destination labelled
  control state of that transition.
\item The generated events, denoted using the \dashcode{send} keyword,
  for firing one or more events upon the execution of the transition.
  The (optional) \dashcode{send} part denotes the name of an event or
  a set of comma-separated events to be generated when the transition
  is taken.
\end{enumerate}

\dash{} semantics define two kinds of steps: \emph{big steps} and
\emph{small steps}.  A big step consists of one or more sequential
small steps meant to represent the transition system reacting to the
external environment or its own internal changes.  Each small step
corresponds to a transition, and small steps are taken until the
system cannot take anymore transitions, at which point it is said to
have become \emph{stable}.  With respect to the frame problem,
monitored variables (marked with \dashcode{env}) in \dash{} are
allowed to change from one snapshot to the next when the next snapshot
is stable (\emph{i.e.} at the big step boundaries), and will otherwise
retain their values from the source snapshot.  For controlled
variables, if the primed version is mentioned in the action of a
transition, it is assumed that the action will constrain it;
otherwise, they are forced to retain their value from the source
snapshot.

\input{figure/control-trans}


\section{Invariants}
\label{sec:control/invs}

This section describes how invariants for a transition system are
represented in each language.  An invariant of a transition system is
a formula that is true in every snapshot of the transition system.  In
other words, an invariant must hold in the initial snapshot and after
every transition.

In \B{} and \eventb, invariants are written in the \bcode{INVARIANT}
and \eventbcode{INVARIANTS} section of a machine respectively.  In a
model checking setting, \emph{e.g.} using ProB, the invariants are
checked to hold in every snapshot.  In a theorem proving setting, the
invariants must be proven to be established by the initialization, and
be preserved by every transition.

In \alloy{} and \dash, invariants are written in \alloycode{fact}
blocks.  \dash{} additionally has \dashcode{invariant} blocks.  In
both languages, invariants are constraints on snapshots and limit the
reachable snapshot space of the model.

In \tla{} and \pluscal, invariants are defined as \tla{} predicates.
In a model checking setting, these predicates must be added to the
\texttt{Invariants} portion of the \tlc{} settings for the model,
which will then be checked to hold in every snapshot.  In a theorem
proving setting, invariants appear as consequent of an implication in
a \tlacode{THEOREM}.

In \asmetal, invariants are defined using the \asmcode{invariant over}
keywords, in the \asmcode{definitions} section of an \asm{} after the
\asmcode{rule} (transition) definitions.  \asmetal{} invariants are
verified to hold in every snapshot of the model during analysis
(\emph{e.g.} animating or model checking).


\section{Fairness}
\label{sec:control/fairness}

This section describes how fairness constraints~\cite{lamportslf2019,
  DBLP:journals/scp/AptO83, DBLP:journals/toplas/Lamport94} for a
transition system are represented in each language.  A fairness
constraint is a condition on the snapshot traces of a transition
system model.  A trace is said to be fair with respect to a formula if
and only if it satisfies the formula.  There are two kinds of fairness
constraints: weak fairness (also referred to as justice) and strong
fairness (also referred to as compassion).  In a declarative modelling
language, fairness constraints can either be used to limit the model
to include only ``fair'' traces, or as part of the properties to limit
the traces on which a property is evaluated.  In this work, we are
only interested in the former.

In \B, \eventb, \alloy, and \dash{} fairness constraints are not part
of the transition system model, but rather part of the properties to
be checked.

In \tla, weak or strong fairness for transitions can be added to the
specification of the transition system using the \tlacode{WF} and
\tlacode{SF} operators respectively.  If a transition with weak
fairness is always enabled, it will eventually be taken.  If a
transition with strong fairness is enabled infinitely often, it will
eventually be taken.

In \pluscal, a \pluscalcode{process} can be marked as weakly fair
using the \pluscalcode{fair} keyword, or strongly fair using
\pluscalcode{fair+}.  Further, for a \pluscal{} label \pluscalcode{A:}
in an unfair process, \pluscalcode{A:+} marks the label as weakly
fair; and for a label \pluscalcode{A:} in an weakly fair process,
\pluscalcode{A:+} makes it strongly fair.  In both cases,
\pluscalcode{A:-} marks the label as unfair.  The notion of weak and
strong fairness in \pluscal{} match those of \tla.

In \asmetal, for a Boolean formula \asmcode{f}, \asmcode{JUSTICE f}
imposes weak fairness and requires that \asmcode{f} be true infinitely
often.  For two Boolean formulas \asmcode{f} and \asmcode{g},
\asmcode{COMPASSION (f, g} requires that if \asmcode{f} is true
infinitely often then \asmcode{g} be true infinitely often as well
(the missing closing parenthesis is intentional and part of the
\asmetal{} grammar).  \asmcode{JUSTICE} and \asmcode{COMPASSION} must
be used in the \asmcode{definitions} section of an \asm{}, after the
\asmcode{rule} (transition) definitions but before any of the
\asmcode{invariant}s and the \asmcode{main rule}.


\section{Discussion on Inconsistency}
\label{sec:control/incon}

In declarative models, inconsistency stems from contradictions in
logical formulas.  All languages allow inconsistencies and there is no
distinguishing comparison criteria.  However, it is important to
understand the effects of these inconsistencies in models.  In the
context of declarative transition systems, we consider three kinds of
inconsistency that may occur in the description of a transition
system:
\begin{itemize}
\item \textbf{Contradictory transition postcondition}: when the
  logical formula corresponding to the postcondition of a transition
  is a contradiction.  One possible form of contradictory transition
  postconditions is simultaneous assignment (also sometimes referred
  to as parallel assignment) to the same variable in a transition.
  Having a contradictory transition postcondition is possible in all
  languages.
\item \textbf{Contradictory transition relation}: when the logical
  formula corresponding to the transition relation, $TR$, is a
  contradiction (\emph{i.e.} is never true), and therefore there does
  not exist a snapshot trace satisfying the constraints of $TR$'s
  definition.  In \B, \eventb, \pluscal, and \dash, one cannot create
  a contradictory $TR$ explicitly, since the transition relation of
  the model is created implicitly from the elements described by the
  modeller, and the above languages do not have an explicit language
  construct for defining $TR$ in the model text.  However, it may
  still be possible to create a contradictory transition relation
  indirectly if there are inconsistencies in these elements, and
  having a contradictory transition relation is possible in all
  languages.
\item \textbf{Deadlock}: refers to a snapshot that has no explicitly
  modelled outgoing transitions.  In the absence of
  \textbf{stuttering} steps in a declarative modelling language, this
  means a non-total transition relation.  Some languages perform
  implicit stuttering steps when a transition system reaches a
  deadlock, thereby ensuring the totality of the transition relation
  and enabling potential further progress of the transition system.
  Another method for ensuring the totality of a transition relation is
  making the transition preconditions complete; \emph{i.e.}  setting
  up the transitions such that the disjunction of the preconditions of
  all transitions combined is true.
\end{itemize}

It is possible to write contradictory transition postconditions in
\alloy{} and \dash{} that possibly result in a contradictory $TR$
(when no other transition is enabled).
Figure~\ref{fig:control/incon-dash-contra-postcond} is an exemplar of
a transition system with a contradictory transition postcondition.  In
both \alloy{} and \dash{} it is possible to have a contradictory $TR$
for which no satisfying instances exist.  In \alloy, $TR$ is written
explicitly by the modeller and thus may be the direct source of
inconsistency; whereas in \dash, $TR$ is constructed implicitly, and
$TR$-related inconsistencies would be those trickling up from the
individual transitions.  For instance, in \dash{} a contradictory
(false) transition postcondition leads to a contradictory $TR$; and
even though \dash{} has implicit \textbf{stuttering} at the big step
boundaries, they only happen when all the transition preconditions are
false, and will not help when a transition's precondition is true but
its postcondition is false.  In \alloy, it is possible to have a
non-total transition relation that reaches a deadlock wherein no
transitions can be taken.

\input{figure/control-incon-dash-contra-postcond}

Inconsistency in \tla{} comes in several forms.  The simplest is an
obviously false specification \md for instance $Init \triangleq 1 = 2$, or
$Init \triangleq a \in \varnothing$ \md which results in \tlc{} errors like ``The
spec is trivially false because Init is false'' or ``Init is never
enabled'' \md which can be an instance of the contradictory transition
postcondition or contradictory transition relation categories of
inconsistencies.  In \tla, a contradictory transition postcondition
results in that transition never being enabled.  It is also possible
to write a transition relation that eventually reaches a deadlock, as
well as writing a contradictory $TR$ for which no satisfying instance
exists.

In \asmetal, it is possible to write a transition relation for an
\asm{} that eventually reaches a deadlock.
Figure~\ref{fig:control/incon-asmetal-deadlock} is an example of an
\asm{} that eventually reaches a deadlock (when \asmcode{v = 3}).  The
interpretation of the deadlock depends on the tooling used: for
instance, the interactive runner for Asmeta considers the deadlock
snapshot the end of execution and will terminate the run when that
snapshot is reached, whereas the Asmeta animator will \textbf{stutter}
infinitely when the deadlock state is reached.

\input{figure/control-incon-asmetal-deadlock}

In \B{} and \eventb, a transition with a contradictory postcondition
(\emph{e.g.} an action/substitution like $x :\in \varnothing$ that is
always false) is effectively never enabled (same as a transition with
a false precondition), and the transition system would thus reach a
deadlock if no other transition is enabled.  In
Figure~\ref{fig:control/incon-b-eventb-deadlock}, the transitions
\bcode{contra_pre} and \bcode{contra_post} in both \B{} and \eventb{}
are always disabled and each transition system is deadlocked.  Both
\B{} and \eventb{} employ static checks as part of their type system
to catch various modelling errors like type mismatches (\emph{e.g.}
$\text{\bcode{a}} = \varnothing$ in the above exemplar) or simultaneous
assignment to the same variable (\emph{e.g.} \bcode{a := a1; a := a2})
in the same transition.

\input{figure/control-incon-b-eventb-deadlock}

For \pluscal, the general conditions described for \tla{} above apply
to \pluscal{} models as well.  However, \pluscal{} has additional
safeguards to make certain kinds of inconsistency unrepresentable in
valid models.  This is achieved by using \pluscal{} \emph{labels} to
impose restrictions on valid statements and expressions.  For
instance, each labelled section may only contain at most one
assignment statement for each variable.  This eliminates a case of
contradictory transition postcondition corresponding to the logical
formula $a' = b \wedge a' = c$ where $b \neq c$.
Figure~\ref{fig:control/incon-pluscal-contra-postcond} shows an
example of this, and \pluscal{} will show an error about a missing
label between lines \ref{lbl:control/incon-pluscal-a-2} and
\ref{lbl:control/incon-pluscal-a-3}.

\input{figure/control-incon-pluscal-contra-postcond}


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