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 */

}

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