verifying models with priorities

mlfv · 2013-04-29 22:42:20

Hi,

I am trying to verify some recursive nets with SPIN. I used priorities to simulate synchronizations e.g. between the parent net (process) and the child nets. However, I got some unexpected verification errors, e.g.,

spin -a rpnFactPriorities.pml
ltl t: [] ((! (((p4>0)) && ((_nr_pr==1)))) || (((((p2==0)) && ((len(p3.d)==0))) && ((p1==((a-f)+1)))) && ((p5==f))))
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNOREDUCE -w -o pan pan.c
./pan -m10000 -a -N t
Pid: 4936
pan:1: used: enabled(pid=thisproc) (at depth 107)
pan: wrote rpnFactPriorities.pml.trail

*** Could you tell me why does this error occur? Thanks in advance.

Here is the model I used.

1 typedef NetPlace { chan d = [3] of {short,byte,byte,bit} }
2
3 inline sP(p, e) { set_priority(p,e); }
4
5 inline consNetTok(c, p) {
6    do:: c ?? [eval(p),_,_,0] -> c ?? eval(p),_,_,0;
7    :: else -> break
8    od; skip }
9
10 inline fT(bp,l,k) { d_step{
11    bp > 0 &&
12    ! pc ?? [eval(_pid),l,k,0] -> pc ! _pid,l,k,0 } }
13
14 inline dT(k) { if :: pc ?? [_pid,_,k,0] -> pc ?? _pid,_,k,0 :: else fi }
15
16 byte p1, p5, f;
17
18 byte p2, p4, a; NetPlace p3;
19
20 ltl t { []((p4>0 && _nr_pr == 1) -> (p2==0 && len(p3.d)==0 && p1==a-f+1 && p5==f))}
21
22 proctype netF(chan pc){
23    byte p6 = 1, p8, nt, it; NetPlace p7; f++;
24    do::
25    do
26    :: fT(p6,10,3)
27    :: d_step{ p6>0 && p1>0 ->
28    sP(_pid, 3);
29    p1--; p6--; dT(3);
30    pc ! _pid,0,4,1 }
31    :: d_step{
32    p7.d ?? [_,10,_,0] ->
33    sP(_pid, 3);
34    p7.d ?? nt,10,it,0;
35    consNetTok(p7.d, nt);
36    p7.d ! nt,11,it,1; sP(nt, 2);
37    p8++;
38    sP(_pid, 1); }
39    :: fT(p8,10,6)
40    od unless atomic{ pc ?? eval(_pid),_, it,1 -> sP(_pid, 3) }
41    if :: atomic{ it == 4 ->
42    nt = run netF(p7.d);
43    p7.d ! nt, 255,0,0 ;
44    sP(_pid, 1); }
45    :: atomic{ it == 3 -> p6--; p5++; break }
46    :: atomic{ it == 6 -> p8--; p5++; break }
47    :: atomic{ it == 0 -> break }
48    fi
49    od; sP(_pid, 1); }
50
51 init{
52    byte nt, it;
53 p1=3; p2=1; a=p1; p4 =0; p5=0;
54 end: do :: atomic{ p2>0 ->
55    sP(_pid, 3);
56    p2--;
57    nt = run netF(p3.d);
58    p3.d ! nt,255,0,0;
59    sP(_pid, 1); }
60    :: atomic{
61    p3.d ?? [_,10,_,0] ->
62    sP(_pid, 3);
63    p3.d ?? nt,10,it,0;
64    consNetTok(p3.d,nt);
65    p3.d ! nt,11,it,1; sP(nt, 2);
66    p4++;
67    sP(_pid, 1); }
68    od }

spinroot · 2013-04-30 04:31:10

Yes I believe this is a bug that was reported earlier. It will be fixed in the next release (6.2.5)

mlfv · 2013-04-30 13:32:20

Maybe the problem is due to the combination with the unless construction. In a similar model, the variable 'it' is not properly updated after the escape sequence and the next transition fails. Btw, have you considered to include a statement to terminate a process, e.g. return? In this model, for example, I would like to replace the break in lines 45, 46 and 47 in order to reach the termination state as soon as the atomic region is completed.

spinroot · 2013-04-30 16:18:53

if you want to fix the bug before 6.2.5 is released, please lookup the definition of the function "highest priority", which is defined in an array in pangen1.h, and make it match this new definition:
"int",
"highest_priority(int pid, Trans *t)",
"{ int i; uchar *othis = this;",
"",
"#ifdef VERI",
" if (pid == 0)",
" { return 1;", /* never claim */
" }",
"#endif",
"#ifdef HAS_PROVIDED",
" i = pid+BASE;", /* uncorrected process number */
"#endif",
" if (i < 0",
" || i >= (int) now._nr_pr",
"#ifdef HAS_PROVIDED",
" || !provided(i, (uchar) ((P0 *)this)->_t, (int) ((P0 *)this)->_p, t)",
"#endif",
" )",
" { return 0;",
" }",
"",
" for (i = BASE; i < now._nr_pr; i++)", /* all except never, if present */
" { this = pptr(i);",
" if (i != pid+BASE",
" && ((P0 *)this)->_priority > ((P0 *)pptr(pid+BASE))->_priority",
"#ifdef HAS_PROVIDED",
" && provided(i, (uchar) ((P0 *)this)->_t, (int) ((P0 *)this)->_p, 0)",
"#endif",
" && enabled(i+1, i-BASE))", /* enabled adds back BASE in 2nd arg */
" { this = othis;",
" return 0;",
" } }",
" this = othis;",
" return 1;",
"}",

mlfv · 2013-05-02 13:18:40

Thanks for the quick response. However, I didn't find the file pangen1.h. I am using Spin 6.2.4 and iSpin 1.1.0.

mlfv · 2013-05-02 15:10:39

Back to the use of the break in the above example, there might be a bug when it is used inside the unless. In the model, if priorities are disabled (the body of sP is skip) and the last part of netF is replaced as follows, then I got an invalid end state; it seems that the break do not terminate the outer do. The same happens without using an atomic region.

40 od unless atomic{ pc ?? eval(_pid),_, it,1 -> sP(_pid, 3);
41 if :: { it == 4 ->
42 nt = run netF(p7.d);
43 p7.d ! nt, 255,0,0 ;
44 sP(_pid, 1); }
45 :: { it == 3 -> p6--; p5++; break }
46 :: { it == 6 -> p8--; p5++; break }
47 :: { it == 0 -> break }
48 fi; sP(_pid, 1); }
49 od; }

On the other hand, when the if is placed outside the unless no error is found.

40 od unless atomic{ pc ?? eval(_pid),_, it,1 -> sP(_pid, 3); }
41 if :: { it == 4 ->
42 nt = run netF(p7.d);
43 p7.d ! nt, 255,0,0 ;
44 sP(_pid, 1); }
45 :: { it == 3 -> p6--; p5++; break }
46 :: { it == 6 -> p8--; p5++; break }
47 :: { it == 0 -> break }
48 fi; sP(_pid, 1);
49 od; }

Is there something wrong I am missing in the first variant?

spinroot · 2013-05-03 05:32:30

Just a quick follow-up: your first example reveals a bug in the code generation by Spin.
I will fix it and see if the symptom your saw also disappears.
Thanks for reporting the detailed example!

spinroot · 2013-05-03 18:30:29

The problem has been fixed. I will put the new release 6.2.5 into the distribution later this weekend.
Thanks again for the bug-report.

spinroot · 2013-05-05 00:44:29

Spin Version 6.2.5 is now in the distribution -- it should fix the problems you've reported.
Let me know if you see anything else that looks wrong.

mlfv · 2013-05-05 03:08:55

Hi spinroot and thanks a lot for your prompt replies! I verified the model and the first error was fixed. However, I am still concerned with the break issue (Post #6). It would be very useful for me to include the if in the atomic region of the unless, in order to reduce the state space of larger models. But even in this new release, I got an invalid end state (regardless the use of priorities) I can't understand. Could you please clarify me about this?

spinroot · 2013-05-05 21:10:30

you are correct -- this is also a bug, as shown by the following small example:
init {
do
:: printf("A\n"); do :: 1 od unless if :: 2 -> break fi
od;
assert(false)
}
clearly here the assertion violation is possible, but not detected.
omitting the inner-do loop, or the if..fi selection in the unless makes the bug go away.
i'll check the cause of this problem
thanks again for reporting this!

spinroot · 2013-05-05 23:59:03

Short term solutions to the problem:
put curly braces around the main sequence (the inner do-loop) of the unless,
or replace the problematic break statement with an explicit goto
Spin Version 6.2.6 will have the real fix to prevent this problem from occurring.

mlfv · 2013-05-07 00:31:37

Hi and thanks for the hints, the curly braces solved the error. Here is a larger model involving priorities. In this case, the error trace has a failing transition at step 13. It seems that the value of 'it' is changed after executing the unless.

1 typedef NetPlace { chan d =
2    [15] of {byte,byte,bit} }
3
4 inline sP(p, e){ set_priority(p,e); }
5 /*inline sP(p, e){ skip; }*/
6
7 inline consNetTok(c, p) {
8    do :: c ??[eval(p),_,0] ->
9    c ??eval(p),_,0;
10    :: else -> break
11    od; skip }
12
13 inline fS(l) { d_step{
14    !pc??[_,l,0] -> pc!_pid,l,0 } }
15
16 inline fT(bp,l) { d_step{
17    bp > 0 &&
18    !pc??[_,l,0] -> pc!_pid,l,0 } }
19
20 inline cT(bp,n,l) { d_step{
21    bp > 0 && !pc??[eval(_pid),l,0]
22    && pc??[_,l,0] ->
23    sP(_pid, 3); pc??n,l,0;
24    pc!n,l,1; pc!_pid,l,1;
25    sP(n, 2); } }
26
27 inline cS(n,l) { d_step{
28    !pc??[eval(_pid),l,0] &&
29    pc??[_,l,0] ->
30    sP(_pid, 3); pc??n,l,0;
31    pc!n,l,1; pc!_pid,l,1;
32    sP(n, 2); } }
33
34 inline dT(l) {
35    if :: pc ?? [eval(_pid),l,0] ->
36    pc ?? eval(_pid),l,0
37    :: else fi }
38
39 proctype netLWF1(chan pc){
40    byte p1=1, p2,p3,p4,p5,nt,it;
41    do ::
42    do :: fT(p1,2) :: cT(p1,nt,2)
43    :: fT(p2,3) :: cT(p2,nt,3)
44    :: fT(p3,5) :: cT(p3,nt,5)
45    :: fT(p3,6) :: cT(p3,nt,6)
46    :: fT(p4,7) :: cT(p4,nt,7)
47    :: fT(p5,10)
48    :: d_step{p2 > 0 ->
49    sP(_pid, 3); p2--;
50    dT(3); p3++; sP(_pid, 1) }
51    od unless atomic{
52    pc ?? eval(_pid),it,1; sP(_pid, 3); }
53    if :: atomic{ it==2 -> p1--; p2++; }
54    :: atomic{ it==3 -> p2--; p3++; }
55    :: atomic{ it==5 -> p3--; dT(6);
56    p4++; }
57    :: atomic{ it==6 -> p3--; dT(5);
58    p4++; }
59    :: atomic{ it==7 -> p4--; p5++;}
60    :: atomic{ it==11 -> break }
61    :: atomic{ it==0 -> break }
62    fi ; sP(_pid, 1);
63    od; }
64
65 proctype netLWF2(chan pc){
66    byte p1=1, p2,p3,p4,p5,n,it;
67    do ::
68    do :: fT(p1,1) :: cT(p1,n,1)
69    :: fT(p2,3) :: cT(p3,n,3)
70    :: d_step{ p2 > 0 ->
71    sP(_pid, 3);
72    p2--; p3++;
73    dT(3); sP(_pid, 1);
74    }
75    :: fT(p3,4) :: cT(p3,n,4)
76    :: fT(p4,8) :: cT(p4,n,8)
77    :: fT(p5,10)
78    od unless atomic{
79    pc ?? eval(_pid),it,1; sP(_pid, 3); }
80    if :: atomic{ it==1 -> p1--; p2++; }
81    :: atomic{ it==3 -> p2--; p3++; }
82    :: atomic{ it==4 -> p3--; p4++; }
83    :: atomic{ it==8 -> p4--; p5++; }
84    :: atomic{ it==11 -> sP(_pid, 1); break }
85    :: atomic{ it==0 -> sP(_pid, 1); break }
86    fi ; sP(_pid, 1);
87    od; }
88
89
90 proctype netAC(chan pc){
91    byte p1 = 0, p2,p3,n,it;
92    do ::
93    do :: fS(1) :: cS(n,1)
94    :: fT(p1,2) :: cT(p1,n,2)
95    :: fS(4) :: cS(n,4)
96    :: fT(p2,5) :: cT(p2,n,5)
97    :: fT(p2,6) :: cT(p2,n,6)
98    :: fS(7) :: cS(n,7)
99    :: fT(p3,8) :: cT(p3,n,8)
100    od unless atomic{
101    pc ?? eval(_pid),it,1 ; sP(_pid, 3); }
102    if :: atomic{ it==1 -> p1++; }
103    :: atomic{ it==2 -> p1--; }
104    :: atomic{ it==4 -> p2++; }
105    :: atomic{ it==5 -> p2--; dT(6); }
106    :: atomic{ it==6 -> p2--; dT(5); }
107    :: atomic{ it==7 -> p3++; }
108    :: atomic{ it==8 -> p3--; }
109    :: atomic{ it==0 -> break }
110    fi ; sP(_pid, 1);
111    od; }
112
113
114    byte p1 = 1, p3; byte p4; NetPlace p2;
115
116    ltl s { <>(p4>0)}
117
118 init{
119    byte nt;
120    end: do :: atomic{ p1 > 0 ->
121    sP(_pid, 3); p1--;
122    nt = run netLWF1(p2.d);
123    p2.d ! nt, 255,0;
124    nt = run netLWF2(p2.d);
125    p2.d ! nt, 255,0;
126    nt = run netAC(p2.d);
127    p2.d ! nt, 255,0;
128    sP(_pid, 1) }
129    :: atomic{
130    p2.d ?? [_,10,0] ->
131    sP(_pid, 3); p2.d ?? nt,10,0;
132    consNetTok(p2.d, nt);
133    p2.d ! nt,11,1; sP(nt, 2);
134    p3++; sP(_pid, 1) }
135    :: atomic{ p3 >= 2 &&
136    p2.d ?? [_,255,0] ->
137    sP(_pid, 3); p3 = p3-2;
138    p2.d ?? nt,255,0;
139    consNetTok(p2.d, nt);
140    p2.d ! nt,0,1; sP(nt, 2);
141    p4++; sP(_pid, 1); break; }
142    od }
143

spinroot · 2013-05-11 19:47:55

This doesn't happen for me if I perform the verification with Spin 6.2.6.
With ./pan -a Spin finds an error trace, and it replays it correctly with spin -t -p as follows:

$ spin -t -p priorities2.pml
ltl s: <> ((p4>0))
starting claim 4
using statement merging
Never claim moves to line 4 [(!((p4>0)))]
2: proc 0 (:init:) priorities2.pml:125 (state 1) [((p1>0))]
3: proc 0 (:init:) priorities2.pml:4 (state 2) [set_priority(_pid, 3)]
3: proc 0 (:init:) priorities2.pml:126 (state 4) [p1 = (p1-1)]
Starting netLWF1 with pid 2 priority 1
3: proc 0 (:init:) priorities2.pml:127 (state 5) [nt = run netLWF1(p2.d)]
4: proc 0 (:init:) priorities2.pml:128 (state 6) [p2.d!nt,255,0]
Starting netLWF2 with pid 3 priority 1
4: proc 0 (:init:) priorities2.pml:129 (state 7) [nt = run netLWF2(p2.d)]
5: proc 0 (:init:) priorities2.pml:130 (state 8) [p2.d!nt,255,0]
Starting netAC with pid 4 priority 1
5: proc 0 (:init:) priorities2.pml:131 (state 9) [nt = run netAC(p2.d)]
6: proc 0 (:init:) priorities2.pml:132 (state 10) [p2.d!nt,255,0]
7: proc 0 (:init:) priorities2.pml:4 (state 11) [set_priority(_pid, 1)]
9: proc 3 (netAC) priorities2.pml:16 (state 3) [(!(pc??[_,1,0]))]
9: proc 3 (netAC) priorities2.pml:16 (state 2) [pc!_pid,1,0]
11: proc 3 (netAC) priorities2.pml:16 (state 31) [(!(pc??[_,4,0]))]
11: proc 3 (netAC) priorities2.pml:16 (state 30) [pc!_pid,4,0]
13: proc 3 (netAC) priorities2.pml:16 (state 73) [(!(pc??[_,7,0]))]
13: proc 3 (netAC) priorities2.pml:16 (state 72) [pc!_pid,7,0]
15: proc 2 (netLWF2) priorities2.pml:20 (state 13) [((((p1>0)&&!(pc??[eval(_pid),1,0]))&&pc??[_,1,0]))]
15: proc 2 (netLWF2) priorities2.pml:4 (state 7) [sub-sequence]
15: proc 2 (netLWF2) priorities2.pml:23 (state 8) [pc??n,1,0]
15: proc 2 (netLWF2) priorities2.pml:24 (state 9) [pc!n,1,1]
15: proc 2 (netLWF2) priorities2.pml:24 (state 10) [pc!_pid,1,1]
15: proc 2 (netLWF2) priorities2.pml:4 (state 12) [sub-sequence]
17: proc 1 (netLWF1) priorities2.pml:18 (state 3) [(((p1>0)&&!(pc??[_,2,0])))]
17: proc 1 (netLWF1) priorities2.pml:18 (state 2) [pc!_pid,2,0]
19: proc 2 (netLWF2) priorities2.pml:83 (state 75) [pc??eval(_pid),it,1]
20: proc 2 (netLWF2) priorities2.pml:4 (state 76) [set_priority(_pid, 3)]
22: proc 2 (netLWF2) priorities2.pml:89 (state 105) [((it==0))]
transition failed
23: proc 2 (netLWF2) priorities2.pml:4 (state 106) [set_priority(_pid, 1)]
25: proc 3 (netAC) priorities2.pml:105 (state 99) [pc??eval(_pid),it,1]
26: proc 3 (netAC) priorities2.pml:4 (state 100) [set_priority(_pid, 3)]
28: proc 3 (netAC) priorities2.pml:106 (state 108) [((it==1))]
28: proc 3 (netAC) priorities2.pml:106 (state 109) [p1 = (p1+1)]
30: proc 3 (netAC) priorities2.pml:4 (state 146) [set_priority(_pid, 1)]
32: proc 3 (netAC) priorities2.pml:16 (state 3) [(!(pc??[_,1,0]))]
32: proc 3 (netAC) priorities2.pml:16 (state 2) [pc!_pid,1,0]
34: proc 3 (netAC) priorities2.pml:20 (state 27) [((((p1>0)&&!(pc??[eval(_pid),2,0]))&&pc??[_,2,0]))]
34: proc 3 (netAC) priorities2.pml:4 (state 21) [sub-sequence]
34: proc 3 (netAC) priorities2.pml:23 (state 22) [pc??n,2,0]
34: proc 3 (netAC) priorities2.pml:24 (state 23) [pc!n,2,1]
34: proc 3 (netAC) priorities2.pml:24 (state 24) [pc!_pid,2,1]
34: proc 3 (netAC) priorities2.pml:4 (state 26) [sub-sequence]
36: proc 3 (netAC) priorities2.pml:105 (state 99) [pc??eval(_pid),it,1]
37: proc 3 (netAC) priorities2.pml:4 (state 100) [set_priority(_pid, 3)]
39: proc 3 (netAC) priorities2.pml:107 (state 111) [((it==2))]
39: proc 3 (netAC) priorities2.pml:107 (state 112) [p1 = (p1-1)]
41: proc 3 (netAC) priorities2.pml:4 (state 146) [set_priority(_pid, 1)]
43: proc 1 (netLWF1) priorities2.pml:55 (state 89) [pc??eval(_pid),it,1]
44: proc 1 (netLWF1) priorities2.pml:4 (state 90) [set_priority(_pid, 3)]
46: proc 1 (netLWF1) priorities2.pml:56 (state 98) [((it==2))]
46: proc 1 (netLWF1) priorities2.pml:56 (state 99) [p1 = (p1-1)]
46: proc 1 (netLWF1) priorities2.pml:56 (state 100) [p2 = (p2+1)]
48: proc 1 (netLWF1) priorities2.pml:4 (state 138) [set_priority(_pid, 1)]
50: proc 1 (netLWF1) priorities2.pml:18 (state 17) [(((p2>0)&&!(pc??[_,3,0])))]
50: proc 1 (netLWF1) priorities2.pml:18 (state 16) [pc!_pid,3,0]
52: proc 1 (netLWF1) priorities2.pml:51 (state 88) [((p2>0))]
52: proc 1 (netLWF1) priorities2.pml:4 (state 77) [sub-sequence]
52: proc 1 (netLWF1) priorities2.pml:52 (state 78) [p2 = (p2-1)]
52: proc 1 (netLWF1) priorities2.pml:40 (state 84) [sub-sequence]
52: proc 1 (netLWF1) priorities2.pml:38 (state 80) [pc??eval(_pid),3,0]
52: proc 1 (netLWF1) priorities2.pml:40 (state 83) [.(goto)]
52: proc 1 (netLWF1) priorities2.pml:53 (state 85) [p3 = (p3+1)]
52: proc 1 (netLWF1) priorities2.pml:4 (state 87) [sub-sequence]
54: proc 1 (netLWF1) priorities2.pml:18 (state 31) [(((p3>0)&&!(pc??[_,5,0])))]
54: proc 1 (netLWF1) priorities2.pml:18 (state 30) [pc!_pid,5,0]
56: proc 1 (netLWF1) priorities2.pml:18 (state 45) [(((p3>0)&&!(pc??[_,6,0])))]
56: proc 1 (netLWF1) priorities2.pml:18 (state 44) [pc!_pid,6,0]
<<<<<START OF CYCLE>>>>>
spin: trail ends after 58 steps
#processes: 4
p1 = 0
p3 = 0
p4 = 0
queue 1 (d): [1,255,0][2,255,0][3,255,0][3,4,0][3,7,0][3,1,0][1,5,0][1,6,0]
58: proc 3 (netAC) priorities2.pml:96 (state 148)
58: proc 2 (netLWF2) priorities2.pml:92 (state 117) <valid end state>
58: proc 1 (netLWF1) priorities2.pml:45 (state 93)
58: proc 0 (:init:) priorities2.pml:125 (state 56) <valid end state>
58: proc - (s) _spin_nvr.tmp:3 (state 3)
4 processes created

mlfv · 2013-05-12 02:40:28

In this trace

- step 15, process 2 must have priority 3, why is process 1 executed at step 17?
- step 22, why "transition failed"?

spinroot · 2013-05-12 05:23:44

thank you again -- this pinpointed yet another problem
it will be fixed in 6.2.6
thanks very much for your very good observations

spinroot · 2013-05-12 18:00:03

for completeness: with the fixed version of spin, the verification becomes far more time consuming,
but a bitstate search with -w36 finds a counter-example in about 96 seconds:

$ ./pan -a -m10000000 -w36
Depth= 16578 States= 1e+06 Transitions= 2.39e+06 Memory= 8956.600 t= 4.19 R= 2e+05
Depth= 16578 States= 2e+06 Transitions= 4.95e+06 Memory= 8956.600 t= 8.55 R= 2e+05
Depth= 16578 States= 3e+06 Transitions= 7.69e+06 Memory= 8956.600 t= 13.5 R= 2e+05
Depth= 16578 States= 4e+06 Transitions= 1.06e+07 Memory= 8956.600 t= 18.7 R= 2e+05
Depth= 16578 States= 5e+06 Transitions= 1.33e+07 Memory= 8956.600 t= 23.5 R= 2e+05
Depth= 16578 States= 6e+06 Transitions= 1.62e+07 Memory= 8956.600 t= 28.7 R= 2e+05
Depth= 16578 States= 7e+06 Transitions= 1.95e+07 Memory= 8956.600 t= 34.5 R= 2e+05
Depth= 16578 States= 8e+06 Transitions= 2.28e+07 Memory= 8956.600 t= 40.6 R= 2e+05
Depth= 16578 States= 9e+06 Transitions= 2.65e+07 Memory= 8956.600 t= 47.4 R= 2e+05
Depth= 16578 States= 1e+07 Transitions= 3.07e+07 Memory= 8956.600 t= 55.7 R= 2e+05
Depth= 16578 States= 1.1e+07 Transitions= 3.43e+07 Memory= 8956.600 t= 62.4 R= 2e+05
Depth= 16578 States= 1.2e+07 Transitions= 3.7e+07 Memory= 8956.600 t= 67.1 R= 2e+05
Depth= 16578 States= 1.3e+07 Transitions= 3.97e+07 Memory= 8956.600 t= 71.8 R= 2e+05
Depth= 16578 States= 1.4e+07 Transitions= 4.25e+07 Memory= 8956.600 t= 76.6 R= 2e+05
Depth= 16578 States= 1.5e+07 Transitions= 4.53e+07 Memory= 8956.600 t= 81.4 R= 2e+05
Depth= 16578 States= 1.6e+07 Transitions= 4.8e+07 Memory= 8956.600 t= 86.2 R= 2e+05
Depth= 16578 States= 1.7e+07 Transitions= 5.08e+07 Memory= 8956.600 t= 91 R= 2e+05
Depth= 16578 States= 1.8e+07 Transitions= 5.34e+07 Memory= 8956.600 t= 95.6 R= 2e+05
pan:1: acceptance cycle (at depth 16512)
pan: wrote priorities2.pml.trail

(Spin Version 6.2.6 -- 11 May 2013)
Warning: Search not completed

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

State-vector 140 byte, depth reached 16580, errors: 1
9122929 states, stored (1.82389e+07 visited)
35595300 states, matched
53834197 transitions (= visited+matched)
1.1038119e+08 atomic steps

hash factor: 3767.74 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
1392.048 equivalent memory usage for states (stored*(State-vector + overhead))
8192.000 memory used for hash array (-w36)
76.294 memory used for bit stack
686.646 memory used for DFS stack (-m10000000)
1.625 other (proc and chan stacks)
8956.600 total actual memory usage

pan: elapsed time 96.6 seconds
pan: rate 188867.11 states/second

mlfv · 2013-05-13 13:26:50

Disabling priorities as in line 5 and using version 6.2.5 with bitstate hashing, the model is verified. I was wondering why the state space is so large for this model, even with partial order reduction. Using priorities I was looking forward some reduction and a faster proof; I wouldn't expect the state space to grow even further.

spin -a priorities2.pml
ltl s: <> ((p4>0))
gcc -DMEMLIM=1024 -O2 -DBITSTATE -DXUSAFE -DNOREDUCE -w -o pan pan.c
./pan -m10000 -k3 -a -w20
Pid: 6680

(Spin Version 6.2.5 -- 3 May 2013)

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

State-vector 120 byte, depth reached 5836, errors: 0
24486 states, stored (541706 visited)
1125411 states, matched
1667117 transitions (= visited+matched)
3055078 atomic steps

hash factor: 1.93569 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
3.082 equivalent memory usage for states (stored*(State-vector + overhead))
0.125 memory used for hash array (-w20)
0.038 memory used for bit stack
0.382 memory used for DFS stack (-m10000)
1.190 total actual memory usage

unreached in proctype netLWF1
(0 of 143 states)
unreached in proctype netLWF2
(0 of 117 states)
unreached in proctype netAC
priorities2.pml:111, state 151, "-end-"
(1 of 151 states)
unreached in init
(0 of 59 states)
unreached in claim s
_spin_nvr.tmp:6, state 6, "-end-"
(1 of 6 states)

pan: elapsed time 3.16 seconds
No errors found -- did you verify all claims?

spinroot · 2013-05-13 15:55:36

Note that the search you performed was a Bitstate search with hash-factor 1.9.
The one I did had a hash-factor of 3767.74, which is a much better guarantee of full coverage.
If I repeat the new run at -w20 then it completes in 2.27 seconds and also doesn't find the counterexample
(hash factor 2.12):

$ ./pan -a -m20000 -w20 -k3
error: max search depth too small

(Spin Version 6.2.6 -- 11 May 2013)

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

State-vector 140 byte, depth reached 19999, errors: 0
40939 states, stored (494021 visited)
544227 states, matched
1038248 transitions (= visited+matched)
2650191 atomic steps

hash factor: 2.12253 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
6.247 equivalent memory usage for states (stored*(State-vector + overhead))
0.125 memory used for hash array (-w20)
0.153 memory used for bit stack
1.373 memory used for DFS stack (-m20000)
1.820 other (proc and chan stacks)
3.507 total actual memory usage

unreached in proctype netLWF1
(0 of 143 states)
unreached in proctype netLWF2
(0 of 117 states)
unreached in proctype netAC
priorities2.pml:116, state 151, "-end-"
(1 of 151 states)
unreached in init
(0 of 59 states)
unreached in claim s
_spin_nvr.tmp:6, state 6, "-end-"
(1 of 6 states)

pan: elapsed time 2.27 seconds
pan: rate 217630.4 states/second

spinroot · 2013-05-13 15:56:49

or, without cutting off the depth:

$ ./pan -a -m100000 -w20 -k3

(Spin Version 6.2.6 -- 11 May 2013)

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

State-vector 140 byte, depth reached 95910, errors: 0
40845 states, stored (539597 visited)
609666 states, matched
1149263 transitions (= visited+matched)
2756965 atomic steps

hash factor: 1.94326 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
6.232 equivalent memory usage for states (stored*(State-vector + overhead))
0.125 memory used for hash array (-w20)
0.763 memory used for bit stack
6.867 memory used for DFS stack (-m100000)
8.066 other (proc and chan stacks)
15.860 total actual memory usage

unreached in proctype netLWF1
(0 of 143 states)
unreached in proctype netLWF2
(0 of 117 states)
unreached in proctype netAC
priorities2.pml:116, state 151, "-end-"
(1 of 151 states)
unreached in init
(0 of 59 states)
unreached in claim s
_spin_nvr.tmp:6, state 6, "-end-"
(1 of 6 states)

pan: elapsed time 2.45 seconds
pan: rate 220243.67 states/second

mlfv · 2013-05-13 18:49:22

Is the new release available?

mlfv · 2013-05-13 21:13:23

SPIN was right! I performed the verification on an improved model (but without priorities), with version 6.2.5, pan -a -m10000000 -w28, and found a very subtle error in 11.2s! Thanks a lot for pointing it. Looking forward the new release.

Spinroot

#1 2013-04-29 22:42:20

verifying models with priorities

#2 2013-04-30 04:31:10

Re: verifying models with priorities

#3 2013-04-30 13:32:20

Re: verifying models with priorities

#4 2013-04-30 16:18:53

Re: verifying models with priorities

#5 2013-05-02 13:18:40

Re: verifying models with priorities

#6 2013-05-02 15:10:39

Re: verifying models with priorities

#7 2013-05-03 05:32:30

Re: verifying models with priorities

#8 2013-05-03 18:30:29

Re: verifying models with priorities

#9 2013-05-05 00:44:29

Re: verifying models with priorities

#10 2013-05-05 03:08:55

Re: verifying models with priorities

#11 2013-05-05 21:10:30

Re: verifying models with priorities

#12 2013-05-05 23:59:03

Re: verifying models with priorities

#13 2013-05-07 00:31:37

Re: verifying models with priorities

#14 2013-05-11 19:47:55

Re: verifying models with priorities

#15 2013-05-12 02:40:28

Re: verifying models with priorities

#16 2013-05-12 05:23:44

Re: verifying models with priorities

#17 2013-05-12 18:00:03

Re: verifying models with priorities

#18 2013-05-13 13:26:50

Re: verifying models with priorities

#19 2013-05-13 15:55:36

Re: verifying models with priorities

#20 2013-05-13 15:56:49

Re: verifying models with priorities

#21 2013-05-13 18:49:22

Re: verifying models with priorities

#22 2013-05-13 21:13:23

Re: verifying models with priorities

Board footer