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_S13
17 :: (! ((q)) && (p)) -> goto T0_S26
18 :: (! ((q))) -> goto T0_S32
19 :: (! ((r))) -> goto T0_S44
20 :: (1) -> goto T0_init
24 :: (! ((q)) && ! ((r))) -> goto T0_S8
28 :: (! ((q)) && ! ((r))) -> goto accept_S8
32 :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
33 :: (! ((q)) && ! ((r))) -> goto T0_S13
37 :: (! ((q)) && ! ((r))) -> goto accept_S8
38 :: (! ((q))) -> goto T0_S26
42 :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
43 :: (! ((q)) && ! ((r))) -> goto T0_S13
44 :: (! ((q)) && (p)) -> goto T0_S26
45 :: (! ((q))) -> goto T0_S32
49 :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
50 :: (! ((q)) && ! ((r))) -> goto T0_S13
51 :: (! ((r))) -> goto T0_S44
58 Use Load to open a file or a template.
61 warning: for p.o. reduction to be valid the never claim must be stutter-closed
62 (never claims generated from LTL formulae are stutter-closed)
63 (Spin Version 3.2.4 -- 16 October 1998)
64 + Partial Order Reduction
66 Full statespace search for:
68 assertion violations + (if within scope of claim)
69 acceptance cycles + (fairness disabled)
70 invalid endstates - (disabled by never-claim)
72 State-vector 96 byte, depth reached 1944, errors: 0
73 16191 states, stored (18994 visited)
75 65775 transitions (= visited+matched)
77 hash conflicts: 1713 (resolved)
78 (max size 2^19 states)
80 Stats on memory usage (in Megabytes):
81 1.684 equivalent memory usage for states (stored*(State-vector + overhead))
82 0.998 actual memory usage for states (compression: 59.24%)
83 State-vector as stored = 54 byte + 8 byte overhead
84 2.097 memory used for hash-table (-w19)
85 0.240 memory used for DFS stack (-m10000)
86 3.464 total actual memory usage
88 unreached in proctype CC
89 line 28, state 25, "-end-"
91 unreached in proctype HC
92 line 35, state 6, "-end-"
94 unreached in proctype BS
95 line 65, state 31, "-end-"
97 unreached in proctype MS
98 line 78, state 14, "-end-"
100 unreached in proctype System
101 line 98, state 13, "-end-"
103 unreached in proctype Out
104 line 105, state 7, "-end-"