Promela Reference -- rand(7)

Google

Promela

Omissions

rand(7)

NAME
rand - for random number generation.

DESCRIPTION
There is no random number generation function in Promela. The reason is that during a verification we effectively check for all possible executions of a system. Having even a single occurrence of a call on the random number generator would increase the number of cases to inspect by the range of the generator. Random number generators can be useful on a simulation, but they can be disastrous when allowed in verification.

In almost all cases, Promela's notion of non-determinism can replace the need for a random number generator. Note that to make a random choice between N alternatives, it suffices to place these N alternatives in a selection structure with N options. The verifier will interpret the non-determinism accurately, an is not bound to the restrictions of a pseudo-random number generation algorithm.

During random simulations, Spin will internally make calls on a (pseudo) random number generator to resolve all cases of non-determinism. During verifications no such calls are made (because all cases are effectively considered here, one at a time).

Promela's equivalent of a ``random number generator'' could be the following program.

active proctype randnr()

{	/* don't call this rand()...

	 * to avoid a clash with the C-routine

	 */

	byte nr;	/* force a value modulo 256 */

	do

	:: nr++		/* randomly increment */

	:: nr--		/* or decrement */

	:: break	/* or stop */

	do;

	printf("nr: %d\n")	/* nr: 0..255 */

}

Note that the verifier would generate at least 256 distinct reachable states for this model. The simulator would traverse it once, and could execute any number of steps (from one to infinitely many...).

SEE ALSO
if(3), do(3).


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)