SPIN: Visit statements infinitely often

Question

I'm wondering whether it's possible to verify an LTL property in a program with a fairness constraint that states that multiple statements must be executed infinitely often.

E.g.:

bool no_flip;
bool flag;

active[1] proctype node()
{
  do
  :: skip -> progress00: no_flip = 1
  :: skip -> progress01: flag = 1
  :: !no_flip -> flag = 0
  od;
}

// eventually we have flag==1 forever
ltl p0  { <> ([] (flag == 1)) }

This program is correct iff eventually the no_flip flag becomes true and flag becomes true.

However, running both 'pan -a' and 'pan -a -f' (weak fairness) yields a cycle through the no_flip=1 statement and the acceptance state (from LTL formula).

I thought the progress labels would enforce that the execution passed through them infinitely often, but that doesn't seem to be the case. So, is it possible to add such kind of fairness constraints?

Thanks, Nuno

Answer 1

Just the inclusion of a progress label itself does not guarantee that the execution will be limited to non-progress cases. You need to add 'non-progress' somewhere in your ltl or never claim.

As a never claim you enforce progress with <>[](np_) (using spin -p '<>[](np_)' to generate the never claim itself). A possible ltl form for your verification is:

ltl { []<>!(np_) && <>[](flag==1) }

Also note that making 'progress' does not mean visiting each progress label infinitely often; it means visiting any progress label infinitely often. So, when enforcing progress, a viable path through your code is the first do option - which is not what you expect.

Answer 2

Answering my own question, for this simple example, I can split each loop branch into separate processes. Then by running pan in weak fairness mode, I have the guarantee that each process will be scheduled eventually. However, this "solution" is not very interesting for my case, since I have a model with dozens of branches in each process.. Any other ideas?

bool no_flip;
bool flag;

active[1] proctype n1()
{
  do
  :: skip -> no_flip = 1
  od;
}

active[1] proctype n2()
{
  do
  :: skip -> flag = 1
  od;
}

active[1] proctype n3()
{
  do
  :: !no_flip -> flag = 0
  od;
}

// eventually we have flag==1 forever
ltl p0  { <>[] (flag == 1) }