Spinroot

A forum for Spin users

You are not logged in.

#1 2011-05-10 16:36:17

heinz
Member
Registered: 2011-04-29
Posts: 6

weak fairness affects simple model

Hello,
I just observed that enabling/disabling weak fairness (wf) affects the outcome of verifying "<>[](n==1)" in the following simple model:

byte n = 0;
active proctype P() { n=1 }
active proctype Q() { n=2 }

Clearly, there should be two endstates with n==1 and n==2, respectively. Spin reports an error for the above ltl-formula only if wf is turned off, which I find surprising because I don't think that there are unfair computation paths. The same behaviour appears when "1" is replaced by "0" or "2" in the formula. For values n==3,4,... there is always an error reported by spin independently from wf.

A similar behaviour can be observed with "<>[](n==0)" and the following model:

byte n = 0;
active proctype P() {
   if
     :: n=1
     :: n=2
   fi
}

So my question is why does enabling/disabling weak fairness have an effect on these verifications?

Many thanks in advance,
Heinz

Offline

#2 2011-05-10 17:31:33

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: weak fairness affects simple model

this is indeed surprising, and likely a bug
i will look into it -- thanks for the example!

Offline

#3 2011-05-10 19:11:45

heinz
Member
Registered: 2011-04-29
Posts: 6

Re: weak fairness affects simple model

Here is some more information that might help:

When looking at the reachable states in the system automaton after verification (using spin spider) there is only one endstate present, namely the one with n==1. There is a transition in the diagram from state (P:end, Q: n=2, n==1 ) to state (P:end, Q:end, n==1), so setting n=2 is not recognized.

I checked that this was also true in spin version 4.3.0.

Offline

#4 2011-05-10 21:58:31

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: weak fairness affects simple model

It is indeed a bug. It will be fixed in version 6.1.1.

It is a subtle interaction between the fairness algorithm and the cycle detection algorithm that has been hiding in Spin for probably about 20 years now! The cycle is actually found, but not reported in this case because of a mistake.

Thanks very much for your very clear example that allowed me to pin this down and fix it.

Offline

Board footer

Powered by FluxBB