never gh {
do
:: atomic { c_expr {depth >= 58} -> assert(0) }
:: else
od
}
(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.....
#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)
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?
]]>