Promela Reference -- mtype(2)

`mtype`

NAME
mtype - for defining symbolic names of numeric constants.

SYNTAX
mtype [:name] [ = ] { name [, name ]* }

mtype [:name] name [ = mtype_name ]

mtype [:name] 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.

Optionally, in Spin Version 6.4.8 or later, the keyword mtype can be followed by a colon and a name (as in mtype:fruit = { appel, pear }) to indicate a specific subtype. If so, then every use of the mtype keyword must be followed by the same suffix for all variables declared to be of that subtype.

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	1

Note 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.

An example of using subtypes is as follows, illustrating also some type of assignments of one subtype to another that can now be caught.

// requires Spin Version 6.4.8 or later

mtype { one, two, three }

mtype:fruit = { appel, pear, banana }

mtype:sizes = { small, medium, large }

chan q = [0] of { mtype, mtype:fruit, mtype:sizes, int }

proctype recipient(mtype:fruit z; mtype y)
{	mtype a
	mtype:fruit b
	mtype:sizes c

	atomic {
		printf("z: "); printm(z); printf("\n");
		printf("y: "); printm(y); printf("\n");
	}

	q?a,b,c,_
	atomic {
		printm(a)
		printm(b)
		printm(c)
		printf("\n")
	}
	q?c,a,b,_	// flagged as type error
	atomic {
		printm(a)
		printm(b)
		printm(c)
		printf("\n")
	}
}

init {
	mtype numbers, nn;
	mtype:fruit snack, ss;
	mtype:sizes package, pp;

	run recipient(pear, two)
//	run recipient(small, two)	// type error

//	package = pear			// type error
	numbers = one
	snack = pear
	package = large

	printm(numbers)
	printm(snack)
	printm(package)
	printf("\n")

	q!numbers,snack,large,9
//	q!large,ss,pp,3			// type error

	assert(false)
}

SEE ALSO
datatypes
printf
printm

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage (Page updated: 8 January 2017)

`Promela`

`Declarator`

`mtype`