Given the Peterson algorithm implementation (taken from p.92 "Principles of
the Spin model checker"), jSpin (4-6) reports a non-progress cycle although
Peterson is supposed to be starvation free (p. 161):
pan: non-progress cycle (at depth 12)
pan: wrote peterson-over.pml.trail
(Spin Version 5.2.4 -- 2 December 2009)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations + (if within scope of claim)
non-progress cycles + (fairness enabled)
invalid end states - (disabled by never claim)
State-vector 36 byte, depth reached 35, ••• errors: 1 •••
14 states, stored (19 visited)
3 states, matched
22 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
4.195 memory usage (Mbyte)
pan: elapsed time 0.01 seconds
Java is:
java version "1.6.0_15"
Java(TM) SE Runtime Environment (build 1.6.0_15-b03)
Java HotSpot(TM) 64-Bit Server VM (build 14.1-b02, mixed mode)
Original issue reported on code.google.com by markus.k...@gmail.com on 25 Jan 2010 at 4:28
Original issue reported on code.google.com by
markus.k...@gmail.com
on 25 Jan 2010 at 4:28Attachments: