State annotations

> > > >

A state annotation adds state information to a location in an automaton. For basic information on state annotations, see the language tutorial. Here we discuss further details.

State annotations (@state) can be added to the following elements in CIF specifications:

Locations of automata.

The annotation has the following constraints, in addition to the general constraints that apply to all annotations:

A single location may have multiple state annotations, if that location represents multiple states of a state space.
Each argument of a state annotation represents either an automaton with its current location, or a variable with its current value.
There can be any number of arguments (including no arguments), as models may have any number of automata and variables.
The arguments may be in any order.
The name of the argument must be the absolute name of the corresponding automaton or variable.
Argument values, and parts of argument values (in case of containers), must be literals of type bool, int, real, string, tuple, list, set, or dict. This implies that the values must be statically evaluable, and that evaluating an argument value must not result in an evaluation error.
If at least one location in an automaton has at least one state annotation, all other locations in that same automaton must also have at least one state annotation, as all these locations should then represent a least one state from the state space.
Different state annotations on the same or different locations of a single automaton must have the same number of arguments, the arguments must have the same names, and the values of arguments with matching names must have compatible types (ignoring ranges), as they should represent states from the same state space. The arguments don’t have to be in the same order.

Most values can thus be represented as literals, but there are some exceptions. The following overview indicates how to represent locations and different types of values:

Location / value Represented as

Location / value	Represented as
Location of an automaton	String literal with the non-escaped name of the location, or `"*"` for a nameless location.
Boolean value	`true` or `false` boolean literal.
Integer value	Integer literal, such as `0`, `1` or `1234`. Note that negative integer values are represented as a negation (unary operator) applied to a positive integer literal. And `-2147483648` is represented as `-(2147483647) - 1`.
Real value	Real literal, such as `0.0`, `1e5` or `0.5e-3`. Note that negative real values are represented as a negation (unary operator) applied to a positive real literal.
Enumeration value	String literal with the non-escaped name of the enumeration literal.
String value	String literal, such as `"some text"`.
Tuple value	Tuple literal, such as `(1, 2)` or `(true, (1, 2))`.
List value	List literal, such as `[1, 2]` or `[[1, 2], [3, 4]]`. Note that empty lists typically require a type hint in the form of a type cast, such as `<list[0] int>[]`.
Set value	Set literal, such as `{1, 2}` or `{{1, 2}, {3, 4}}`. Note that empty sets typically require a type hint in the form of a type cast, such as `<set int>{}`.
Dictionary value	Dictionary literal, such as `{1: 2, 3: 4}` or `{1: {2: 3}, 2: {4, 5}}`. Note that empty dictionaries typically require a type hint in the form of a type cast, such as `<dict(int:int)>{}`.
Function value	String literal with the non-escaped absolute name of the function, or `"*"` for functions that represent a default initial value of a variable with a function type.

Location of an automaton

String literal with the non-escaped name of the location, or "*" for a nameless location.

Boolean value

true or false boolean literal.

Integer value

Integer literal, such as 0, 1 or 1234. Note that negative integer values are represented as a negation (unary operator) applied to a positive integer literal. And -2147483648 is represented as -(2147483647) - 1.

Real value

Real literal, such as 0.0, 1e5 or 0.5e-3. Note that negative real values are represented as a negation (unary operator) applied to a positive real literal.

Enumeration value

String literal with the non-escaped name of the enumeration literal.

String value

String literal, such as "some text".

Tuple value

Tuple literal, such as (1, 2) or (true, (1, 2)).

List value

List literal, such as [1, 2] or [[1, 2], [3, 4]]. Note that empty lists typically require a type hint in the form of a type cast, such as <list[0] int>[].

Set value

Set literal, such as {1, 2} or {{1, 2}, {3, 4}}. Note that empty sets typically require a type hint in the form of a type cast, such as <set int>{}.

Dictionary value

Dictionary literal, such as {1: 2, 3: 4} or {1: {2: 3}, 2: {4, 5}}. Note that empty dictionaries typically require a type hint in the form of a type cast, such as <dict(int:int)>{}.

Function value

String literal with the non-escaped absolute name of the function, or "*" for functions that represent a default initial value of a variable with a function type.