Promela |
Declarator |
mtype |
NAME
mtype -
for defining symbolic names of numeric constants.
SYNTAX
mtype [ = ] { name [, name ]* }
mtype name [ = mtype_name ]
mtype name '[' const ']' [ = mtype_name ]
DESCRIPTION
An
mtype declaration allows for the introduction of
symbolic names for constant values.
There can be multiple
mtype declarations in a verification model.
If multiple declarations are given, they are
equivalent to a single
mtype declaration that contains the concatenation of
all separate lists of symbolic names.
If one or more mtype declarations are present, the keyword mtype can be used as a data type, to introduce variables that obtain their values from the range of symbolic names that was declared. This data type can also be used inside chan declarations, for specifying the type of message fields.
EXAMPLES
The declaration
mtype = { ack, nak, err, next, accept }is functionally equivalent to the sequence of macro definitions:
#define ack 5 #define nak 4 #define err 3 #define next 2 #define accept 1Note that the symbols are numbered in the reverse order of their definition in the mtype declarations, and that the lowest number assigned is one, not zero.
If multiple mtype declarations appear in the model, each new set of symbols is prepended to the previously defined set, which can make the final internal numbering of the symbols somewhat less predictable.
The convention is to place an assignment operator in between the keyword mtype and the list of symbolic names that follows, but this is not required.
The symbolic names are preserved in tracebacks and error reports for all data that is explicitly declared with data type mtype .
In this example:
mtype a; mtype p[4] = nak; chan q = [4] of { mtype, byte, short, mtype };the mtype variable a is not initialized. It will by default be initialized to zero, which is outside the range of possible mtype values (identifying the variable as uninitialized). All four elements of array p are initialized to the symbolic name nak . Channel q , finally, has a channel initializer that declares the type of the first and last field in each message to be of type mtype .
NOTES
Variables of type
mtype are stored in a variable of type
unsigned char in their C equivalent.
Therefore, there can be at most 255 distinct symbolic
names in an
mtype declaration.
The utility function printm can be used to print the symbolic name of a single mtype variable. Alternatively, in random or guided simulations with Spin, the name can be printed with the special printf conversion character sequence %e . The following two lines, for instance, both print the name nak (without spaces, linefeeds, or any other decoration):
mtype = { ack, nak, err, next, accept } init { mtype x = nak; printm(x); printf("%e", x) }The printm form is prefered, since it will also work when error traces are reproduced with the verifier, for models with embedded C code.
SEE ALSO
datatypes
printf
printm
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |