Does urandom function nondeterministically in modelchecking mode?

[Andrew Helwer]

If I have the following code:

type ValueRange : 1 .. 5;

var Value : ValueRange = 1;

rule SetValue {
    Value = urandom<ValueRange>();
}

Does the call to urandom make the SetValue rule nondeterministic? That would be an elegant & intuitive way of doing nondeterministic value assignment!

[Andrew Helwer]

To clear up ambiguity: the real question I was asking is whether urandom makes the model checker branch out on all possible assignments at this point, or it picks a single random value and that's the only next state found.

I found the answer myself by modifying above code as follows:

type ValueRange : 1 .. 5;

var Value : ValueRange = 1;

rule SetValue {

    if (Value == 1) {

        Value = urandom<ValueRange>();
    }
}

If urandom caused the model checker to branch, we would expect it to find five states. However, it only finds two states.

Would be a neat feature, though!

[Damian Gryski]

On Monday, July 4, 2016 at 7:21:24 AM UTC+2, Andrew Helwer wrote:

To clear up ambiguity: the real question I was asking is whether urandom makes the model checker branch out on all possible assignments at this point, or it picks a single random value and that's the only next state found.

I found the answer myself by modifying above code as follows:

type ValueRange : 1 .. 5;

var Value : ValueRange = 1;

rule SetValue {
    if (Value == 1) {
        Value = urandom<ValueRange>();
    }
}

If urandom caused the model checker to branch, we would expect it to find five states. However, it only finds two states.

Would be a neat feature, though!

This issue also affects the "too many bananas" model, as it randomly selects a number of bananas to return.

In Promela (the language used by Spin), selecting a random value is done with a single non-deterministic choice which, during verification, all possibly options are tried.

Damian 

[Diego Ongaro]

Correct. Random numbers and model checking in Runway aren't currently compatible. And random numbers are causing trouble with the simulator too (runway-compiler#2), which might find that a rule is inactive just because it picked an unlucky number when it tested whether applying the rule would cause state changes. This is a pretty important issue that would be great to make progress on.

One possibility, as Andrew brought up in his original post, is to try to hoist random numbers up to the rule level automatically. So if I ask for a die roll in my rule, I'll end up with a rule instantiated for outcome 1, another for 2, another for 3, etc. This would probably work fine for the banana model, but there are some major challenges to overcome in general. It'd be difficult to support dynamic ranges (m..n as opposed to 1..6). It'd be even harder to support random numbers generated within in loops/recursion. That might not quite be equivalent to the halting problem, but it's getting close.

Maybe an easier approach is to take away urandom altogether, and have models take randomness in as parameters to rules, similar to rule-for today. That means you'd get O(1) random values per rule. Is that too restrictive?

The way rule-for works today is that it instantiates a new child rule for every possible value in an iterable. For example, `rule for person in roommates` will instantiate `size(roommates)` child rules. Implementing random numbers the same way would be easy, but it'd generate rules based on the size of the random range. This would only work well for small ranges of random numbers. 10000..20000 wouldn't be ok, yet that's something the Raft model does to randomize message latency during simulation (perhaps it's relevant that this isn't used in asynchronous model checking for Raft).

On the other hand, what if we didn't instantiate a different rule for each possible random value? Then the random value would be symbolic; i.e., we wouldn't have a concrete value when evaluating whether a rule changes state. Yet logic might depend on it, like `if randomValue < 50 { ... } else { ... }`. And that might be in loops/recursion. Hmm. Maybe we need to restrict the use of random values in some significant way?