Promela |
Omission |
float |
NAME
float -
floating point numbers.
DESCRIPTION
There are no floating point numbers in basic Promela because
the purpose the language is to encourage abstraction
from the computational aspects of a distributed
application while focusing on the verification of
process interaction, synchronization, and coordination.
Consider, for instance, the verification of a sequential C procedure that computes square roots. Exhaustive state-based verification would not be the best approach to verify this procedure. In a verification model, it often suffices to abstract this type of procedure into a simple two-state demon that non-deterministically decides to give either a correct or incorrect answer. The following example illustrates this approach.
mtype = { number, correct, incorrect }; chan sqrt = [0] of { mtype, chan }; active proctype sqrt_server() { do :: sqrt?number(answer) -> /* abstract from local computations */ if :: answer!correct :: answer!incorrect fi od } active proctype user() { chan me = [0] of { mtype }; do :: sqrt!number(me); if :: me?correct -> break :: me?incorrect -> ... fi; od; ... }The predefined data types from Promela are a compromise between notational convenience and modest constraints that can facilitate the construction of tractable verification models. The largest numeric quantity that can be manipulated is, for instance, a 32-bit integer number. The number of different values that even one single integer variable can record, for instance, when used as a simple counter, is already well beyond the scope of a state-based model checker. Even integer quantities, therefore, are to be treated with some suspicion in verification models, and can very often be replaced advantageously with byte or bit variables.
NOTES
In the newer versions of Spin, there is an indirect way to
use external data types, such as
float , via embedded code and embedded declarations.
The burden on the user to find abstractions can thus
be lightened, in return for a potential increase in
verification complexity.
When using embedded C code, the user can decide separately
if some or all of the embedded data objects should be treated
as part of the state descriptor in the verification model,
with the use of
c_state or
c_track declarators.
See the book for a detailed description.
SEE ALSO
c_code
c_decl
c_expr
datatypes
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |