PlusCal: Why does fair algorithm still stutter?

Question

I've used PlusCal to model a trivial state machine that accepts strings matching the regular expression (X*)(Y).

(*--fair algorithm stateMachine
variables
    state = "start";

begin

Loop:    
while state /= "end" do
    either
        \* we got an X, keep going
        state := "reading"
    or
        \* we got a Y, terminate
        state := "end"
    end either;
end while;


end algorithm;*)

Even though I've marked the algorithm fair, the following temporal condition fails because of stuttering ... the model checker allows for the case where the state machine absorbs an X and then simply stops at Loop without doing anything else ever again.

MachineTerminates == <>[](state = "end")

What does fairness actually mean in the context of a simple process like this one? Is there a way to tell the model checker that the state machine will never run out of inputs and thus will always terminate?

Answer 1

Okay, so this is very weird and should pass, but not for the the reason you'd think. To understand why, we first have to talk about the "usual" definition of fairness, then the technical one.

Weak fairness says that if an action is never disabled, it will eventually happen. What you probably expected is the following:

1. Loop could pick "end" but doesn't.
2. Loop could pick "end" but doesn't. This happens some arbitrary number of times.
3. Since Loop is fair*, it is forced to pick "end".
4. We're done.

But that's not the case. Fairness, in pluscal, is at the label level. It doesn't say anything about what happens in the label, just that label itself must happen. So this is a perfectly valid behavior:

1. Because loop is never disabled, it eventually happens. It picks "reading".
2. Because loop is never disabled, it eventually happens. It picks "reading".
3. Because loop is never disabled, it eventually happens. It picks "reading".
4. This keeps going forever.

This corresponds to you inputting a string of infinite length, consisting only of X's. If you only want finite strings, you have to explicitly express that, either as part of the spec or as one of the preconditions to your desired temporal property. For example, you could make your temporal property state = "end" ~> Termination, you could model the input string, you could add a count for "how many x's before the y", etc. This gets out of what's actually wrong and into what's good spec design, though.

That's the normal case. But this is a very, very specific exception to the rule. That's because of how "fairness is defined". Formally, WF_vars(A) == <>[](Enabled <<A>>_v) => []<><<A>>_v. We usually translate that as

If the system is always able to do A, then it will keep on doing A.

That's the interpretation I was using up until now. But it is wrong in one very big way. <<A>>_vars == A /\ (vars' /= vars), or "A happens and vars changes. So our definition actually is

If the system is always able to do A in a way that changes its state, then it will keep on doing A in a way that changes its state.

Once you have pc = "Loop" /\ state = "reading", doing state := "reading" does not change the state of the system, so it doesn't count as <<Next>>_vars. So <<Next>>_vars didn't actually happen, but by weak fairness it must eventually happen. The only way for <<Next>>_vars to happen is if the loop sets state := "reading, which allows the while loop to terminate.

This is a pretty unstable situation. Any slight change we make to the spec is likely to push us back into more familiar territory. For example, the following spec will not terminate, as expected:

variables
    state = "start";
    foo = TRUE;        
begin
Loop:    
while state /= "end" do
    foo := ~foo;
    either
        \* we got an X, keep going
        state := "reading"
    or
        \* we got a Y, terminate
        state := "end"
    end either;
end while;
end algorithm;*)

Even though foo doesn't affect the rest of the code, it allows us to have vars' /= vars without having to update state. Similarly, replacing WF_vars(Next) with WF_pc(Next) makes the spec fail, as we can reach a state where <<Next>>_pc is disabled (aka any state where state = "reading").

*Loop isn't fair, the total algorithm is. This can make a big difference in some cases, which is why we spec. But it's easier in this case to talk about Loop, as it's the only action.