Syntax and Semantics

Values

Three kinds of values are supported:

• Integers (5)

• Atoms (:atom) -- TODO: atom/symbol?

• Arrays ([elem0, elem1, ...])

Data types

Supported data types:

• Integer ranges min..max. min and max are integer-valued expressions. Ranges are inclusive.

• Enumerations {val1, val2, ...}. vals are identifiers and are interpreted as atoms.

• Arrays elem_type[length]. elem_type is any type (including arrays), length is an integer-valued expression.

Examples:

• 1..5 denotes the set {1, 2, 3, 4, 5}

• {up, down} denotes the set of atoms {:up, :down}

• (1..2)[3] denotes the set of arrays of length exactly 3 whose elements are integers in range [1, 2] inclusive.

Expressions

The following standard operators on integers are currently supported: +, -, % (modulo).

No operations (except comparing for equality) are possible on atoms.

The following operations are supported on arrays:

• Extracting an element (indexing): array[n] denotes nth element of array, starting from 0.

• Slicing: array[n..m] denotes portion of array from index n to m, inclusively (n - m + 1 elements).

• Concatenation: array1 + array2.

For example, to rotate a size-element array to the left:

array[1..size-1] + [array[0]]

Predicates

Predicates consist of comparison operators (=, !=, <, <=, >, >=) applied to expressions and standard Boolean operators (&&, ||).

Servers

TODO

State variables

Actions

Processes

TODO

Server instances

TODO