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

DavidFarago · 2017-06-24 09:36:16

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?

spinroot · 2017-07-11 17:38:55

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?

DavidFarago · 2017-07-14 10:45:39

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)

spinroot · 2017-07-15 17:18:02

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.....

spinroot · 2017-07-15 17:19:57

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
}

DavidFarago · 2017-08-09 13:42:52

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

Spinroot

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

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

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

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

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

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

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

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

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

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

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

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

Board footer