# Contents

# Types

There are 4 predefined types: `int`, `bool`,
`clock`, and `chan`. Array and record types can be
defined over these and other types.

Type ::= Prefix TypeId Prefix ::= 'urgent' | 'broadcast' | 'meta' | 'const' TypeId ::= ID | 'int' | 'clock' | 'chan' | 'bool' | 'int' '[' Expression ',' Expression ']' | 'scalar' '[' Expression ']' | 'struct' '{' FieldDecl (FieldDecl)* '}' FieldDecl ::= Type ID ArrayDecl* (',' ID ArrayDecl*)* ';' ArrayDecl ::= '[' Expression ']' | '[' Type ']'

The default range of an integer is [-32768, 32767]. Any assignment out of range will cause the verification to abort.

Variables of type `bool` can have the values `false`
and `true`, which are equivalent to the the integer values 0
and 1. Like in C, any non-zero integer value evalutes to true and 0
evaluates to false.

Channels can be declared as urgent and/or broadcast channels. See the section on synchronisations for information on urgent and broadcast channels.

## Constants

Integers, booleans, and arrays and records over integers and
booleans can be marked constant by prefixing the type with the keyword
`const`.

## Meta variables

Integers, booleans, and arrays and records over integers and
booleans can be marked as meta variables by prefixing the type with
the keyword `meta`.

Meta variables are stored in the state vector, but are sematically not considered part of the state. I.e. two states that only differ in meta variables are considered to be equal.

## Arrays

The size of an array is specified either as an integer or as a
bounded integer type or scalar set type. In the first case the array
will be 0-indexed. In the latter case, the index will be of the given
type. The following declares a scalar set `s_t` of size 3 and
an integer array `a` of size 3 indexed by the scalar:

typedef scalar[3] s_t; int a[s_t];

## Record Variables

Record types are specified by using the `struct` keyword,
following the C notation. For example, the record `s` below
consist of the two fields `a` and `b`:

struct { int a; int b; } s;

## Scalars

Scalars in UPPAAL are integer like elements with a limitted number of operations: Assignment and identity testing. Only scalars from the same scalar set can be compared.

The limitted number of operations means that scalars are unordered
(or that all orders are equivalent in the sense that the model
cannot distinguish between any of the them). UPPAAL applies
*symmetry reduction* to any model using scalars. Symmetry
reduction can lead to dramatic reductions of the state space of the
model. resulting in faster verification and less memory being used.

Notice that symmetry reduction is **not** applied if diagnostic
trace generation is enabled or when `A<>`, `E[]`
or `-->` properties are verified.

Scalar sets are treated as types. New scalar sets are constructed
with the `scalar[n]` type constructor, where `n` is an
integer indicating the size of the scalar set. Scalars of different
scalar sets are incomparable. Use `typedef` to name a scalar
set such that is can be used several times, e.g.

typedef scalar[3] mySet; mySet s; int a[mySet];

Here `mySet` is a scalar set of size 3, `s` is a
variable whos value belongs to the scalar set `mySet` and
`a` is an array of integers indexed by the scalar set
`mySet`. Thus `a[s] = 2` is a valid expression.