Promela |
Omissions |
float(7) |
NAME
float
-
floating point numbers.
DESCRIPTION
There are no floating point numbers in Promela.
The purpose of a verification model in Promela is to
abstract from the
computational
aspects of a concurrent system, and to focus on the
coordination
(interaction, synchronization) aspects.
Consider, for instance, the verification problem for a sequential C procedure that computes square roots. Exhaustive state-based verification would clearly be the wrong approach here. For a Promela verification model it often suffices to model such a procedure as a simple two-state process that non-deterministically decides to give either the correct or an incorrect answer. For instance:
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 };
again:
sqrt!number,me;
if
:: me?correct
:: me?incorrect -> goto again
fi;
...
}
The data types available in 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 ``states'' that even one
single integer variable could obtain, e.g., when
used as a simple counter, is well beyond the search
space of state-based model checkers. Even integer
quantities, therefore, are to be treated with some
suspicion in verification models, and can very often
advantageously be replaced with
byte
or
bit
variables.
SEE ALSO
datatypes(2).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |