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.

]]>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.

]]>i will look into it -- thanks for the example!]]>

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