Promela Reference -- rand(6)




rand - for random number generation.

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:

Note that the verifier would generate at least 256 distinct reachable states for this model. The simulator, on the other hand, would traverse the model only once, but it could execute a sequence of any length (from one to infinitely many execution steps). A simulation run will only terminate if the simulator eventually selects the break option (which is guaranteed only in a statistical sense).

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.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 13 November 2015)