Spinroot

A forum for Spin users

You are not logged in.

#1 2013-01-07 19:16:49

robstewartuk
Member
Registered: 2013-01-04
Posts: 8

LTL generated claim fails to verify

Hi,

I have a model that has a LTL generated never claim that I cannot verify with spin. It uses a propositional symbol 'p' which is always 1. I would expect the LTL formula '[] p' to therefore always be verifiable, as such in this never claim:

#define p 1
never  {    /* ! [] p */
T0_init:
        if
        :: (! ((p))) -> goto accept_all
        :: (1) -> goto T0_init
        fi;
accept_all:
        skip
}

However, this is not the case...

$ spin -a  model.pml
$ gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c
$ ./pan -m10000  -a -N never_6
To replay the error-trail, goto Simulate/Replay and select "Run"
..
spin: trail ends after 14 steps
MSC: ~G line 326

On line 326 is the "if" line in the never claim. I'm not sure what the "MSC: ~G" line means? Also, interestingly, the model includes 7 processes. If I comment out any one of the "run" lines i.e. reducing the model to 6 processes, then the never claim is successfully verified. I'm also not sure if this problem is something to do with liveliness of my model (is that the "~G" line?). I've tried inserting "progress: " labels prepended on the non-terminating do loops in my model, but no luck.

1) I'm surprised this never claim cannot be verified, as 'p' is always (1)
2) What is "~G" ?
3) Is there anything in the anomaly of 6 processes succeeding, 7 not so ?

Last edited by robstewartuk (2013-01-07 19:18:00)

Offline

#2 2013-01-08 07:45:46

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

Re: LTL generated claim fails to verify

With p equal to 1, the never claim can not report a violation. So, if spin finds an error it has a different cause, e.g. A deadlock or an assertion violation, but it cannot be the never claim.
The syntax MSC ~G was used in the old GUI xspin to color code steps in message sequence charts. It's no longer used for that, but not yet removed from the output...
Nothing special about 6 or 7 processes as far as this never claim is concerned...

Offline

#3 2013-01-08 15:52:03

robstewartuk
Member
Registered: 2013-01-04
Posts: 8

Re: LTL generated claim fails to verify

Hi, thanks.

I've spent a few hours trying to get to the root of this problem. There are no assertions in my code, and as you say, the never claim with the p propositional symbol cannot be violated. And on inspecting the lines on which each process is on following the "trail ends after... #processes 7" signal, I can see that some of them should be executable (variable assignment and so on).

However - I have seemingly solved the problem, though not at all how I would have expected to. At the bottom of my code, I have 7 never claims, all generated from LTL formula. To test each one, I have in the "verification" tab in ispin, selected "use claim" and typed in "never_0" or "never_1" or "never_2"... up to "never_6". The never claim "! [] p" was the bottom claim in the source code, and therefore in my mind "never_6". Indeed, when I look through the trail of the failed runs, it is executing lines within this never claim.

How did I fix it? I simply removed the other 6 never claims from my source code, leaving only this one. This time when I select "use claim", I leave the "claim name" box blank, as there is only one. This time, SPIN cannot find any violations in my never claim, and no errors are thrown. What is going on here? Am I misunderstanding the ispin interface for verifying never claims? This is the before and after runs:  https://gist.github.com/4484319 .

Offline

#4 2013-01-08 16:10:45

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

Re: LTL generated claim fails to verify

Just look at the actual error message that ./pan gives you for the first case...

Offline

#5 2013-01-08 16:15:05

robstewartuk
Member
Registered: 2013-01-04
Posts: 8

Re: LTL generated claim fails to verify

Oh dead oh dear.

Don't I look stupid. -DVECTORSZ=1100 fixes everything, and the never claims are verified as I would expect.

Offline

#6 2013-01-08 17:08:40

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

Re: LTL generated claim fails to verify

don't worry -- happens to all of us! ;-)

Offline

Board footer

Powered by FluxBB