F1.3.1.1.  Overview

An abstract state machine (ASM) is a model of computation that treats first-order structures as dynamic entities whose states can change during a computation.

An abstract state machine has a set of states $S$, a subset of initial states $S_0\subseteq S$ and a function $\tau :S\to S$, called the one-step transformation. Every state is a first-order structure. All the states of an ASM have the same signature, which is also called the signature of the ASM, and all the states have the same base set, called the base set of the ASM. $\tau$ does not change the base set, but it does, in general, change the equivalences that hold between terms of the signature.

The behaviour of an abstract state machine is modelled as a run or sequence of states. A run starts with an initial state, and each subsequent state is derived from its predecessor by application of the one-step transformation. Each application of the one-step transformation is called a move.

	$\tau$		$\tau$		$\tau$		moves
$s_0\in S_0$	$\to$	$s_1$	$\to$	$s_2$	$\to$	$\dots$	states

F1.3.1.2.  States

The base set of the abstract state machine, which is the base set of every state of the ASM, contains three distinct elements: true, false and undefined. The base set also contains an infinite number of reserve elements. A state also has functions and predicates that are defined over the base set. All functions are total, with undefined being used to mimic partial functions. Predicates are functions whose only possible values are true or false. Special unary predicates called domain names identify members of the base set as belonging to particular domains. This allows states to be viewed as many-sorted structures.

Embedded within a state are certain substructures or background classes [b-Blass] and [b-Blass 2008]. One such background includes true, false, the domain name Boolean and the Boolean operators. The backgrounds used in modelling SDL-2010 include numbers, sets and sequences. A minimal background is defined in [b-Blass] and [b-Blass 2008] to characterize the ASMs that model parallel algorithms.

F1.3.1.3.  One-step transformation

The one-step transformation $\tau$ updates the values of functions. In general, for $s\in S$, some equivalences hold in $s$ but not in $\tau \left(s\right)$ and vice versa. In some cases, τhas no effect, so $s$ and $\tau \left(s\right)$ are the same.

To express the relationship between $s$ and $\tau \left(s\right)$ more precisely, the changes effected by τare described in terms of an update set. An update set $\Delta$ is a set of triples $<f,\left[a\right],b>$ where $f$ is a function symbol, $\left[a\right]$ is a tuple of elements of the base set of the abstract state machine that respects the arity of $f$, and $b$ is an element of the base set. The relationship between $s$ and $\tau$ is expressed by stating that $\Delta$ contains all information of the form $f\left[a\right]=b$ that is not true in the state $s$ but is true in $\tau \left(s\right)$ [b-Blass].

The pair $<f,\left[a\right]>$ is also called a location of a state $s$. This captures the idea of updating the value of a variable in a conventional imperative programming language. A member $<f,\left[a\right],b>$ of an update set is also known as an update and may be written $f\left[a\right]≔b$ to reinforce the idea of variable assignment.

An abstract state machine provides a model of computation for an algorithm that is expressed as a program using a programming-style syntax. The algorithm defines the update set for every state of the ASM. To facilitate the study of the kinds of algorithms captured by different kinds of ASM, axioms [b-Blass] have been developed to define classes of ASMs in a syntax-independent way [b-Glausch]. As well as capturing the ideas of state and one-step transformation outlined above (the Sequential Time and Abstract State postulates, [b-Blass] and [b-Gurevich 2000]), axioms aim to capture the idea that the amount of computation required to move from $s$ to $\tau \left(s\right)$ must be bounded, where the bound depends only on the algorithm and not on the state.

F1.3.1.4.  Specifying an abstract state machine

An ASM specification consists of a set of declarations that define its vocabulary (signature), its initial state(s) and a transition rule that defines the one-step transformation $\tau :S\to S$. The transition rule, called the ASM program, is defined using a pseudo-code-like syntax based on terms of the signature.

F1.3.1.5.  Specifying the signature (vocabulary)

An ASM signature comprises function names, predicate names and domain names. Names in the signature have a specified arity, and are interpreted over the base set of the states of an ASM. The interpretation of names respects their arity.

The following notational conventions are used when declaring names.

• Domain names start with an uppercase letter and presented in small-capitalized italics (as in Agent), except when denoting a non-terminal of the SDL-2010 abstract grammar. In that case, domain names are written as the SDL-2010 non-terminals, i.e., in italics, hyphenated, and starting with an uppercase letter (as in Agent-definition). A domain name $D$ is declared by domain $D$. A domain name is interpreted as a unary predicate which yields true for the members of the base set that belong to the domain.

• Function names are written in italics starting with a lowercase letter (as in mode). A function name $f$ is declared by $f:D_1\times D_2\times \dots \times D_n\to D_0$ , where $n$ is the arity of $f$, and $D_0$, $D_1$, $D_2\dots D_n$ are domain names. A function name is interpreted as a function over the base set. The interpretation respects the arity of $f$.

• Predicate names that are not Domain names are also written in italics (as in available). A predicate name $p$ is declared by $p:D_1\times D_2\times \dots \times D_n\to$ Boolean. A predicate is interpreted as a function whose value is either true or false.

Declarations also include qualifiers, which specify further restrictions on their interpretation. Qualifiers on name declarations constrain interpretation of the one-step transformation.

• Static names are qualified by the keyword static. A name that is declared static has the same interpretation in every state of an ASM. This means that the one-step transformation cannot update a static name. So the interpretation of a static domain name yields true for the same elements in every state, and a static function name yields the same value for a given argument tuple in every state of an ASM.

• Dynamic names are qualified by one of the keywords controlled, shared or monitored. The one-step transformation can change the value of the interpretation of a dynamic name. A dynamic function can yield different values for a given set of arguments in different states of an ASM. An ASM can be subject to external environmental influences. ASM agents can communicate [b-Glässer 2007]. When any of these situations is specified, the keywords controlled, shared and monitored constrain visibility and updates of domains, functions and predicates.

The static domain names Agent, Token and Mode are introduced to represent the (single) agent of the system, the set of tokens, and the different access modes (exclusive, shared), respectively. The names mode and owner denote dynamic functions; they are used to model the current access mode of an agent and the current owner of a token, respectively. The 0-ary function name ag refers to a value of the domain Agent. idle, waiting, busy, and available are names of derived, dynamic predicates. stop denotes a monitored predicate, which will be explained later.

The vocabularies we will consider also include predefined names, which include all the items in the background classes of the ASM. These include the equality sign, the 0-ary predicate names true, false and undefined, the domain names Boolean, Nat and Real, as well as the names of frequently used standard functions (such as Boolean operations $\wedge ,\vee ,\neg ,\Rightarrow ,\Leftarrow$, and set operations $\subseteq ,\cup ,\cap ,\in ,\notin$, etc.). The full collection of predefined names is listed in clause F1.3.6. Interpretation of predefined names is constrained to the usual meanings of those names.

The notational conventions described above enable declaration of basic names that are interpreted directly over the ASM base set. As well as basic names, the signature of an ASM may include derived names, whose interpretation depends on the interpretation of the basic names. Derived names are defined using logical formulae involving other names. The interpretation of a derived name is determined by the interpretations of those other names, and ultimately by the interpretation of base names.

Let derivedName be an n-ary name, and let formula($v_1,\dots ,v_n$) denote a formula of the domain $D$ with free variables $v_1,\dots ,v_n$ of domains $D_1,\dots ,D_N,n\ge 0$. The general form of a derived name definition is:

The result domain $D$ is omitted in case of a derived domain definition.

An agent a is, for instance, idle if the function mode yields the value undefined for that agent, and a does not hold any token. A token $t$ is available if no agent is holding $t$.

For an improved readability, use of the "." -notation is allowed for unary functions and predicates. For instance, a.mode is equivalent to mode(a).

F1.3.1.6.  Initial states

The set of initial states $S_0\subseteq S$ is defined by constraints imposed on domains, functions and predicates as associated with the names in $V$. The initial constraints for predefined domains and operations are given implicitly (see clause F1.3.6). Initial constraints have the following general form:

The first constraint defines the initial set Agent to consist of a single element ag. The second constraint expresses that initially, the agent of RMS is idle (a.mode = undefined), and all tokens are available (t.owner = undefined). Note that no constraint on stop is defined.

F1.3.1.7.  State transitions and runs

A (global) state $s\in S$ is given by an interpretation of the names in $V$ over the base set of $M$. State transitions can be defined in terms of partial reinterpretations of dynamic domains, functions and predicates. This gives rise to the notions of location as a conceptual means to refer to parts of global states, and of update to describe state changes.

A location of a state $s$ of $M$ is a pair $lo{c}_s=<f,s\left(x\right)>$, where $f$ is a dynamic name in $V$, and $s\left(x\right)$ is a sequence of elements of the base set according to the arity of $f$. An update of s is a pair ${\delta }_s=<lo{c}_s,s\left(y\right)>$, where $s\left(y\right)$ identifies an element of the base set as the new value to be associated with the location $lo{c}_s$. To fire ${\delta }_s$ means to transform $s$ into a state $s\prime$ of $M$ such that $f_{s\prime }\left(s\left(x\right)\right)=s\left(y\right)$, while all other locations $lo{c}_s\prime$ of $s$, $lo{c}_s\prime \ne lo{c}_s$, remain unaffected. In other words, firing an update modifies the interpretation of a state in a well-defined way.

The potential behaviour of a basic ASM is captured by a program $P$, which is defined by a transition rule (see clause F1.3.1.8 and clause F1.3.1.10). For each state $s\in S$, a program $P$ of $M$ defines an update set ${\Delta }_s\left(P\right)$ as a finite set of updates of $s$. ${\Delta }_s\left(P\right)$ is consistent, if and only if it does not contain any two updates ${\delta }_s,\delta {\prime }_s$ such that ${\delta }_s=<lo{c}_s,s\left(y\right)>$, $\delta {\prime }_s=<lo{c}_s,s\left(y\prime \right)>$, and $s\left(y\right)\ne s\left(y\prime \right)$. The firing of a consistent update set ${\Delta }_s\left(P\right)$ in state $s$ means to fire all its members simultaneously, i.e., to produce (in one atomic step) a new state $s\prime$ such that for all locations $lo{c}_s=<f,s\left(x\right)>$ of $s$, $f_{s\prime }\left(s\left(x\right)\right)=s\left(y\right)$, if $<<f,s\left(x\right)>,s\left(y\right)>\in {\Delta }_s\left(P\right)$, and $f_{s\prime }\left(s\left(x\right)\right)=f_s\left(s\left(x\right)\right)$ otherwise, and is called state transition. Firing an inconsistent update set has no effect, i.e., $s\prime =s$.

The behaviour of a single-agent ASM $M$ is modelled through (finite or infinite) runs of $M$, where a run is a sequence of state transitions of the form:

	${\Delta }_{s0}\left(P\right)$		${\Delta }_{s1}\left(P\right)$		${\Delta }_{s2}\left(P\right)$		moves
$s_0$	$\to$	$s_1$	$\to$	$s_2$	$\to$	…​	states

such that $s_0\in S_0$, and $s_{i+1}$ is obtained from $s_i$, for $i\ge 0$, by firing ${\Delta }_{si}\left(P\right)$ on $s_i$, where ${\Delta }_{si}\left(P\right)$ denotes an update set defined by the program $P$ of $M$ on $s_i$ (see clause F1.3.1.10). The meaning of an ASM is defined to be the set of all its runs. In the sequel, we restrict attention to runs starting in an initial state, also called regular runs.

F1.3.1.8.  Transition rules

Transition rules specify update sets over ASM states. Complex rules are formed from elementary rules using various rule constructors. The elementary form of transition rule is called update instruction.

• update instruction

Here, $f$ is a non-static name of $V$ denoting either a controlled or a shared function, predicate or domain, and $t_0,t_1,\dots ,t_n$ are terms over $V$ identifying, for a given state $s$, the location $loc=<f,<s\left(t_1\right),\dots ,s\left(t_n\right)>>$ to be changed and the new value $s\left(t_0\right)$ to be assigned, respectively. In other words, the above update instruction specifies the update set $\left\{<<f,<s\left(t_1\right),\dots ,s\left(t_n\right)>>,s\left(t_0\right)>\right\}$, consisting of a single update. Note that only locations related to (non-static) basic names may occur at the left-hand side of an update instruction.

The construction of complex transition rules out of elementary update instructions is recursively defined by means of ASM rule constructors. For the ASM model applied to define the SDL-2010 semantics, six different constructors (if-then, do-in-parallel, do-forall, choose, extend, let) are used. These constructors are listed below, with an informal description of their meaning. Here, Rule, Rule_i denote transition rules, $g$ denotes a Boolean term, and $v,v_1,\dots ,v_n$ denote free variables over the base set of $M$. The scope of a rule constructor is expressed by appropriate keywords, and can additionally be indicated by indentation. The closing keywords can be omitted, if no confusion arises. If closing keywords are omitted, the corresponding constructor extends as much as possible, but not over the next where-clause.

• if-then-constructor

The update set specified by Rule in a given state $s$ is defined to be the update set of Rule₁ or Rule₂, depending on the value of $g$ in state $s$. Without the optional else-part, the update set defined by Rule is the update set of Rule₁ or the empty update set. Sometimes, elseif is used as abbreviation for else if.

• do-in-parallel-constructor

The update set defined by Rule in state $s$ is defined to be the union of the update sets of Rule₁ through Rule_n. In other words, the order in which transition rules belonging to the same block are stated is irrelevant. For brevity, the keywords do in-parallel and enddo may be omitted, where no confusion arises. Hence, an ASM program often appears as a collection of rules rather than a monolithic block rule.

• do-forall-constructor

The effect of Rule is that Rule₀ is fired simultaneously for all elements v of the base set of $M$ for which the Boolean condition $g\left(v\right)$ holds in state $s$, where v is a free variable in Rule₀. More precisely, ${\Delta }_s\left(\text{Rule}\right)$ is the union of all update sets ${\Delta }_s$ (Rule₀(v)) such that $g\left(v\right)$ holds in state $s$. Recall that update sets are required to be finite; therefore, $g\left(v\right)$ must hold for a finite number of values only.

• choose-constructor

The effect of Rule is that Rule₀ is fired for an element v of the base set of $M$ for which the condition $g\left(v\right)$ holds in state $s$, where v is a free variable in Rule₀. More precisely, ${\Delta }_s\left(\text{Rule}\right)$ is some update set ${\Delta }_s$ (Rule₀(v)) such that $g\left(v\right)$ holds in state $s$, or the empty update set if no such v exists.

• extend-constructor

The effect of Rule when fired at state $s$ is that $n$ reserve elements of $s$ (see clause F1.3.1.2) are imported into the dynamic domain $D$ (while being removed from the reserve), that $v_1,\dots ,v_n$ become bound to one of the imported elements each, and then Rule₀ $\left(v_1,\dots ,v_n\right)$ is fired.

The extend constructor can be used to mimic object-based ASM definitions, where objects are dynamically created. Thus, for each object to be created, an element from the reserve is assigned to the corresponding domain, and initialized.

• let-constructor

The effect of Rule when fired in some state $s$ is that v is bound to the value of expression, and that Rule₀ is fired with this value.

The precise meaning of the rule is given by its update set with respect to a state $s$, which is either {$<<ow\ne r,<s\left(t\right)>>,s\left(ag\right)>$} for some token $s\left(t\right)$ available in $s$, if all further predicates stated in the if-then-constructor hold in $s$, or the empty update set otherwise.

F1.3.1.9.  Abbreviations

Rules can be structured using abbreviations, consisting of rule macros and derived names, which may have parameters. This allows for hierarchical definitions, and the stepwise refinement of complex rules, which supports the understanding of ASM model definitions.

Derived names are introduced (as explained in clause F1.3.1.5 and clause F1.3.5.3), i.e., by declaration and definition, or alternatively, in the compact form, by combining declaration and definition.

• rule-macro-definition

Let Rule₀ denote a transition rule with free variables $v_1,\dots ,v_n$ of domains $D_1,\dots ,D_N,n\ge 0$. The general form of a rule macro definition is:

Rule macro names are, by convention, written in small capitals, with a leading capital letter (as in SharedAccess).

• where-part

By default, rule macros and derived names have a global scope. However, their scope can also be restricted to a particular transition rule Rule by using the where-part.

• rule-macro-constructor

Rule macros are applied in transition rules as follows:

Formally, rule macros are syntactical abbreviations, i.e., each occurrence of a macro in a rule is to be replaced textually by the related macro definition (replacing formal parameters by actual parameters).

F1.3.1.10.  ASM programs

An ASM program $P$ is given by a framed transition rule (or rule for short) of the following form:

As already mentioned, rule macro definitions may either have a local or a global scope. To have a global scope, the macro definitions can be given outside the ASM program and can thus also be applied in the ASM program.

In the basic ASM model there is just one ASM program, which is statically associated with an implicitly defined agent executing this program. The next clause allows several ASM programs to be defined and associated with different agents that are introduced dynamically during abstract machine runs.

The ASM program is defined by a single transition rule as shown in the frame. The transition rule uses the do-in-parallel-constructor and 3 rule macros, which results in a hierarchical rule definition.

F1.3.2.1.  Signature

The signature (vocabulary) $V$ of a multi-agent ASM $M$ includes distinguished domain names:

representing a dynamic set $A$ of agents and an invariant set $P$ of ASM programs, respectively. Agent, Program and program: Agent $\to$ Program constitutes further background classes.

Furthermore, $V$ includes a distinguished function name:

and a special 0-ary function Self (see clause F1.3.2.2), whose interpretation is different for each agent.

F1.3.2.2.  Agents and runs

A multi-agent, distributed ASM has a finite number of agents. Agents can be created and destroyed dynamically. Each agent executes its own basic ASM. The behaviour of each agent is determined by a program, which is defined by a transition rule. The association between agents and their behaviour is specified by the background function program: Agent $\to$ Program. This function can be updated, allowing agents' behaviour to be modified dynamically, and allowing behaviour to be assigned to newly created agents.

Agents operate concurrently and interact by sending messages to one another (see [b-Blass] and [ITU-T Z.101]). More precisely, agents interact by updating locations that are accessible to other agents. Agents can act as Communicators [b-Glässer], whose behaviour is to read input locations, transform the values read, and update output locations that can be read by other agents. In this way messages can be passed asynchronously between agents without the original source or the final destination necessarily having a commonly accessible location. Agents also interact with an external environment, which can be viewed as an agent in its own right, or as a collection of agents.

A multi-agent distributed ASM is formed by combining its constituent single-agent ASMs. Like a single agent ASM, it has a set states $S$, a subset of initial states $S_0\subseteq S$ and a function $\tau :S\to S$, called the one-step transformation.

To assign a behaviour to an agent of $M$, the distinguished function program (see clause F1.3.2.1) yields (for each agent a of M) the program of $P$ to be executed by a. The function program thus allows the definition (or redefinition) of the behaviour of agents dynamically; it is thereby possible to create new agents at run time. In a given state s of $M$, the agents of $M$ are all those elements a of s such that a.program identifies a behaviour (asdefined by some program of P) to be associated with a.

A special 0-ary function Self serves as a self-reference identifying the respective agent calling Self:

For every agent, Self has a different interpretation. By using Self as an additional function argument, each agent a can have its own partial view of a given global state of $M$ on which it fires the rule in a.program.

F1.3.2.3.  Distributed ASM programs

A distributed ASM M has a finite set $P$ of programs. Eachprogram $p\in P$ is given by a program name and a transition rule (or rule for short). The program name uniquely identifies $p$ within $P$, and is represented by a unary static function. Programs are stated in the following form:

Asm-Program:

Program names are, by convention, hyphenated and written in small capitals, with a leading uppercase letter (as in Resource-Management-Program).

By default, the following implicit constraint applies:

where program₁ ,…​, program_N are the names of the programs that are defined in the ASM model.

The program of the distributed ASM has the name Resource-Management-Program, and is defined as the single-agent ASM program before, with one difference: all occurrences of ag have been replaced by calls of the function Self. This allows the association of the program with different agents, while accessing the local state of these agents.

F1.3.5.1.  Informal description

In order to illustrate the ASM model, a simple resource management system RMS consisting of a group of $n>1$ agents competing for a resource, for instance, a device or service, is defined. Informally, this system is characterized as follows:

• There is a set of $m$ tokens, $m<n$, used to grant exclusive or non-exclusive (shared) access to the resource.

• Depending on whether the desired access mode is exclusive or shared, an agent must own all tokens or one token, respectively, before he may access the resource.

• An agent is idle when not competing for a resource, waiting when trying to obtain access to the resource, or busy when owning the right to access the resource.

• Once an agent is waiting, it remains so until it obtains access to the resource.

• A busy agent releases the resource when it is no longer needed, as indicated by a stop condition for that agent that is externally set. On releasing the resource, all tokens owned by the agent are returned.

• Stop conditions are only indicated when an agent is busy.

• Initially, all agents are idle, and all tokens are available.

F1.3.5.2.  Vocabulary

F1.3.5.3.  Derived names

F1.3.5.4.  Integrity constraints

F1.3.5.5.  Initial constraints

F1.3.5.6.  ASM programs

Resource-Management-Program

F1.3.6.1.  ASM-specific domains

static domain $X$	ASM base set (meta domain)
static domain Boolean	Boolean values
static domain Nat	Natural values greater than or equal to zero
static domain Real	Real values
shared domain Agent	ASM agents
static domain Program	ASM programs
static domain Token	Syntax tokens (character strings)
_ *	Domain constructor: finite sequences of
_ +	Domain constructor: non-empty, finite sequences of
_ -set	Domain constructor: finite sets of
_ × _ prec(7)	Tuple domain constructor
_ $\cup$ _ prec(6)	Union domain constructor

F1.3.6.2.  ASM-specific functions

static undefined: $\to X$	Indicator for undefined values
monitored Self: $\to$ Agent	Self reference for ASM agents
controlled program: Agent $\to$ Program	Program of an ASM agent
monitored currentTime: $\to$ Real	The current system time

F1.3.6.3.  Boolean functions and predicates

static true: $\to$ Boolean	Predefined literal
static false: $\to$ Boolean	Predefined literal
_ = _ prec(4)	Equality
_ $\ne$ _ prec(4)	Inequality
_ $\wedge$ _ prec(3)	Logical and
_ $\vee$ _ prec(2)	Logical or
_ $\to$ _ prec(1)	Implication
_ $\iff$ _ prec(1)	Logical equivalence
$\neg$ _	Negation
$\exists x\in D:P\left(x\right)$ prec(0)	Existential quantification (at least one element)
$\exists !x\in D:P\left(x\right)$ prec(0)	Unique existential quantification (exactly one element)
$\forall x\in D:P\left(x\right)$ prec(0)	Universal quantification

F1.3.6.4.  Terms

X	0-ary function application
f(t1,…​, tn)	Function application with n argument expressions
if Formula then Term else Term endif	Conditional expression; again we use elseif instead of else if
s- _ (_)	Tuple selection function (see Tuples below)
mk- _ (…​)	Tuple construction (see Tuples below)
inv- _ (…​)	The inverse of a function or map, inv- Fun(x) =def take({ a $\in$ D:Fun(a) = x })

F1.3.6.5.  Functions and relations on syntax tokens (character strings)

_ $+$ _ prec(6)	String concatenation
" _ "	Domain constructor – QUOTATION MARKS around character string
chr: Nat $\to$ Token	Single character Token for character with value given by Nat
head: Token $\to$ Token	First character of string representing the Token
last: Token $\to$ Token	Last character of string representing the Token
length: Token $\to$ Nat	Length of the string representing the Token
num: Token $\to$ Nat	Nat value of first character of string representing the Token
substring: Token × Nat × Nat $\to$ Token	substring of string representing the Token from element i length j.
tail: Token $\to$ Token	Tail of string representing the Token.

F1.3.6.6.  Functions and relations on integers

_ > _, _ ≥ _, _ < _ , _ ≤ _ prec(4)	Comparison operators
_ + _ prec(6)	Addition
_ - _ prec(6)	Subtraction
_ * _ prec(7)	Multiplication
_ / _ prec(7)	Division
_ ^ _ prec(8)	Raise x to the power y
0, 1, …​	Integer literals

F1.3.6.7.  Functions on sequences

static empty: $\to D^{*}$	Empty sequence
static head: $D^{*}\to D$	Head of the sequence (undefined when empty)
static tail: $D^{*}\to D^{*}$	Tail of the sequence (undefined when empty)
static last: $D^{*}\to D$	Last element of a sequence (undefined when empty)
static length: $D^{*}\to$ Nat	Length of a sequence
static < >: $D_1\times D_2\times \dots \times D_n\to {\left(D_1\cup D_2\cup \dots \cup D_n\right)}^{*}$	Sequence constructor; arguments are listed inside the brackets, separated by commas
1 …​ n	Sequence constructor for the sequence $<1,2,..n>$; can be used so long as it is clear that this constructs a sequence and not a set.
_ ⁀ _ prec(6)	Concatenation of sequences
toSet: $D^{*}\to D$ -set	Conversion of the elements of a sequence into a set
_ [_]	Access an element of a list; the index within the brackets must be of type Nat
_ in _ prec(4)	Element of?
<expression> | <var> in <seq>: <cond> >	Sequence comprehension; acts like a filter on <seq>, i.e., order-preserving; <seq> is an input sequence whose values are bound to <var>; <var> is a free variable in <expression>; evaluating <expression> with <var> bound to a value of <seq> yields a value; <cond> is a condition which determines whether or not that value will be included in the final sequence.
< <var> in <seq>: <cond> > =def < <var> | <var> in <seq>: <cond> >	Abbreviated sequence comprehension; <cond> acts as a filter on <seq>
< <expression> | <var> in <seq> > =def < <expression> | <var> in <seq>: true >	Abbreviated sequence comprehension
NOTE – The character ⁀ is the Unicode character with the decimal value 8256 (use find u^8256 in MSWord to locate).

F1.3.6.8.  Functions on sets

_ $\cup$ _ prec(6)	Set union
_ $\cap$ _ prec(7)	Intersection
_ \ _ prec(6)	Set subtraction
_ $\in$ _ prec(4)	Element of?
_ $\notin$ _ prec(4)	Not element of?
_ $\subseteq$ _ prec(4)	Subset of?
_ $\subset$ _ prec(4)	Proper subset of?
| _ |	Cardinality of a set
$\bigcup$ _	Big union: union of all sets included within the argument set
$\varnothing$	Empty set
static { }: $D_1\times D_2\times \dots \times D_n\to \left(D_1\cup D_2\cup \dots \cup D_n\right)$ -set	Set constructor; comma-separated list of arguments in the brackets
1..n	Set constructor for the set $\left\{1,2,..n\right\}$; can be used where there is no ambiguity with sequence constructor.
take: $D\text{-set}\to D$	Select an arbitrary element from the set, or undefined for an empty set
_ $..$ _ prec(5)	Natural range from the first value to the second. Empty set when the second expression is smaller than the first one
{ <expression> | <var> $\in$ <set>: <cond>}	Set comprehension, acts like a filter on <set>; <set> is an input set; <expression> is evaluated for each binding of <var> to a value of <set>, yielding a candidate for inclusion in the new set; <cond> determines whether or not the candidate is included in the final set.
{<var> $\in$ <set>: <cond> } =def {<var> | var $\in$ <set>: <cond> }	Abbreviated set comprehension
{ <expression> | <var> $\in$ <set> } =def { <expression> | <var> $\in$ <set>: true }	Abbreviated set comprehension

F1.3.6.9.  Patterns and case-expressions

Patterns provide a means to easily access the structure of values. The following patterns are provided:

• Variables: A variable matches any value. However, if the variable is already bound, it only matches itself.

• Anonymous variables: Anonymous variables are denoted by "*". They are shorthand for introducing an unused variable.

• Constructor: A constructor is given by its name and the arguments that are again patterns. It matches any value that is constructed using that constructor and with the arguments matching their corresponding pattern.

Named pattern: The notation Variable = Pattern introduces a name for (the value matching) the pattern.

Patterns are used to describe functions on the syntax tree. The non-terminal names of the grammar are used as the constructor functions.

A case expression is used to determine a value depending on pattern matching.

If the value of Term matches at least one Pattern_i, then the result of the case expression is given by the Term_i. If no pattern matches, the result is Term₀ (if present). Otherwise, the result is undefined.

F1.3.6.10.  Union domains

Union domains contain the values of their constituent domains. They are used below as models for named and unnamed unions and alternative right sides to abstract syntax rules.

F1.3.6.11.  Sequence domains

Sequence domains contain sequences of the values of their constituent domains. They are used below as models for named and unnamed sequences, and sequences defined as (parts of) the right sides of abstract syntax rules expressed using extended BNF.

F1.3.6.12.  Tuples

Tuple domains contain elements of the Cartesian product of their constituent domains. They are used below as models for the tuples specified by the right sides of abstract syntax rules. For every declared tuple domain, several implied constructor and selector functions are defined. For example, the tuple definition:

also defines the following constructor and selector functions:

When the tuple includes the same domain more than once, selector functions similar to s2- $D_1$ are defined. For union, the special selector function s-implicit is defined.

If a domain on the right hand side is optional (written as [D]), the selector function s-$D$ is still valid and gives the result undefined if $D$ is absent and the value of selecting $D$ otherwise. Similarly s-D-seq is valid for [$D^{*}$], and s-D-set is valid for [D-set].

An invalid selector returns undefined.

F1.3.6.13.  Abstract syntax rules

Abstract syntax rules from the language definition are directly translated to the ASM notation, using the metalanguage for the concrete grammar as defined in [ITU-T Z.111] with the modified representation of semantic subcategories used in Annex F2. This allows rules to be expressed using the usual BNF conventions extended to include square brackets to indicate optional items, suffixes to indicate various kinds of list, and curly brackets to group related items.

An abstract syntax rule defined with "::" declares a domain of syntax nodes. Each syntax node has an identity and a value. The value is a member of an auxiliary domain of tuples of syntax nodes. For example, the rule

declares

The abbreviation mk-Symbol creates new elements of the domain Symbol,

Note that mk-Symbol is not an ASM function, but an abbreviation for an ASM rule.

Selector functions, s-, select the components of the tuple that is the value of a syntax node.

Here is a more elaborate example, illustrating the definitions introduced by a variety of extended BNF constructs.

which is translated to:

As with the previous example, an abbreviation mk-Symbol is also introduced. This abbreviation creates a new object of domain Symbol using the extend primitive and sets the contents-Symbol value of the newly produced object to the corresponding element of Symbol-aux.

The abbreviation mk-Symbol is not a function, but in fact an ASM rule item. Therefore, it must be used only within ASM rules and not as an ASM location.

If for a given Symbol, sym, the optional $Symbo{l}_4$ is not present, that fact is expressed in the ASM model by leaving the corresponding value undefined: sym.s-Symbol₄ = undefined. An empty sequence of symbols (constructor with no parts) is denoted by (). For example, the abstract syntax rule

declares a singleton domain, Symbol, whose only element is the empty tuple.

The equality for syntax nodes is always a structural equality, i.e., the contents of the symbols are compared instead of the symbols themselves.

A rule of the form

where each alternative right side consists of a single symbol, is equivalent to

In this case, there are selectors .s- Symbol_i , $\left(i=1,\dots ,n\right)$ and if $x\in$ Symbol, then all but one of those selectors will have the value undefined. Moreover, x. s-implicit = x.contents-Symbol.

More usually, rules like this will be represented as named unions. The syntax rules introducing named unions have the form:

which is modelled as:

Note that since Symbol is a union domain, the expansion yields a domain definition, but no abbreviation mk-Symbol and no selector functions s- Symbol_i ($i=1,\dots ,n$) that can be applied to elements of Symbol.

Of course, it is still possible to construct elements of Symbol using any constructor that generates an element any of the domains Symbol₁, Symbol₂, …​, Symbol_n, and given $x\in$ Symbol, an expression of the form x $\in$ Symbol_i ($i=1,\dots ,n$) will to test whether or not x belongs to one of the constituent domains of Symbol.

If a name is not required, unnamed unions may be introduced by rules like:

instead of introducing a name for the union:

Named sequences can be introduced using rules like this:

which defines the domain of sequences of elements of Symbol₁. Similarly, a rule like

defines the domain of sequences of tuples (a,b) where a $\in$ Symbol₁ and b $\in$ Symbol₂

As with named unions, Symbol yields a domain definition, but not functions mk- nor s-. Elements of Symbol are constructed using the sequence constructor, $<>$, and components of Symbol can be accessed using the functions on sequences.

It is not always necessary to name a sequence explicitly. Unnamed sequences may be introduced by rules like:

or like:

Named and unnamed sets can be introduced in a similar way.

For each SDL-2010 keyword KEYWORD, there is an associated keyword domain Keyword with just one value:

It is required that all keyword domains are mutually disjoint.

Given the abstract grammar, there is a derived domain called DefinitionAS1, which is composed of all abstract syntax symbol domains as follows:

where Symbol₁, Symbol₂, …​, Symbol_n are all the symbols (terminal and non-terminal) of the abstract grammar. This includes unnamed non-terminals that appear in the syntax such as Graph-node^* and {Terminator | Decision-node} in the AS1 rule Transition, and {Open-range | Closed-range}^* in the AS1 rule Size-constraint, which in ASM are denoted (respectively) as Graph-node -seq, (Terminator $\cup$ Decision-node) and (Open-range $\cup$ Closed-range) -seq.

There is a similar domain DefinitionAS0 for the concrete grammar (AS0).

F1.3.6.14.  Abstract syntax tree

The syntax nodes declared by abstract syntax rules can be used to construct an abstract syntax tree.

To navigate downward in a given abstract syntax tree, the functions s- can be used. To navigate upward, two parent functions are defined.

Suppose node is an abstract syntax node and a member of the domain Symbol, one of the constituent domains of DefinitionAS1:

The parent of node, if it exists, includes node, in its contents-Symbol. That is,

Similarly, for node $\in$ Symbol $\subset$ DefinitionAS0:

Moreover, two functions are defined to find the parent of a particular kind.

The top node of the current abstract or concrete syntax tree is denoted by the following 0-ary functions:

The value of rootNodeAS1.parentAS1 is undefined.

The value of rootNodeAS0.parentAS0 is undefined.

The functions isAncestorAS1 and isAncestorAS0 determine if the first node is an ancestor of the second one:

The functions isSameNodeAS1 and isSameNodeAS0 determine if the first node is the same node as the second one, that is they are equal and in the same position in the syntax tree:

The abstract syntax tree AS0 can be modified using the following derived functions:

The first parameter of the function is the old sub-tree, the second one is the new sub-tree and the third parameter is the old tree. The function returns the new tree, where all old sub-trees are replaced by the new sub-tree.

The first parameter of the function is the old sub-tree, the second one is the new sub-tree and the third parameter is the old tree. The function returns the new tree, where the first old sub-tree is replaced by the new sub-tree, and each subsequent old sub-tree occurrence is unchanged.