A forum for Spin users
You are not logged in.
Very nice explanation! Thanks.
So, if e.g. a process has a single statement if or do with all the options enclosed in d_steps then no unreachable code will be reported for that process. In order to detect an unreachable option it should be enclosed in atomic and e.g. the unguarded part in d_step.
Yes, see https://www.dropbox.com/s/h94s2r208vucbz0/forecastingExDstepsImp.pml?dl=0
It has two invalid assertions at lines 357 and 365. The safety verification reports no error but doesn't report the unreachable states.
I have a model with some unreachable code which is not reported by the exhaustive search. Does spin find all unreachable states in a model or it may miss some of them?
Thanks for the quick response!
This fix allows the use of poll operations in rhs, isn't it?
No, it's just a guarded assignment as line 9.
Hi,
According to the online Promela Manual and Grammar, the channel poll operations "can be used freely in expressions or even assignments". As the model below shows, these operations can indeed be used in expressions but a compilation error is produced if they are used in assignments. In addition, it seems that in the former case, the semantics of the operation ??[] in a random simulation is not same as in verification. In a random simulation with ispin, the execution is blocked at line 10; but in a safety verification no error is reported.
1 chan d = [5] of {byte, byte}
2
3 init{
4 d !! 1,1
5 d !! 4,0
6 d !! 2,1
7 d ! 3,2
8 int a, b = 1, c = 2
9 (d?? [ _,0]) +1 > 1 && b -> b = a
10 (d?? [ _,0]) +1 > 2 && c -> c = a
11
12 /* a = d?? [ _,0]+1 /* This is an error */
13 }
I noticed this because I am trying to reduce the state space of certain models and the use of embedded C-code is not helping (besides the random simulations are not allowed). After several tests, I realized that in my case, the best solution would be if the operator ??[]
1) returns the number of messages in the channel matching the pattern and
2) can be used in assignments.
I looked into the pan files and the semantics of ??[] in verification (Q_has function) returns zero or the position of the first message (true and false in simulations). Therefore, I believe that few changes are required in order to allows 1) without changing the underlying goal, i.e. testing the executability of the receive statement. I think that 2) may be harder to deal with; but since now the error that it produces is not a syntax error, the compiler would not require a major modification but a local one. Is it possible to consider the inclusion of these features into the language? I believe it would be very helpful to other SPIN users too.
A second issue is the combination of hidden variables and d_steps inside atomic regions. I used them in a model (see https://www.dropbox.com/s/l9w4k1cqhsacovj/prosecutionExImpDsteps.pml?dl=0), but when trying to verify the property I got an unexpected error. When replaying the error trail several warnings are shown ("d_step inside atomic") and also a "transition failed" message at step 145. It looks like the value of the variable (lt) from the previous step was mysteriously changed. Nevertheless, if e.g. the variable is not hidden or the d_steps inside atomic are removed or the assignment lt=0 is added after line 133, then the property is verified.
Thanks :-)
Hi,
the next model simulates a simple Petri net with a deadlock. The safety verification does not report the invalid state but the
deadlock can be found by adding an invalid assertion or using an ltl formula. Why the default search can't find the invalid state?
1 byte transitionNumber;
2
3 byte p1=1, p2, p3=1; bit p4=1,p5,p6,p7,f;
4
5 ltl p { !( (<>[] (f==0)) || (<>[] (f==1)) ) }
6
7 init{
8 do :: atomic{ p4>0 && p1 >0 -> /* t1 */
9 f = !f; transitionNumber = 1;
10 p4--; p1--; p5++; p2++ }
11 :: atomic{ p6>0 && p2 >0-> /* t2 */
12 f = !f; transitionNumber = 2;
13 p6--; p2--; p7++; p1++; }
14 :: atomic{ p5>0 && p3 >0 -> /* t3 */
15 f = !f; transitionNumber = 3;
16 p5--; p3--; p1++; }
17 :: atomic{ p1 >0 -> /* t4 */
18 f = !f; transitionNumber = 4;
19 p1--; p6++; p3++; }
20 :: atomic{ p7>0 && p3 >0 -> /* t5 */
21 f = !f; transitionNumber = 5;
22 p7--; p3--; p2++ }
23 :: atomic{ p2 >0 -> /* t6 */
24 f = !f; transitionNumber = 6;
25 p4++; p2--; p3++; }
26 /* :: else -> assert(0) */
27 od
28 }
Thanks for the quick response!
Is there a way to produce an error trail in case an integer overflow happens during verifications, without adding an assertion for each variable?
I think there is small bug when showing the process priorities in an error trail. For instance, priorities are properly attached to processes in a random simulation trail for the above model. But, if we add ltl p {[]( len(c)<5 )}, then some priorities in the error trail (below) are wrong; e.g. the priority of A (_pid=1) is set to 4 in step 8, but in steps 10-13 the process appears with priority 1. Besides, in lines 22-27, A appears with priority 3 (the last priority of B - never shown) instead of 1. The never claim p got priority 2 instead of init; perhaps this is the source of the bug.
ltl p: [] ((len(c)<5))
starting claim 3
using statement merging
MSC: ~G line 4
1: proc - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
Never claim moves to line 4 [(1)]
2: setting priority of proc 0 to 2
2: proc 0 (:init::1) channelsT.pml:18 (state 1) [set_priority(0, 2)]
3: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
Starting A with pid 2 priority 1
4: proc 0 (:init::1) channelsT.pml:18 (state 2) [(run A())]
5: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
Starting B with pid 3 priority 2
6: proc 0 (:init::1) channelsT.pml:18 (state 3) [(run B())]
7: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
8: proc 2 (B:2) channelsT.pml:12 (state -) [values: 1!1]
8: proc 2 (B:2) channelsT.pml:12 (state 4) [c!1]
queue 1 (c): [1]
8: setting priority of proc 1 to 4
8: proc 2 (B:2) channelsT.pml:12 (state 2) [set_priority(1, 4)]
queue 1 (c): [1]
8: proc 2 (B:2) channelsT.pml:12 (state -) [values: 1!2]
8: proc 2 (B:2) channelsT.pml:12 (state 3) [c!2]
queue 1 (c): [1][2]
9: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
10: proc 1 (A:1) channelsT.pml:5 (state 1) [((i<4))]
11: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
12: proc 1 (A:1) channelsT.pml:5 (state -) [values: 1!3]
12: proc 1 (A:1) channelsT.pml:5 (state 2) [c!3]
queue 1 (c): [1][2][3]
13: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
14: setting priority of proc 1 to 1
14: proc 1 (A:1) channelsT.pml:6 (state 3) [set_priority(_pid, 1)]
15: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
16: setting priority of proc 2 to 3
16: proc 2 (B:2) channelsT.pml:13 (state 5) [set_priority(_pid, 3)]
17: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
18: proc 2 (B:2) channelsT.pml:14 (state -) [values: 1!4]
18: proc 2 (B:2) channelsT.pml:14 (state 6) [c!4]
queue 1 (c): [1][2][3][4]
19: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
20: proc 2 terminates
21: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
22: proc 1 (A:3) channelsT.pml:7 (state 4) [i = (i+1)]
A(1):i = 1
23: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
24: proc 1 (A:3) channelsT.pml:5 (state 1) [((i<4))]
25: proc - (p:2) _spin_nvr.tmp:4 (state 4) [(1)]
26: proc 1 (A:3) channelsT.pml:5 (state -) [values: 1!3]
26: proc 1 (A:3) channelsT.pml:5 (state 2) [c!3]
queue 1 (c): [1][2][3][4][3]
MSC: ~G line 3
27: proc - (p:2) _spin_nvr.tmp:3 (state 1) [(!((len(c)<5)))] <merge 0 now @2>
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!((len(c)<5))))
#processes: 2
queue 1 (c): [1][2][3][4][3]
27: proc 1 (A:3) channelsT.pml:6 (state 3)
27: proc 0 (:init::1) channelsT.pml:18 (state 4)
27: proc - (p:2) _spin_nvr.tmp:3 (state 2)
3 processes created
Exit-Status 0
It would very helpful to use both versions (perhaps the constant version with another name)
select statements with non-constant expressions now produce a syntax error
Error: expecting select ( name : constant .. constant ) near 'select'
I am using Windows 7 64-bits and spin 64 bits.
Hi,
I reinstalled spin and cygwin (cygwin64) but when I try to verify any model I get the next error
verification result:
spin -a a1.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
Pid: 2080
spin: error, the version of spin that generated this pan.c assumed a different wordsize (4 iso 8)
Any idea about how to fix this error? Thanks in advance for any help.
A random simulation using ispin (seed 123) for the next model
1 chan c = [10] of { byte };
2
3 proctype A()
4 { int i;
5 do :: i < 4 -> c ! 3;
6 set_priority(_pid, 1);
7 i++;
8 od
9 }
10
11 proctype B() {
12 d_step { c ! 1; set_priority(1, 4); c ! 2; }
13 set_priority(_pid, 3);
14 c ! 4
15 }
16
17 init { set_priority(0, 2); run A(); run B() priority 2;}
produces the error
spin: priorities3.pml:15, Error: cannot happen - weights
Furthermore, removing line 13 produces a more strange error
spin: allocated 1 Gb, wanted 44 bytes more
spin: priorities3.pml:16, Error: not enough memory
Another case that now produces a syntax error is the unless e.g.
if ... fi
unless ...
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.
Is the new release available?
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?
In this trace
- step 15, process 2 must have priority 3, why is process 1 executed at step 17?
- step 22, why "transition failed"?
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
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?