3 #define r (BS[a_id]@progress || BS[p_id]@progress)
6 * Formula As Typed: (![]<>(r)) -> [](<>p -> <>q)
7 * The Never Claim Below Corresponds
8 * To The Negated Formula !((![]<>(r)) -> [](<>p -> <>q))
9 * (formalizing violations of the original)
12 never { /* !((![]<>(r)) -> [](<>p -> <>q)) */
15 :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
16 :: (! ((q)) && ! ((r))) -> goto T0_S17
17 :: (! ((q)) && (p)) -> goto T0_S44
18 :: (! ((q))) -> goto T0_S58
19 :: (! ((r))) -> goto T0_S91
20 :: (1) -> goto T0_init
24 :: (! ((q)) && ! ((r))) -> goto accept_S8
28 :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
29 :: (! ((q)) && ! ((r))) -> goto T0_S17
33 :: (! ((q)) && ! ((r))) -> goto accept_S8
34 :: (! ((q))) -> goto T0_S44
38 :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
39 :: (! ((q)) && ! ((r))) -> goto T0_S17
40 :: (! ((q)) && (p)) -> goto T0_S44
41 :: (! ((q))) -> goto T0_S58
45 :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
46 :: (! ((q)) && ! ((r))) -> goto T0_S17
47 :: (! ((r))) -> goto T0_S91
52 Use Load to open a file or a template.
57 warning: for p.o. reduction to be valid the never claim must be stutter-closed
58 (never claims generated from LTL formulae are stutter-closed)
59 (Spin Version 3.4.0 -- 7 August 2000)
60 + Partial Order Reduction
62 Full statespace search for:
64 assertion violations + (if within scope of claim)
65 acceptance cycles + (fairness disabled)
66 invalid endstates - (disabled by never-claim)
68 State-vector 128 byte, depth reached 1833, errors: 0
69 44455 states, stored (48719 visited)
70 137737 states, matched
71 186456 transitions (= visited+matched)
73 hash conflicts: 8962 (resolved)
74 (max size 2^19 states)
76 Stats on memory usage (in Megabytes):
77 6.046 equivalent memory usage for states (stored*(State-vector + overhead))
78 3.379 actual memory usage for states (compression: 55.89%)
79 State-vector as stored = 68 byte + 8 byte overhead
80 2.097 memory used for hash-table (-w19)
81 0.240 memory used for DFS stack (-m10000)
82 5.819 total actual memory usage
84 unreached in proctype CC
85 line 49, state 25, "-end-"
87 unreached in proctype HC
88 line 56, state 6, "-end-"
90 unreached in proctype MSC
92 unreached in proctype BS
93 line 95, state 31, "-end-"
95 unreached in proctype MS
96 line 108, state 14, "-end-"
98 unreached in proctype P
100 unreached in proctype Q
102 unreached in proctype System
104 unreached in proctype top
105 line 143, state 7, "-end-"
107 unreached in proctype bot
108 line 149, state 7, "-end-"
110 5.1u 0.1s 5r ./pan -X -m10000 -w19 -a ...