Promela |
Declarator |
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
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:
NOTES
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):
An example of using subtypes is as follows, illustrating also some type
of assignments of one subtype to another that can now be caught.
SEE ALSO
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.
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 .
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.
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.
// 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)
}
datatypes
printf
printm
Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 8 January 2017)