Promela Reference -- typedef(2)





typedef - to declare a user-defined structured data type.

typedef name { decl_lst }

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.

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.

arrays(2), datatypes(2), mtype(2).

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