Constants

RBL allows the definition of constants. A constant can be defined in terms of literals or expressions including other constants. They are defined using the const keyword:

const x : int = 5;
const b : bool = true;
const squares : array 4 of int = [1, 4, 9, 16];

A constant can have any type listed on the type system page. The type annotation is optional. If no type is given, the type of the constant is inferred from the expression.

Constants can be left undefined in the model:

const x : int;

In this case, the constant’s value must be provided on the command line, for example:

rbsc my_model.rbl -c x=2

Enumerations

Constants are sometimes used to give names to locations, for instance:

const INIT = 0;
const SEND = 1;
const RECEIVE = 2;

module sensor {
    loc : [0 .. 2] init INIT;
}

In order to define such constants with increasing values, an enum block can be used:

enum {
    INIT,
    SEND,
    RECEIVE
}

This enumeration is equivalent to the constant definitions above. If the enumeration is only used by a single module, it can also be inlined:

module sensor {
    loc : enum { INIT, SEND, RECEIVE} init INIT;
}

Note that the constants defined this way are still global.