Promela Reference -- mtype(2)





mtype - for defining symbolic names of numeric constants.

mtype [ = ] { name [ , name ]* } /* symbolic names */
mtype name [ , name ]* } /* variables ranging over mtype names */

An mtype declaration allows for the introduction of symbolic names for constant values. There can be only one mtype declaration per verification model. If an mtype declaration is present, the keyword mtype can also be used as a data type, to introduce variables that obtain their values from the range that was declared. This data type can also be used inside chan declarations, for specifying the type of message fields.

The definition

mtype = { ack, nak, err, next, accept }

is functionally equivalent to the sequence of macro definitions:
#define	ack	1

#define nak	2

#define	err	3

#define next	4

#define accept	5

The convention is to place an assignment operator in between the keyword mtype and the list of symbolic names that follows, but it is not strictly required.

The symbolic names are preserved in tracebacks and error reports for all data that is explicitly declared with data type mtype . For instance,

mtype a; mtype p[4] = nak;

chan q = [4] of { mtype, byte, short, mtype };

Variables of type mtype are stored in an unsigned char in C implementations. Therefore, there can be at most 255 distinct symbolic names in an mtype declaration.

In version 3.3 and later, more than one mtype declaration may appear in a single specification. In this case, the mtype declarations are automatically concatenated by the parser, in the order in which they appear in the specification. The upper limit of 255 distinct symbolic names declared in one or more mtype declarations still holds.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)