Types

Type Definitions

Users can define types in type models stored in files with extension '.types' or in interface signature models.

A type model may import other type models by the following import statement:

import "myTypes.types"

The import mechanism works transitively: when a type model is imported, the models imported by it are also imported.

Predefined types: bool, int, real, string, bulkdata.

Values of type real can also support the exponential notation with e. A value of type real has the syntax:

3.2
2.0e-5

Values of type bulkdata are uninterpreted byte arrays.

A value of type bulkdata has the syntax:

Bulkdata<$optional_size$>

Examples:

Bulkdata<1000>
Bulkdata<>

Basic types Users can define their own basic types:

   type unit
   type uint
   type wstring
   type Pixel
   type Time
   type Command

User-defined basic types are uninterpreted, their set of values is unknown. It is possible to relate a basic type to one of the predefined types int, string, and real. In this way values of the predefined type can be used for the basic type:

type unit base on int

Enumeration types An example:

enum Mode {
    updating
    working
    sleeping
}

Refer to an element of an enumeration type by

Mode::working

Optionally, enumeration literals may be assigned with non-negative integers:

enum Mode {
    updating = 1 //if not explicitly given, the first literal assumes value 0
    working  //if not given, the value will increment the previous one, i.e. 2
    sleeping = 4 //user may give a value greater than the increment of the previous value
}

Vector Types

Vector types are defined by giving a base type and a number of dimensions. For each dimension, an optional size can also be given.

vector Image = Pixel [ 10 ] [ 20 ]
vector Requests = Command []

Literal values of vector types have the syntax: <VectorType>[element1, element2, …​]. For example:

<int[]>[] //example of empty vector of integers
<int[]>[1, 2]
<string[][]>[<string[]>["John", "Smith"], <string[]>["John", "Doe"]]

Record Types

record Status {
    Image image1
    Pixel [10 ] [ 20 ] image2
    Time time
}

In this example, the field image2 illustrates the possibility to use vector types inline, i.e. without giving an explicit name like in the case of type Image.

It is also possible for one record type to extend another:

record Person {
    string name
    string address
}

record Student extends Person{
    string university
}

Instances of record types have the syntax: TypeName{field1 = value1, field2 = value2, …​}. For example:

Person{name = "John", age = 25}

Map Types

Map types are defined by giving the key and value types of the map. The key type must be a basic type or enumeration.

aMapType = map<int, int>

Map types can also be used inline (without giving a name).

Instances of map types have the syntax: <type>{key1 → value1, key2 → value2, …​}. For example:

<aMapType>{} //example of an empty map
<map<int, int>>{1 -> 0, 2 -> 0}

Limitations for maps:

  • Maps are not supported in simulation and test generation tasks. They can be used in behavior specifications (interfaces and component functional constraints) and are supported in monitoring tasks.

  • Maps cannot be used as parameter and return types of events in signatures.

Types Usage

Types are used in variable declarations and in event parameter declarations. Types are given either by name or as inline vector or map declarations (similar to C-family of languages).

Examples:

variables
int i //variable of the predefined type int
Mode m //variable of enumeration type named Mode
Image img //variable of named vector type

int[] intVector //variable of inlined vector type

Default Values

Every type has a default value. It is usually used to automatically initialize variables that are not explicitly given a value. Below are the default values for each type.

Default values:

  • int: 0

  • real: 0.0

  • bool: true

  • string: ""

  • enums: the first enumeration literal

  • records: a record with the default values for the field types

  • vector: an empty vector

  • map: an empty map