Spinroot

A forum for Spin users

You are not logged in.

#2 Re: General » unreachable code missed by the safety verification » 2016-09-26 21:54:31

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.

#3 Re: General » unreachable code missed by the safety verification » 2016-09-26 01:01:45

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.

#4 General » unreachable code missed by the safety verification » 2016-09-24 15:06:02

mlfv
Replies: 6

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?

#6 Re: General » poll operations in assignments; hidden variable + d_step inside atomic » 2016-09-08 17:28:08

This fix allows the use of poll operations in rhs, isn't it?

#8 General » poll operations in assignments; hidden variable + d_step inside atomic » 2016-09-07 15:27:18

mlfv
Replies: 6

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.

#10 Re: General » Checking for invalid end states in full statespace search » 2015-10-05 15:26:26

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    }

#12 General » Integer overflow in verifications » 2015-07-20 14:01:51

mlfv
Replies: 1

Is there a way to produce an error trail in case an integer overflow happens during verifications, without adding an assertion for each variable?

#13 Re: Bug Reports » ispin random simulations with priorities » 2015-07-20 13:53:17

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

#14 Re: Announcements » Spin Version 6.4.3 now available » 2015-01-19 19:20:07

It would very helpful to use both versions (perhaps the constant version with another name)

#15 Re: Announcements » Spin Version 6.4.3 now available » 2015-01-19 18:42:12

select statements with non-constant expressions now produce a syntax error

Error: expecting select ( name : constant .. constant ) near 'select'

#16 Re: General » pan error concerning wordsize » 2014-12-13 15:02:50

I am using Windows 7 64-bits and spin 64 bits.

#17 General » pan error concerning wordsize » 2014-12-12 15:17:22

mlfv
Replies: 2

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.

#18 Bug Reports » ispin random simulations with priorities » 2014-05-08 20:28:08

mlfv
Replies: 5

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

#19 Re: Announcements » Spin Version 6.3.0 now available » 2014-05-08 20:07:51

Another case that now produces a syntax error is the unless e.g.
if  ...  fi
  unless ...

#20 Re: General » verifying models with priorities » 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.

#22 Re: General » verifying models with priorities » 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?

#23 Re: General » verifying models with priorities » 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"?

#24 Re: General » verifying models with priorities » 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

#25 Re: General » verifying models with priorities » 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?

Board footer

Powered by FluxBB