random numbers in rules cause trouble

[ongardie]

@vidbina ran into an issue where using urandomRange() in a rule got the simulator confused about which rules were active vs inactive. See this conversation on Twitter: https://twitter.com/ongardie/status/735474014798413825. I suggested using a rule-for to hoist the random number generation out of the rule and into the simulator.

Similarly, since the bananas model generates a random number of bananas to bring back from the store, we can't effectively use the model checker on it.

I think the possibly bad conditions are these:

1. during model checking, any rule generates a random number,
2. during simulation, a rule (active or inactive) generates a random number that affects control flow.

Hrm, that's a bit difficult to warn about because of the "affects control flow", will have to think more.

[dgryski]

The solution Spin takes when checking a model that includes randomness is to try all the possibilities. For the bananas case, that means each trip to the store means 9 (0..8) more states to check.

[ongardie-sfdc]

There's more related discussion on the runway-dev thread Does urandom function nondeterministically in modelchecking mode?