Statements are used in the bodies of transitions and in initialization sections. The following statements are supported:
-
Assignment:
Variable := Expression
-
Record field assignment:
RecordExpression.field := Expression
. Example:person.name = "John"
-
If-Then-Else:
-
if BooleanExpression then Statements else Statements fi
-
if BooleanExpression then Statements fi
-
-
Reply to command:
reply(Expression)
orreply
if no return value is expected -
Sending notification:
NotificationName(Expression1, Expression2, …)
Expressions
Basic Types, Enumerations and Bulkdata
-
Numbers (integers and reals):
1, 23.0, -1, -10.2, 2.0e-2
-
Strings:
"This is a string"
-
Booleans:
true, false
-
Bulkdata values:
Bulkdata<1024>, Bulkdata<>
-
Enumeration literals:
EnumTypeName::Literal
, e.g.Status::On
Operations:
-
Boolean operators:
AND, OR, NOT
-
Comparators: `<, >, ⇐, >=, ==, != `
-
Arithmetics:
+, -, *, /, mod, min, max, ^
-
Predefined functions:
abs(Expr), asReal(Expr), length(BulkdataExpr), matches(Pattern, StringExpr)
, in matches, the Pattern is a string that uses the Java syntax for regular expressions
Records
-
Records:
RecordTypeName{fieldsName = Expression, …}
, e.g.Person{firstName = "John", lastName = "Smith"}
-
Record field access:
RecordExpression.fieldName
Using the any value (*) is possible for fields in records but only if the record is used as a value in event:
reply(Result{flag = true, someOtherField = *})
Vectors
Vectors: <TypeName>[element1, element2, …]
, e.g. <int[]>[], <string[][]>[<string[]>["John", "Smith"], <string[]>["John", "Doe"]]
Operations:
-
Quantifiers:
-
exists(Variable_decl in VectorExpr : BooleanExpr)
-
forAll(Variable_decl in VectorExpr : BooleanExpr)
-
-
Predefined functions:
isEmpty(VectorExpr), size(VectorExpr), contains(VectorExpr, Expr), add(VectorExpr, Expr), delete(Variable_decl in VectorExpr : BooleanExpr)
Changing the content of vectors
In order to mutate a vector by adding a new element in its end use the following:
persons := add(persons, "John")
In this example, the predefined function add returns a new vector without changing the argument persons. In order to update the value of persons use the expression in an assignment statement.
Function delete removes vector elements that satisfy a given condition. The result is a vector without those elements:
persons := delete(string p in persons : p == "John")
Maps
Maps: <Type>{key → value, key → value, …}
, e.g. <map<int, int[]>>{1 → <int[]>[], 2 → <int[]>[0]}
Operations:
-
map update with single key-value pair:
MapExpr[keyExpr → valueExpr]
. Returns a new map that is the update of MapExpr with the given (key, value) pair. MapExpr is unaltered. -
map update with a collection of key-value pairs:
MapExpr[Var_decl in collection : keyExpr → valueExpr]
. Returns a new map that is the update of MapExpr with the (key, value) pairs created while the Var_decl iterates over the elements of the given collection. MapExpr is unaltered. -
map read with single key:
MapExpr[keyExpr]
. Returns the value associated to the keyExpr. If the keyExpr does not exist as a key in the map, the default value for the map value type is returned. MapExpr remains unchanged. -
map read with a collection of keys:
MapExpr[Var_decl in collection : keyExpr]
. Returns a collection of the values associated to the keys calculated by keyExpr while Var_decl iterates over the elements of the collection. If the keyExpr does not exist as a key in the map, the default value for the map value type is returned. MapExpr remains unchanged. -
Predefined functions:
-
hasKey(MapExpr, KeyExpr)
-
deleteKey(MapExpr, KeyExpr)
: returns a new map derived from MapExpr by removing the KeyExpr key and its associated value. MapExpr is unchanged. -
deleteKey(MapExpr, CollectionOfKeys)
: returns a new map derived from MapExpr by removing the keys in CollectionOfKeys and their associated value. MapExpr is unchanged.
-
Examples:
Assume given types
enum Segment {front middle back}
MoveStatus = map<Segment,bool>
then a variable can be defined and initialized as follows:
variables
MoveStatus moving
init
moving := <MoveStatus>{Segment::front→false, Segment::middle→false, Segment::back→false}
Given a part
of type Segment
, the variable can be updated as follows:
moving := moving[part → true]
Given segments
of type <Segment[]>
, the variable can be updated as follows:
moving := moving[Segment s in segments : s → true]
Some values in moving
can be read as:
moving[Segment s in segments : s]
. The result is a vector of booleans.
In a guard we might use not (moving[Segment::front] or moving[Segment::middle])
.