Spinroot

A forum for Spin users

You are not logged in.

#1 2017-06-24 09:36:16

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

What kind of states & transitions does Spin's “depth reached” consider

Since there seem to be more questions related to Promela and Spin on stackoverflow, I have posted my question there: https://stackoverflow.com/q/44684675/750378.

However, since there are only 5 views, I am posting this link here in the hope that it will be answered.


Best
David

------------

In case the link above no longer works, here is the contents:

For verifications (with ispin) that use never claims, I get outputs with `depth reached` larger than the number of states and the number of transitions, e.g.:

    Full statespace search for:
        never claim             + (REQ5)
        assertion violations    + (if within scope of claim)
        cycle checks           - (disabled by -DSAFETY)
        invalid end states    - (disabled by never claim)
   
    State-vector 60 byte, depth reached 87, errors: 1
           41 states, stored
           10 states, matched
           51 transitions (= stored+matched)
            9 atomic steps
    hash conflicts:         0 (resolved)

I find that a bit unintuitive. Is there a precise description of the semantics of "depth reached" somewhere (more thorough than [pan's output format description](http://spinroot.com/spin/Man/Pan.html#C))? Maybe the meaning of

> longest depth-first search path contained 87 transitions

does not refer to the 51 transitions, but to the transitions of the system automata composed with the never claim?

Offline

#2 2017-07-11 17:38:55

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

Re: What kind of states & transitions does Spin's “depth reached” consider

That's a good question. Can you post the example that generated these numbers, so that I can find out in more detail what causes the depth to be that large?

Offline

#3 2017-07-14 10:45:39

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: What kind of states & transitions does Spin's “depth reached” consider

Thanks for your reply. Here is a <strike>minimal</strike>small example:

#define k 3
#define succ(index) ((index+1) % k)
#define pre(index) ((index+(k-1)) % k)

mtype  = { C, B, F, E };
mtype arr[k];
bool u;

ltl REQ5 {[]( (arr[1]==B) -> (arr[2] != F) )}

proctype sp (byte index)
{
  do   
  ::  atomic{ (arr[index] == C && arr[pre(index)] == F)
        -> assert(u == false); arr[index] = B; u = true }
  ::  atomic{ (arr[index] == B && arr[succ(index)] != F)
        -> arr[index] = F; u = false }
  ::  atomic{ (arr[index] == F && arr[pre(index)]!=F && u)
        -> arr[index] = E }
  ::  atomic{ (arr[index] == E && arr[pre(index)]!=E)
        -> arr[index] = C }
  od
}

init {
atomic {
        byte index = 0;   
        do
        :: index < k ->
            arr[index] = E;
            run sp (index);
            index++
        :: index >= k ->    break
        od;
        arr[0] = B; u = true;
       }
}

Checking REQ5 leads to the following output:

Warning: Search not completed
    + Partial Order Reduction

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

State-vector 52 byte, depth reached 39, errors: 1
       16 states, stored
        2 states, matched
       18 transitions (= stored+matched)
        9 atomic steps
hash conflicts:         0 (resolved)

Offline

#4 2017-07-15 17:18:02

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

Re: What kind of states & transitions does Spin's “depth reached” consider

From this more verbose trace you can see how the search depth changes.
I got the following trail by compiling cc -DVERBOSE -o pan pan.c and after I replaced
the property with a claim that said that the search depth could not increase beyond 58
(thus getting a counter-example for the case where it does get to 59 steps).
From this trace I removed the unsuccessful moves that were backtracked, to make the
search sequence more clear:
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
0: Down - claim non-accepting [pids 1-1]
    New state 0
  0: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
1: Down - program non-accepting [pids 1-1]
  1: proc 1 exec 5, 13 to 8, index = 0 atomic  non-accepting [tau=0]
2: Down - program non-accepting [pids 1-1]
  2: proc 1 exec 6, 8 to 4, ((index<3)) atomic  non-accepting [tau=8]
3: Down - program non-accepting [pids 1-1]
  3: proc 1 exec 7, 4 to 5, (run sp(index)) atomic  non-accepting [tau=8]
4: Down - program non-accepting [pids 1-1]
  4: proc 1 exec 8, 5 to 8, index = (index+1) atomic  non-accepting [tau=8]
5: Down - program non-accepting [pids 1-1]
  5: proc 1 exec 6, 8 to 4, ((index<3)) atomic  non-accepting [tau=8]
6: Down - program non-accepting [pids 1-1]
  6: proc 1 exec 7, 4 to 5, (run sp(index)) atomic  non-accepting [tau=8]
7: Down - program non-accepting [pids 1-1]
  7: proc 1 exec 8, 5 to 8, index = (index+1) atomic  non-accepting [tau=8]
8: Down - program non-accepting [pids 1-1]
  8: proc 1 exec 6, 8 to 4, ((index<3)) atomic  non-accepting [tau=8]
9: Down - program non-accepting [pids 1-1]
  9: proc 1 exec 7, 4 to 5, (run sp(index)) atomic  non-accepting [tau=8]
10: Down - program non-accepting [pids 1-1]
10: proc 1 exec 8, 5 to 8, index = (index+1) atomic  non-accepting [tau=8]
11: Down - program non-accepting [pids 1-1]
11: proc 1 exec 9, 8 to 14, ((index>=3))   non-accepting [tau=8]
12: Down - claim non-accepting [pids 4-1]
    New state 1
12: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
13: Down - program non-accepting [pids 4-1]
13: proc 3 exec 15, 16 to 16, (((arr[index]==E)&&(arr[((index+(3-1))%3)]!=E)))   non-accepting [tau=0]
14: Down - claim non-accepting [pids 4-1]
    New state 2
14: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
15: Down - program non-accepting [pids 4-1]
15: proc 4 exec 15, 16 to 16, (((arr[index]==E)&&(arr[((index+(3-1))%3)]!=E)))   non-accepting [tau=0]
16: Down - claim non-accepting [pids 4-1]
    New state 3
16: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
17: Down - program non-accepting [pids 4-1]
17: proc 2 exec 13, 16 to 16, (((arr[index]==B)&&(arr[((index+1)%3)]!=F)))   non-accepting [tau=0]
18: Down - claim non-accepting [pids 4-1]
    New state 4
18: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
19: Down - program non-accepting [pids 4-1]
19: proc 3 exec 12, 16 to 16, (((arr[index]==C)&&(arr[((index+(3-1))%3)]==F)))   non-accepting [tau=0]
20: Down - claim non-accepting [pids 4-1]
    New state 5
20: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
21: Down - program non-accepting [pids 4-1]
21: proc 3 exec 13, 16 to 16, (((arr[index]==B)&&(arr[((index+1)%3)]!=F)))   non-accepting [tau=0]
22: Down - claim non-accepting [pids 4-1]
    New state 6
22: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
23: Down - program non-accepting [pids 4-1]
23: proc 4 exec 12, 16 to 16, (((arr[index]==C)&&(arr[((index+(3-1))%3)]==F)))   non-accepting [tau=0]
24: Down - claim non-accepting [pids 4-1]
    New state 7
24: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
25: Down - program non-accepting [pids 4-1]
25: proc 2 exec 14, 16 to 16, ((((arr[index]==F)&&(arr[((index+(3-1))%3)]!=F))&&u))   non-accepting [tau=0]
26: Down - claim non-accepting [pids 4-1]
    New state 8
26: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
27: Down - program non-accepting [pids 4-1]
27: proc 4 exec 13, 16 to 16, (((arr[index]==B)&&(arr[((index+1)%3)]!=F)))   non-accepting [tau=0]
28: Down - claim non-accepting [pids 4-1]
    New state 9
28: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
29: Down - program non-accepting [pids 4-1]
29: proc 2 exec 15, 16 to 16, (((arr[index]==E)&&(arr[((index+(3-1))%3)]!=E)))   non-accepting [tau=0]
30: Down - claim non-accepting [pids 4-1]
    New state 10
30: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
31: Down - program non-accepting [pids 4-1]
31: proc 2 exec 12, 16 to 16, (((arr[index]==C)&&(arr[((index+(3-1))%3)]==F)))   non-accepting [tau=0]
32: Down - claim non-accepting [pids 4-1]
    New state 11
32: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
33: Down - program non-accepting [pids 4-1]
33: proc 3 exec 14, 16 to 16, ((((arr[index]==F)&&(arr[((index+(3-1))%3)]!=F))&&u))   non-accepting [tau=0]
34: Down - claim non-accepting [pids 4-1]
    New state 12
34: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
35: Down - program non-accepting [pids 4-1]
35: proc 3 exec 15, 16 to 16, (((arr[index]==E)&&(arr[((index+(3-1))%3)]!=E)))   non-accepting [tau=16]
36: Down - claim non-accepting [pids 4-1]
    New state 13
36: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
37: Down - program non-accepting [pids 4-1]
37: proc 2 exec 13, 16 to 16, (((arr[index]==B)&&(arr[((index+1)%3)]!=F)))   non-accepting [tau=16]
38: Down - claim non-accepting [pids 4-1]
    New state 14
38: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
39: Down - program non-accepting [pids 4-1]
39: proc 3 exec 12, 16 to 16, (((arr[index]==C)&&(arr[((index+(3-1))%3)]==F)))   non-accepting [tau=0]
40: Down - claim non-accepting [pids 4-1]
    New state 15
40: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
41: Down - program non-accepting [pids 4-1]
41: proc 4 exec 14, 16 to 16, ((((arr[index]==F)&&(arr[((index+(3-1))%3)]!=F))&&u))   non-accepting [tau=0]
42: Down - claim non-accepting [pids 4-1]
    New state 16
42: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
43: Down - program non-accepting [pids 4-1]
43: proc 2 exec 14, 16 to 16, ((((arr[index]==F)&&(arr[((index+(3-1))%3)]!=F))&&u))   non-accepting [tau=16]
44: Down - claim non-accepting [pids 4-1]
    New state 18
44: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
45: Down - program non-accepting [pids 4-1]
45: proc 4 exec 15, 16 to 16, (((arr[index]==E)&&(arr[((index+(3-1))%3)]!=E)))   non-accepting [tau=0]
46: Down - claim non-accepting [pids 4-1]
    New state 19
46: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
47: Down - program non-accepting [pids 4-1]
47: proc 3 exec 13, 16 to 16, (((arr[index]==B)&&(arr[((index+1)%3)]!=F)))   non-accepting [tau=0]
48: Down - claim non-accepting [pids 4-1]
    New state 20
48: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
49: Down - program non-accepting [pids 4-1]
49: proc 2 exec 15, 16 to 16, (((arr[index]==E)&&(arr[((index+(3-1))%3)]!=E)))   non-accepting [tau=16]
50: Down - claim non-accepting [pids 4-1]
    New state 21
50: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
51: Down - program non-accepting [pids 4-1]
51: proc 4 exec 12, 16 to 16, (((arr[index]==C)&&(arr[((index+(3-1))%3)]==F)))   non-accepting [tau=0]
52: Down - claim non-accepting [pids 4-1]
    New state 22
52: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
53: Down - program non-accepting [pids 4-1]
53: proc 3 exec 14, 16 to 16, ((((arr[index]==F)&&(arr[((index+(3-1))%3)]!=F))&&u))   non-accepting [tau=16]
54: Down - claim non-accepting [pids 4-1]
    New state 23
54: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
55: Down - program non-accepting [pids 4-1]
55: proc 4 exec 13, 16 to 16, (((arr[index]==B)&&(arr[((index+1)%3)]!=F)))   non-accepting [tau=0]
56: Down - claim non-accepting [pids 4-1]
    New state 24
56: proc 0 exec 2, 5 to 5, else   non-accepting [tau=4]
57: Down - program non-accepting [pids 4-1]
57: proc 3 exec 15, 16 to 16, (((arr[index]==E)&&(arr[((index+(3-1))%3)]!=E)))   non-accepting [tau=0]
58: Down - claim non-accepting [pids 4-1]
    New state 25
pan:1: assertion violated 0 (at depth 58)
pan: wrote req5.pml.trail

(Spin Version 6.4.7 -- 19 March 2017)
Warning: Search not completed
    + Partial Order Reduction
    + FullStack Matching

Full statespace search for:
    never claim             + (REQ5)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     - (not selected)
    invalid end states    - (disabled by never claim)

State-vector 52 byte, depth reached 58, errors: 1
       26 states, stored
        6 states, matched
        6 matches within stack
       32 transitions (= stored+matched)
       10 atomic steps

Counting steps, I see 24 steps by process 0 (that is the never claim process,
handling the LTL property), and 34 steps by the other active  processes.
Those 34 steps are close to what you would expect to see, with half the steps
by the never claim and half by the system.
If you remove the ltl property, you get depth matching the nr of transitions, so
yes, the larger depth number is contributed by running the LTL checker (the never
claim).
From the trace you should also be able to pin down why the nr of process steps is 34
and not 36, but that's probably more in the noise here.....

Offline

#5 2017-07-15 17:19:57

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

Re: What kind of states & transitions does Spin's “depth reached” consider

By the way, the property I used to check for the long trace
(after commenting out the original LTL property) is this:
(it uses embedded C code to get to the value of 'depth' that
spin itself maintains during the search);

never gh {

    do
    :: atomic { c_expr {depth >= 58} -> assert(0) }
    :: else
    od
}

Offline

#6 2017-08-09 13:42:52

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: What kind of states & transitions does Spin's “depth reached” consider

Thanks for your answer, and for the very helpful never claim.

Offline

Board footer

Powered by FluxBB