Spinroot

A forum for Spin users

You are not logged in.

#1 2012-05-12 23:33:42

alb012
Member
Registered: 2012-05-12
Posts: 1

verification problem

Hello spinroot,

I have the following program, where []a should hold:

bit p;

init
{
	p = 1;
}

#define a p

active proctype test()
{
  d_step { p = 1;}
  do
    :: p -> goto accept
  od;
  accept: printf("Accepted");
}


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

But there is an error:

$ spin -a source.pml
$ gcc -o pan pan.c
$ ./pan -m2000 -x -a
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: end state in claim reached (at depth 3)
pan: wrote source.pml.trail

(Spin Version 6.1.0 -- 2 May 2011)
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 36 byte, depth reached 3, errors: 1
        2 states, stored
        0 states, matched
        2 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 (unsuccessful compression: 238334.38%)
         	state-vector as stored = 152506 byte + 28 byte overhead
    4.000	memory used for hash table (-w19)
    0.107	memory used for DFS stack (-m2000)
    4.302	total actual memory usage


pan: elapsed time 0 seconds

$ spin -t -p source.pml
Never claim moves to line 23	[(!(p))]
  2:	proc  1 (test) source.pml:12 (state 2)	[p = 1]
Never claim moves to line 27	[(1)]
spin: trail ends after 3 steps
#processes: 2
		p = 1
  3:	proc  1 (test) source.pml:13 (state 5)
  3:	proc  0 (:init:) source.pml:5 (state 1)
  3:	proc  - (never_0) source.pml:28 (state 8) <valid end state>
2 processes created

I don't understand the following lines.

...
Never claim moves to line 23	[(!(p))]
  2:	proc  1 (test) source.pml:12 (state 2)	[p = 1]
Never claim moves to line 27	[(1)]
...

Never claim searches for p=0 , but it is always p=1. Why does never claim move to  line 27    [(1)]?
(Actually in line 27 there is "skip" and not (1) ).


What am I doing wrong?

Thanks!

Last edited by alb012 (2012-05-12 23:39:38)

Offline

#2 2012-05-13 04:34:09

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

Re: verification problem

p is not always 1 -- the initial value is 0....

Offline

Board footer

Powered by FluxBB