salesforce
random numbers in rules cause trouble
@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:
- during model checking, any rule generates a random number,
- 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.
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.
There's more related discussion on the runway-dev thread Does urandom function nondeterministically in modelchecking mode?
