Promela Reference -- datatypes(2)

Promela

Declarator

datatypes


NAME
bit , bool , byte , pid , short , int , unsigned - predefined data types.

SYNTAX
typename name [ = anyexpr ]

unsigned name : constant [ = anyexpr ]

DESCRIPTION
There are seven predefined integer data types: bit , bool , byte , pid , short , int , and unsigned . There are also constructors for user-defined data types (see the manual pages for mtype , and typedef ), and there is a separate predefined data type for message passing channels (see the manual page for chan ).

Variables of the predefined types can be declared in C-like style, with a declaration that consists of a typename followed by a comma-separated list of one or more identifiers. Each variable can optionally be followed by an initializer. Each variable can also optionally be declared as an array, rather than as a scalar (see the manual page for arrays ).

The predefined data types differ only in the domain of integer values that they provide. The precise domain may be system dependent in the same way that the corresponding data types in the C language can be system dependent.

Variables of type bit and bool are stored in a single bit of memory, which means that they can hold only binary, or boolean values.

ISO compliant implementations of C define the domains of all integer data types in a system header file named limits.h , which is accessible by the C compiler. The table summarizes these definitions for a typical system.

Variables of type unsigned are stored in the number of bits that is specified in the (required) constant field from the declaration. For instance,

declares a variable named x that is stored in five bits of memory. This declaration also states that the variable is to be initialized to the value 15. As with all variable declarations, an explicit initialization field is optional. The default initial value for all variables is zero. This applies both to scalar variables and to array variables, and it applies to both global and to local variables.

If an attempt is made to assign a value outside the domain of the variable type, the actual value assigned is obtained by a type cast operation that truncates the value to the domain. Information is lost if such a truncation is applied. Spin will warn if this happens only during random or guided simulation runs.

Scope: The scope of a variable declaration is global if it appears outside all proctype or init declarations. The scope of a local variable includes the complete body of a proctype . The declaration itself can be placed anywhere within the proctype or init declaration, provided only that it appears before the first use of the variable. Each separate process has a private copy of all variables that are declared locally within the corresponding proctype or init declaration.

The formal parameters of a proctype are indistinguishable from local variables. These formal parameters are initialized to the values that are specified in a run statement, or they are initialized to zero when the process is instantiated through an active prefix on a proctype declaration.

EXAMPLES
The code fragment

declares the names a and b as variables of type byte , and c as an array of three variables of type short . Variable a has the default initial value zero. Variable b is initialized to the value 2 , and all three elements of array c are initialized to 3 .

A variable may also be initialized with an expression, but this is generally not recommended. Note that if global variables are referenced in such initializations, the precise value of such globals may be uncertain.

NOTES
Each process has a predefined local variable _pid of type pid that holds the process instantiation number. Each model also has a predefined, write-only, global variable _ (underscore) of type int that can be used as a scratch variable, and predefined, read-only, global variables _nr_pr (of type int ) and _last (of type pid ). See the corresponding manual pages for further details on these variables.

An array of bit , bool , or unsigned variables is stored internally as an array of byte variables. This may affect the behavior of the model if, for instance, the user relies on automatic truncation effects during a verification (an unwise strategy). When the verifier source is generated in verbose mode, Spin will warn if it encounters such cases.

In the C language, the keywords short and unsigned can be used as a prefix of int . This is not valid in Promela.

SEE ALSO
_
_last
_pid
arrays
chan
mtype
run
typedef


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 8 March 2013)