Peterson Algorithm and "Non-progress" Verification causes "pan: non-progress cycle (at depth 12)"

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

Attachments:

peterson-over.pml.trail

eyoon13 / jspin

Peterson Algorithm and "Non-progress" Verification causes "pan: non-progress cycle (at depth 12)" #2