AltaRica : Domains

Basic domains

The AltaRica language allows several predefined sets:

  • The set of Booleans values is denoted with the keyword bool. It contains the two value true and false.
  • Integers and ranges. Integer variables and constants can be defined. The keyword integer denotes the set of integers. Even if this domain is allowed by the language, it is not necessarily supported by tools (e.g. the algorithms implemented into ARC assume that variables are defined on finite domains). Finite ranges of integers can be defined between brackets [ and ] e.g. [1, 5]. The bounds of a range can be any constant integer expression but its value be defined (i.e. it can not make reference to a named constant without a value).
  • Sets of symbolic values. The language allows to define sets with abstract names; these names have no particular semantics. These values can be considered like enumerated values in the C language. No order is defined for these values and one can only check the equality of two values. Two variables defined in different enumeration sets can checked for (in)equality.

Compound domains

The AltaRica language allows to define compound domains like structure and arrays; of course, any combination of structures and arrays is allowed.

Arrays have a fixed number of elements. The syntax for such domains uses brackets after the domain of elements. The following example defines two domains: CompFlags that is an array of N Booleans where N is some integer constant. BMatrix is an array of size 2*N of arrays containing N Booleans.

1 const N : integer = 2;
2
3 domain CompFlags = bool[N];
4
5 domain BMatrix = bool[N][2*N];

The description of structures starts with the keyword struct and terminates with tcurts. Between the two keywords a list of declarations of fields is given; lists are separated with semi-colons (;). Several fields, separated by commas (,), may be specified in the same declaration.
The order of declaration of fields is not relevant; the following code gives several examples of structure domains.

1 domain Coords = struct
2                   x : integer;
3                   y : integer;
4                 tcurts;
5
6 domain Segment = struct
7                   src, tgt : Coords
8                  tcurts;

Variables and constants defined as structures or arrays can be checked for equality or inequality but only if domains are comparable. The same constraint holds for assignments (in transitions or initializations).

  • Two array domains are comparable if they have the same number of elements and the domains of the elements are comparable.
  • Two structure domains are comparable if the fields names are the same (independently of the order of declaration) and fields with the same name have comparable domains.

Then, the equality relation is simply defined as follows:

  • Two array variables or constants are equals if each element in the array are equal.
  • Two variables or constants defined as structure are equals if they are equal for each field of the structure.