Spinroot

mlfv

Member

Registered: 2013-04-29

Posts: 28

ispin random simulations with priorities

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

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: ispin random simulations with priorities

This happens only in simulations, right? Not in verifications.
The first error is a bug in the simulation code -- will be fixed in 6.3.1.
Likely the second error was a side-effect of this.
After I fixed the first problem, the second no longer happens.

mlfv

Member

Registered: 2013-04-29

Posts: 28

Re: ispin random simulations with priorities

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

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: ispin random simulations with priorities

i'll look into it
thanks for the bug report!

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: ispin random simulations with priorities

Indeed a bug
Here is the same output for the fixed version of Spin, which will be version 6.4.4:

ltl p: [] ((len(c)<5))
starting claim 3
using statement merging
  1:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
Never claim moves to line 4     [(1)]
  2: setting priority of proc 0 (:init:) to 2
        Pid     Name    Priority
        1       :init:  2
        0       p       1
  2:    proc  0 (:init::2) priorities.pml:25 (state 1)  [set_priority(0, 2)]
  3:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
Starting A with pid 2 priority 1
  4:    proc  0 (:init::2) priorities.pml:26 (state 2)  [(run A())]
  5:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
Starting B with pid 3 priority 2
  6:    proc  0 (:init::2) priorities.pml:27 (state 3)  [(run B())]
  7:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
  8:    proc  2 (B:2) priorities.pml:15 (state 4)       [c!1]
                queue 1 (c): [1]
  8: setting priority of proc 1 (A) to 4
        Pid     Name    Priority
        3       B       2
        2       A       4
        1       :init:  2
        0       p       1
  8:    proc  2 (B:2) priorities.pml:17 (state 2)       [set_priority(1, 4)]
                queue 1 (c): [1]
  8:    proc  2 (B:2) priorities.pml:18 (state 3)       [c!2]
                queue 1 (c): [1][2]
  9:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2]
10:    proc  1 (A:4) priorities.pml:6 (state 1)        [((i<4))]
                queue 1 (c): [1][2]
11:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2]
12:    proc  1 (A:4) priorities.pml:7 (state 2)        [c!3]
                queue 1 (c): [1][2][3]
13:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2][3]
14: setting priority of proc 1 (A) to 1
        Pid     Name    Priority
        3       B       2
        2       A       1
        1       :init:  2
        0       p       1
14:    proc  1 (A:1) priorities.pml:8 (state 3)        [set_priority(_pid, 1)]
                queue 1 (c): [1][2][3]
15:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2][3]
16: setting priority of proc 2 (B) to 3
        Pid     Name    Priority
        3       B       3
        2       A       1
        1       :init:  2
        0       p       1
16:    proc  2 (B:3) priorities.pml:20 (state 5)       [set_priority(_pid, 3)]
                queue 1 (c): [1][2][3]
17:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2][3]
18:    proc  2 (B:3) priorities.pml:21 (state 6)       [c!4]
                queue 1 (c): [1][2][3][4]
19:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2][3][4]
20: proc 2 terminates
21:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2][3][4]
22:    proc  1 (A:1) priorities.pml:9 (state 4)        [i = (i+1)]
                queue 1 (c): [1][2][3][4]
                A(1):i = 1
23:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2][3][4]
24:    proc  1 (A:1) priorities.pml:6 (state 1)        [((i<4))]
                queue 1 (c): [1][2][3][4]
25:    proc  - (p:1) _spin_nvr.tmp:4 (state 4) [(1)]
                queue 1 (c): [1][2][3][4]
26:    proc  1 (A:1) priorities.pml:7 (state 2)        [c!3]
                queue 1 (c): [1][2][3][4][3]
27:    proc  - (p:1) _spin_nvr.tmp:3 (state 1) [(!((len(c)<5)))]       <merge 0 now @2>
                queue 1 (c): [1][2][3][4][3]
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!((len(c)<5))))
27:    proc  - (p:1) _spin_nvr.tmp:3 (state 2) [assert(!(!((len(c)<5))))]
                queue 1 (c): [1][2][3][4][3]
Never claim moves to line 3     [assert(!(!((len(c)<5))))]
spin: trail ends after 27 steps
#processes: 2
                queue 1 (c): [1][2][3][4][3]
27:    proc  1 (A:1) priorities.pml:8 (state 3)
27:    proc  0 (:init::2) priorities.pml:28 (state 4) <valid end state>
27:    proc  - (p:1) _spin_nvr.tmp:2 (state 6)
3 processes created

If you want to make the fix in your current version of Spin:
- edit the file run.c and look for the last function definition, which is set_priority
   change the initial assignment
     int i = nproc - nstop;
   to
     int i = nproc - nstop - Have_claim;
   and add an external declaration for Have_claim somewhere at the top of the file:
     extern short Have_claim;
- recompile and reinstall

mlfv

Member

Registered: 2013-04-29

Posts: 28

Re: ispin random simulations with priorities

Thanks for the quick response!