Promela Reference -- float(6)




float - floating point numbers.

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.

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.

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.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)