0b55f123 |
1 | #define p in?[red] |
2 | #define q out?[red] |
3 | #define r (BS[a_id]@progress || BS[p_id]@progress) |
4 | |
5 | /* |
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) |
10 | */ |
11 | |
12 | never { /* !((![]<>(r)) -> [](<>p -> <>q)) */ |
13 | T0_init: |
14 | if |
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 |
21 | fi; |
22 | accept_S8: |
23 | if |
24 | :: (! ((q)) && ! ((r))) -> goto accept_S8 |
25 | fi; |
26 | T0_S17: |
27 | if |
28 | :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8 |
29 | :: (! ((q)) && ! ((r))) -> goto T0_S17 |
30 | fi; |
31 | T0_S44: |
32 | if |
33 | :: (! ((q)) && ! ((r))) -> goto accept_S8 |
34 | :: (! ((q))) -> goto T0_S44 |
35 | fi; |
36 | T0_S58: |
37 | if |
38 | :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8 |
39 | :: (! ((q)) && ! ((r))) -> goto T0_S17 |
40 | :: (! ((q)) && (p)) -> goto T0_S44 |
41 | :: (! ((q))) -> goto T0_S58 |
42 | fi; |
43 | T0_S91: |
44 | if |
45 | :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8 |
46 | :: (! ((q)) && ! ((r))) -> goto T0_S17 |
47 | :: (! ((r))) -> goto T0_S91 |
48 | fi; |
49 | } |
50 | |
51 | #ifdef NOTES |
52 | Use Load to open a file or a template. |
53 | |
54 | |
55 | #endif |
56 | #ifdef RESULT |
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 |
61 | |
62 | Full statespace search for: |
63 | never-claim + |
64 | assertion violations + (if within scope of claim) |
65 | acceptance cycles + (fairness disabled) |
66 | invalid endstates - (disabled by never-claim) |
67 | |
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) |
72 | 241 atomic steps |
73 | hash conflicts: 8962 (resolved) |
74 | (max size 2^19 states) |
75 | |
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 |
83 | |
84 | unreached in proctype CC |
85 | line 49, state 25, "-end-" |
86 | (1 of 25 states) |
87 | unreached in proctype HC |
88 | line 56, state 6, "-end-" |
89 | (1 of 6 states) |
90 | unreached in proctype MSC |
91 | (0 of 4 states) |
92 | unreached in proctype BS |
93 | line 95, state 31, "-end-" |
94 | (1 of 31 states) |
95 | unreached in proctype MS |
96 | line 108, state 14, "-end-" |
97 | (1 of 14 states) |
98 | unreached in proctype P |
99 | (0 of 4 states) |
100 | unreached in proctype Q |
101 | (0 of 4 states) |
102 | unreached in proctype System |
103 | (0 of 4 states) |
104 | unreached in proctype top |
105 | line 143, state 7, "-end-" |
106 | (1 of 7 states) |
107 | unreached in proctype bot |
108 | line 149, state 7, "-end-" |
109 | (1 of 7 states) |
110 | 5.1u 0.1s 5r ./pan -X -m10000 -w19 -a ... |
111 | |
112 | #endif |