NAME
rand - for random number generation.

DESCRIPTION
There is no predefined 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 full range of the random numbers that could be generated: usually a huge number. 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, and 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 effectively all options for behavior will be explored in this mode, one at a time.

Promela's equivalent of a ``random number generator'' is the following program:

active proctype randnr()
{	/*
	 * don't call this rand()...
	 * to avoid a clash with the C library routine
	 */
	byte nr;	/* pick random value  */
	do
	:: nr++		/* randomly increment */
	:: nr--		/* or decrement       */
	:: break	/* or stop            */
	od;
	printf("nr: %d\n")	/* nr: 0..255 */
}

NOTES
Through the use of embedded C code, a user can surreptitiously include calls on an external C library rand() function into a model. To avoid problems with irreproducible behavior, the Spin-generated verifiers intercept such calls and redefine them in such a way that the depth-first search process at the very least remains deterministic. Spin accomplishes this by pre-allocating an integer array of the maximum search depth maxdepth , and filling that array with the first maxdepth random numbers that are generated. Those numbers are then reused each time the search returns to a previously visited point in the search, to secure the sanity of the search process.

The seed for this pre-computation of random numbers is fixed, so that subsequent runs will always give the same result, and to allow for the faithful replay of error scenarios. Even though this provides some safeguards, the use of random number generation is best avoided, also in embedded C code.

SEE ALSO
c_code
c_expr
if
do