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_S13 |
17 | :: (! ((q)) && (p)) -> goto T0_S26 |
18 | :: (! ((q))) -> goto T0_S32 |
19 | :: (! ((r))) -> goto T0_S44 |
20 | :: (1) -> goto T0_init |
21 | fi; |
22 | accept_S8: |
23 | if |
24 | :: (! ((q)) && ! ((r))) -> goto T0_S8 |
25 | fi; |
26 | T0_S8: |
27 | if |
28 | :: (! ((q)) && ! ((r))) -> goto accept_S8 |
29 | fi; |
30 | T0_S13: |
31 | if |
32 | :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8 |
33 | :: (! ((q)) && ! ((r))) -> goto T0_S13 |
34 | fi; |
35 | T0_S26: |
36 | if |
37 | :: (! ((q)) && ! ((r))) -> goto accept_S8 |
38 | :: (! ((q))) -> goto T0_S26 |
39 | fi; |
40 | T0_S32: |
41 | if |
42 | :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8 |
43 | :: (! ((q)) && ! ((r))) -> goto T0_S13 |
44 | :: (! ((q)) && (p)) -> goto T0_S26 |
45 | :: (! ((q))) -> goto T0_S32 |
46 | fi; |
47 | T0_S44: |
48 | if |
49 | :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8 |
50 | :: (! ((q)) && ! ((r))) -> goto T0_S13 |
51 | :: (! ((r))) -> goto T0_S44 |
52 | fi; |
53 | accept_all: |
54 | skip |
55 | } |
56 | |
57 | #ifdef NOTES |
58 | Use Load to open a file or a template. |
59 | #endif |
60 | #ifdef RESULT |
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 |
65 | |
66 | Full statespace search for: |
67 | never-claim + |
68 | assertion violations + (if within scope of claim) |
69 | acceptance cycles + (fairness disabled) |
70 | invalid endstates - (disabled by never-claim) |
71 | |
72 | State-vector 96 byte, depth reached 1944, errors: 0 |
73 | 16191 states, stored (18994 visited) |
74 | 46781 states, matched |
75 | 65775 transitions (= visited+matched) |
76 | 16 atomic steps |
77 | hash conflicts: 1713 (resolved) |
78 | (max size 2^19 states) |
79 | |
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 |
87 | |
88 | unreached in proctype CC |
89 | line 28, state 25, "-end-" |
90 | (1 of 25 states) |
91 | unreached in proctype HC |
92 | line 35, state 6, "-end-" |
93 | (1 of 6 states) |
94 | unreached in proctype BS |
95 | line 65, state 31, "-end-" |
96 | (1 of 31 states) |
97 | unreached in proctype MS |
98 | line 78, state 14, "-end-" |
99 | (1 of 14 states) |
100 | unreached in proctype System |
101 | line 98, state 13, "-end-" |
102 | (1 of 13 states) |
103 | unreached in proctype Out |
104 | line 105, state 7, "-end-" |
105 | (1 of 7 states) |
106 | |
107 | #endif |