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)orreplyif 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)
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:
MapExpr[keyExpr → valueExpr]. Returns a new map that is the update of MapExpr with the given (key, value) pair. MapExpr is unaltered. -
map read:
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. -
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).
Example:
Assume give 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]
In a guard we might use not (moving[Segment::front] or moving[Segment::middle]).