The AsmM
concrete syntax (AsmetaL) is a textual notation
to be used by modelers to effectively write ASM
models within the ASMETA framework. It is defined in terms of an EBNF (extended
BackusNaur Form) grammar derived from a semantic interpretation of the AsmM
metamodel (the abstract syntax).
The AsmetaL
language can be divided roughly into four parts: the structural
language (provides the constructs required for describing the structure
of an ASM model.), the definitional language (provides the basic
definitional elements such as functions, domains, rules and invariants characterizing
an algebraic specification), the language of terms (provides all
kinds of syntactic expressions which can be evaluated in a state of an ASM),
and the behavioral language or
the language of rules (provides a notation to specify the transition
rule schemes of an ASM).
This quick guide gives a
description of each part by presenting the notation in an intuitive style
for better readability, instead of reporting the grammar productions. For
a more formal definition see the EBNF grammar.
Note that, to write an ASM
model of a system, the file containing the ASM spec must contain a single
ASM structure definition and take the ".asm"
extension (e.g. MyAsmModel.asm).
In this guide the following
conventions are adopted:
An ASM model is structured
into four sections: an header, an initialization, a
body and a main rule. The schema below shows the concrete notation for each
section.

[asyncr] asm name where: 
[ import m_{1} [( id_{11},...,id_{1h1} )] where: 

Body 
definitions : turbo rule TR_{1} [( x_{11} in b_{11},...,x_{1k1} in b_{1k1} )][ in b_{1}] = rule_{1} where: 
[ main rule R = rule ] where: 
[ init I_{1} :
[ domain D_{11} = Dterm_{11}
...
domain D_{1n1} = Dterm_{1n1}
]
[ function F_{11} [( p_{11} in d_{11},...,p_{1s1} in d_{1s1} )]= Fterm_{11}
...
function F_{1m1} [( p_{m11} in d_{m11},...,p_{m1sm1} in d_{m1sm1} )]= Fterm_{1m1}
]
[ agent A_{11} : r_{11}
...
agent
A_{1u1} : r_{1u1}
]
...
]
default init I_{d} :
[ domain D_{d1} = Dterm_{11}
...
domain D_{dnd} = Dterm_{dnd}
]
[ function F_{d1} [( p_{11}
in
d_{11},...,p_{1s1} in d_{1s1} )]= Fterm_{d1}
...
function F_{dmd} [(
p_{md1} in d_{md1},...,p_{mdsmd} in d_{mdsmd} )]= Fterm_{dmd}
]
[ agent A_{d1} : r_{d1}
...
agent
A_{dud}_{ } : r_{dud}
]
[ ...
init I_{t} :
[ domain D_{t1} = Dterm_{t1}
...
domain D_{tnt} = Dterm_{tnt}
]
[ function F_{t1} [( p_{11}
in
d_{11},...,p_{1s1} in d_{1s1} )]= Fterm_{t1}
...
function F_{tmt}[( p_{mt1}
in d_{mt1},...,p_{mtsmt} in d_{mtsmt} )] = Fterm_{tmt}
]
[ agent
A_{t1} : r_{t1}
...
agent
A_{tut}: r_{tut}
]
]
where:
 I_{1},...,I_{d},...,I_{t} are names for the initial states
of the ASM; the default initial state I_{d} is compulsory;
 D_{ij} are names of dynamic concrete domains
 already declared in the signature (see Header)  initialized in the
initial state I_{i};
 F_{ij} are names of dynamic functions 
already declared in the signature (see Header)  initialized in the initial state I_{i};
 p_{ij} are variable terms which specify
the formal parameters of the corresponding function and d_{ij} are the domains where p_{ij} take their value;
 Fterm_{ij} e Dterm_{ij} are terms (see section Terms) specifying the intial
value for the function F_{ij} and domain D_{ij};
 A_{ij} and r_{ij} are agent domains (concrete subdomains of the Agent
typedomain) and rules* assigned as programs to the agents,
respectively.
*Note that, r_{ij} is a macrocall
rule (see section Transition rules), i.e. the invocation of a named rule declared
in the ASM or imported from an other module.
If no agent initialization clause is specified, as default the ASM is
assumed singleagent and the program and the identifier of
the unique agent are respectively the ASM's main rule (see Main rule) and the ASM's
name.
A
lightweight notion of module is also supported. An ASM module is an
ASM without a main rule and without a characterization of the set of initial
states. We write a module in the same way as ASMs
with the keyword asm replaced by the
keyword module.

module name where name is the name of the ASM module. It
must be equal to the name of the ASM file (as name.asm).

[ import m_{1} [( id_{11},...,id_{1h1} )] where: 

Body 
definitions : where: 
We
use the following rules to distinguish among names of domains, functions,
enumeration elements, rules, variables:
ID_VARIABLE a
string begining with the dollar sign "$";
e.g. $x $abc $pippo
ID_ENUM
a string of length greater than or equal
to two and consisting of uppercase letters only; e.g. ON OFF
RED
ID_DOMAIN
a string begining with an uppercase letter;
e.g. Integer
X SetOfBags
Person
ID_RULE
a string begining the lowercase letter "r"
followed by the underscore symbol "_"; e.g. r_SetMyPerson r_update
ID_FUNCTION a
string begining with a lowercase letter, but not
starting with "r_"; e.g. plus
minus re
The ASM domains (or
universes) are classified in: typedomains
and concretedomains.
The typedomains
represent all possible super domains (for practical reasons, the superuniverse S of an ASM state S is divided into smaller
universes) and are further classified in: basic typedomains, domains
for primitive data values like booleans, reals, integers, naturals, strings, etc.; structured
typedomains, domains for building
data structures (like sets, sequences, bags, maps, tuples
etc.) over other domains; abstract typedomains,
dynamic usernamed domains whose elements have no precise structure and are
imported as fresh elements from a possibly infinite reserve by means of extend
rules (see section Transition rules); and enum
domains, finite usernamed enumerations to introduce new concepts of
type (e.g. one may define the enumeration Color
= {RED, GREEN, BLUE} to introduce the new concept of "color").
Concrete domains are usernamed subdomains of
typedomains. As for functions, a concrete domain can be static or dynamic.
The schema below shows the
notation for declaring a domain. Domains declared as "anydomain"
are generic domains representing any other typedomain. The standard library
defines one "predefined" anydomain, named Any, which represents the most generic one. As basic
typedomains only Complex, Real, Integer, Natural, String, Char, Boolean, Rule,
and the singleton Undef={undef} are allowed and defined in the standard library as
predefined basic typedomains. Moreover, two other special abstract domains are
considered predefined: the Agent domain for agents, and the Reserve domain
which works as "reserve" to increase the working space of an ASM. Note
that, the Reserve domain is considered "abstract", and therefore
"dynamic", since it is updated automatically upon execution of an
extend rule (see section Transition rules) – it can not be updated directly by
other transition rules –.
Model
element 
Concrete syntax 
anydomain D where D is the name
of the domain representing any other typedomain. A predefined generic domain
named Any is declared in the standard library and considered the most generic
one. 

basic domain D Only Complex, Real, Integer,
Natural, String, Char, Boolean, Rule, and Undef are allowed (users can not define other
basic domains). They are declared in the standard library as
"predefined" basic typedomains. 

abstract domain D where D is the name
of the typedomain. 

enum domain D = { EL_{1}...EL_{n} } where: 

Prod ( d_{1},d_{2},...,d_{n} ) where d_{1},...,d_{n} are the domains over which the cartesian
product is defined. 

Seq ( d ) where d is the domain over which the sequence domain is defined. 

Powerset ( d ) where d is the domain over which the power set is defined. 

Bag ( d ) where d is the domain over which the bag domain is defined. 

Map ( d_{1},d_{2} ) where d_{1},d_{2 }are the domains over which the map domain is defined. 

[ dynamic ] domain D subsetof td where: 
To declare an ASM function
it is necessary to specify the name, the domain, and the codomain
of the function. Moreover, the function name must be preceded by one of the
keywords static, dynamic or derived,
depending on its kind. Dynamic functions are further classified in monitored,
controlled, shared, out and local.
Local dynamic functions are not considered part of the signature; they are
declared and used only in the scope of a turbo transition rule with "local
state" (see section Transition rules).
The schema below shows the
concrete syntax for declaring a function F (the name) from D (the domain)
to C (the codomain).
Model
element 
Concrete syntax 
static F : [ D > ] C 

[ dynamic ] ( monitored  controlled
 shared  out
 local ) F : [ D > ] C A dynamic function is declared specifying its
kind (monitored, controlled, shared, or out);
optionally, the keyword dynamic can be also added as prefix. Local
dynamic functions can be declared only in the scope of a turbo transition
rule with local state (see section Transition rules). 

derived F : [ D > ] C 
There are two types of terms, basic terms
as in firstorder logic (variables, constants and function
applications) and extended terms to represent special terms like tuple terms, collection terms
(sets, maps, sequences, bags), the conditional term, variablebinding
terms, etc.
Model
element 
Concrete syntax 
Complex number, as in x+iy, where x and y are real numbers and i is the imaginary
unit. A complex number must be written without spaces within, because it is
considered a unique token. E.g.: 2i3 Real terms as floating point numbers. E.g: +3.4 , 3.4
, 3.4, 0.0
,etc... Integer terms as signed numbers. E.g.: 3, +3, 3, 0, etc... Natural numbers as unsigned numbers plus the
suffix "n". E.g.: 3n, 0n, etc... Char terms as char literals delimited by single
quotes. E.g.: 'a', '5',
etc... String terms as a string of literals delimited
of double quotes: E.g.: "hello", "1256", etc... Boolean terms: true,
false Enum term: e where e is an element of an enumeration
typedomain. 

v where v is a variable. The variable can
be a location variable (which is replaced by a location term ), or a rule
variable (which is replaced by a rule term ), or a logical
variable (which is replaced by a term that is neither a location term
nor a rule term). 

[id . ]f [ ( t_{1},...,t_{n} ) ] where: 

A specialized function term where f is a dynamic
function fixed by the ASM signature. 
Model
element 
Concrete syntax 
( t_{1},...,t_{n} ) where t_{1},...,t_{n} are terms, that can have a distinct nature. The empty tuple is not allowed. 

[ t_{1},...,t_{n} ] where t_{1},...,t_{n} are terms of the same nature. [ ] denotes
the empty sequence. A
finite sequence over numbers (real, integer and natural)
can be also defined by means of an interval notation, as in [ t_{low} .. t_{upp} [ ,s ] ] where: 

[
v_{1} in S_{1},...,v_{n} in S_{n}
[
G_{v1,...,vn} ] : t_{v1,...,vn}
] where: 

{ t_{1},...,t_{n} } where t_{1},...,t_{n} are terms of the same nature. { } denotes the empty set. A
finite set over numbers (real, integer and natural)
can be also defined by means of an interval notation, as in [ t_{low} .. t_{upp} [ ,s ] ] where: 

{
v_{1} in D_{1},...,v_{n} in D_{n} [
G_{v1,...,vn} ] : t_{v1,...,vn}
} where: 

< t_{1},...,t_{n} > where t_{1},...,t_{n} are terms of the same nature. < > denotes the empty bag. A
finite bag over numbers (real, integer and natural)
can be also defined by means of an interval notation, as in [ t_{low} .. t_{upp} [ ,s ] ] where: 

< in B_{1},...,v_{n} in B_{n} [
G_{v1,...,vn} ] : t_{v1,...,vn}
> where: 

{
t_{1} > s_{1},...,t_{n} > s_{n} } where: { >} denotes the empty map. 

{v_{1} in D_{1},...,v_{n} in D_{n} [
G_{v1,...,vn} ] : t_{v1,...,vn} > s_{v1,...,vn}
} where: 

if
G then t_{then} [
else t_{else} ] endif where: 

switch t case t_{1} : s_{1} ... case t_{n} : s_{n} [ otherwise s_{n+1} ] endswitch where: 

let ( v_{1}=t_{1},
..., v_{n}=t_{n} ) in t_{v1,...,vn} endlet where: 

( exist v_{1} in D_{1},...,v_{n} in D_{n}
[ with G_{v1,...,vn} ]) where: 

( exist unique v_{1} in D_{1},...,v_{n} in D_{n}
[ with G_{v1,...,vn} ]) where: 

( forall v_{1} in D_{1},...,v_{n} in D_{n}
[ with G_{v1,...,vn} ]) where: 

D where D is the name of a domain declared
in the ASM signature or directly the expression for a structured typedomain. 

<< R[ ( D_{1},...,D_{n} ) ] >> where R is the name of a defined transition rule, and D_{1},...,D_{n} (if any) are the domains of the formal rule parameters*. It is a special term used to denote a transition rule where a term is expected (e.g as actual parameter in a rule application to represent a transition rule). Its interpretation results, therefore, in a transition rule. *Similarly to functions, rules can
be overloaded. When rules are overloaded, it is necessary to indicate
the domains of the formal rule parameters. 
In addition to these terms, the AsmM
concrete syntax admits special expressions to support the infix notation for some wellknown functions on basic domains (like plus,
minus, mult, etc.) of the AsmM Standard Library. In these expressions, basic
terms and the domain term are used as operands. The table
below show the infix operators corresponding to these functions,
together with their associativies and priorities. The
operator priorities range from 0 to 9, where 9 indicates
the strongest one and 0 the weakest one.
Function 
Infix
operator 
Type 
Associativity 
Priority 
minus (unary) plus (unary) 
 + 
Complex → Complex 
left 
9 
pwr 
^ 
Real × Real → Real 
left 
8 
mult 
* 
Complex × Complex →
Complex 
left 
7 
div 
/ 
Complex × Complex →
Complex 
left 
7 
mod 
mod 
Integer × Integer → Integer 
left 
7 
plus 
+ 
Complex × Complex →
Complex 
left 
6 
minus 
 
Complex × Complex →
Complex 
left 
6 
lt 
< 
Real × Real → Boolean 
left 
5 
le 
<= 
Real × Real → Boolean 
left 
5 
gt 
> 
Real × Real → Boolean 
left 
5 
ge 
>= 
Real × Real → Boolean 
left 
5 
eq 
= 
D × D → Boolean 
left 
5 
neq 
!= 
D × D → Boolean 
left 
5 
in 
in 
powerset(D) × D → Boolean 
left 
4 
notin 
notin 
powerset(D) × D → Boolean 
left 
4 
not 
not 
Boolean → Boolean 
left 
3 
and 
and 
Boolean × Boolean →
Boolean 
left 
2 
xor 
xor 
Boolean × Boolean →
Boolean 
left 
1 
or 
or 
Boolean × Boolean →
Boolean 
left 
1 
implies 
implies 
Boolean × Boolean →
Boolean 
left 
0 
iff 
iff 
Boolean × Boolean →
Boolean 
left 
0 
In a given state, a
transition rule of an ASM produces for each variable assignment an update set
for some dynamic functions of the signature. We classify transition rules in
two groups: basic rules and turbo rules. The former are
simply rules, like the skip rule and the update rule, while
the latter are rules, like the sequence rule and the iterate rule,
introduced to support practical composition and structuring principles of the ASMs. Other rule schemes are derived from the basic and the
turbo rules.
Model
element 
Concrete syntax 
skip 

l := t where: 

par R_{1} R_{2} ... R_{n} endpar where R_{1},R_{2},...,R_{n} are transition rules. 

if
G then R_{then} [else R_{else}] endif where: 

switch t case t_{1} : R_{1} ... case
t_{n} : R_{n} [otherwise R_{n+1}] endswitch where: 

let ( v_{1}=t_{1},
..., v_{n}=t_{n} ) in R_{v1,...,vn} endlet where: 

forall v_{1} in D_{1}, ..., v_{n} in D_{n} with G_{v1,...,vn} do R_{v1,...,vn} where: 

choose v_{1} in D_{1}, ..., v_{n} in D_{n} with G_{v1,...,vn} do R_{v1,...,vn} [ ifnone
P ] where: 

r [t_{1},...,t_{n}] where: r [] is used for a macro with no
arguments. 

extend D with v_{1},...,v_{n} do R where: 

seq R_{1} R_{2} ... R_{n} endseq where R_{1},R_{2},...,R_{n} are transition rules. 

iterate R enditerate where R is a transition rule. 

while G do R where: 

r(t_{1},...,t_{n}) where: r() is used to call a rule with no
arguments. 

recwhile G
do R where G is a term representing a boolean condition and R is a transition rule. 

[dynamic] local f_{1} :[D_{1} >]C_{1} [ Init_{1} ] where: 

try P catch l_{1},...,l_{n} Q where: 

l < r(t_{1},...,t_{n}) where: 

v where v is either a rule variable or a
function term. This rule works as a form of wrapper to allow the use of
either a function term or a variable term where a rule is expected. 
Comments can be written as
follows:
// text to be commented
/* text to be
commented*/