Spinroot

Thank you.

I have a follow up question with respect to "What spin will prove is that the positive requirement can be violated, by showing that the negated requirement can be satisfied". Below is an example, a simple verification attempt based on '[] (sr -> <> rr)'. When you wanted to verify that messages may be lost, I want to verify that the boolean 'dead' may be true.

bool dead;

active proctype Foo(){
dead = false;
do
:: dead = true -> skip;
:: skip -> 
   progess: skip ;
od
}

#define alive ( !dead )

never  {    /* ! [] alive */
T0_init:
        do
        :: atomic { (! ((alive))) -> assert(!(! ((alive)))) }
        :: (1) -> goto T0_init
        od;
accept_all:
        skip
}

My positive requirement is that the alive symbol is always true i.e. '[] alive' therefore dead always false, which is intuitively not verifiable. "What spin will prove is that the positive requirement can be violated, by showing that the negated requirement can be satisfied." So, I try and verify the negated claim '! [] alive'. When I attempt to validate this never claim, however, I cannot.

verification result:
spin -a  test_negation.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c
./pan -m10000  -a -N never_0
Pid: 2039
warning: only one claim defined, -N ignored
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: assertion violated  !( !( !(dead))) (at depth 4)
pan: wrote test_negation.pml.trail

(Spin Version 6.2.5 -- 3 May 2013)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (never_0)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 28 byte, depth reached 4, errors: 1
        3 states, stored
        0 states, matched
        3 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000	equivalent memory usage for states (stored*(State-vector + overhead))
    0.291	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  128.730	total actual memory usage

This doesn't seem to follow with the description from Section 4.3.2 of "The Model Checker SPIN". I must still be missing something?

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 .