A forum for Spin users
You are not logged in.
Pages: 1
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
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
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
Oh dead oh dear.
Don't I look stupid. -DVECTORSZ=1100 fixes everything, and the never claims are verified as I would expect.
Offline
Pages: 1