Promela |
Declarator |
mtype(2) |
NAME
mtype
-
for defining symbolic names of numeric constants.
SYNTAX
mtype
[ = ] {
name [ ,
name ]* } /* symbolic names */
mtype
name [ ,
name ]* } /* variables ranging over mtype names */
DESCRIPTION
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.
EXAMPLES
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 5The 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 };
NOTES
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.
SEE ALSO
datatypes(2).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |