Promela |
Declarator |
typedef(2) |
NAME
typedef
-
to declare a user-defined structured data type.
SYNTAX
typedef
name {
decl_lst }
DESCRIPTION
Typedef
declarations can be used to introduce user-defined data types.
User-defined types can be used anywhere predefined integer data types
can be used. Specifically, they can be used as formal and actual
parameters for
proctype
declarations and instantiations, they can be used as fields in
message channels, and as arguments in message send and receive
statements.
A typedef declaration can refer to other, previously declared, typedef structures, but may not be self-referential. A typedef definition must always be global, but it can be used to declare both local and global data objects of the new type.
EXAMPLES
The first example shows how to declare a two-dimensional array
of elements of type
byte
with a
typedef .
typedef array { byte aa[4] }; /* typedefs must be global */
init {
array a[8]; /* 8x4 = 32 bytes total */
a[3].aa[1] = 5
}
The following example introduces two user-defined types named
D
and
Msg ,
and declares an array of two objects of the type
Msg ,
named
top .
typedef D {
short f;
byte g
};
typedef Msg {
byte a[3];
int fld1;
D fld2;
chan p[3];
bit b
};
Msg top[2];
The elements of
top
can be referenced as, for instance:
top[1].fld2.g = top[0].a[2]The types can be used with channels, for instance:
chan q = [2] of { Msg };
q!top[0]; q?top[1]
is a way to recursively copy the contents of all fields
from the first element of
top
into the second element.
SEE ALSO
arrays(2), datatypes(2), mtype(2).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |