Promela Reference -- typedef(2)

Promela

Declarator

typedef


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, with some mild restrictions, they can be used as formal and actual parameters for proctype declarations and instantiations, 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 it 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 .

The following example introduces two user-defined types named D and Msg , and declares an array of two objects of type Msg , named top : The elements of top can be referenced as, for instance: Objects of type Msg can be passed through a channel, provided that they do not contain any field of type unsigned, and provided that they do not contain arrays of typedef'ed structures. If we delete all arrays from the declaration of type Msg we can also use objects of this type in a run parameter, for instance, as follows:

NOTES
The current Spin implementation imposes the following restrictions on the use of typedef objects. It is not possible to assign the value of a complete typedef object directly to another such object of the same type in a single assignment.
A typedef object may be sent through a message channel as a unit provided that it contains no fields of type unsigned and no arrays of typedef'ed structures.
A typedef object can also be used as a parameter in a run statement, but in this case it may not contain any arrays.

Beware that the use of this keyword differs from its namesake in the C programming language. The working of the C version of a typedef statement is best approximated with a macro definition.

SEE ALSO
arrays
datatypes
macros
mtype


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 2 May 2009)