Statements and Expressions

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) or reply 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]).