0b55f123 |
1 | #define elected (nr_leaders > 0) |
2 | #define noLeader (nr_leaders == 0) |
3 | #define oneLeader (nr_leaders == 1) |
4 | |
5 | /* |
6 | * Formula As Typed: <>[]oneLeader |
7 | * The Never Claim Below Corresponds |
8 | * To The Negated Formula !(<>[]oneLeader) |
9 | * (formalizing violations of the original) |
10 | */ |
11 | |
12 | never { /* !(<>[]oneLeader) */ |
13 | T0_init: |
14 | if |
15 | :: (1) -> goto T0_init |
16 | :: (! ((oneLeader))) -> goto accept_S5 |
17 | fi; |
18 | accept_S5: |
19 | if |
20 | :: (1) -> goto T0_init |
21 | fi; |
22 | accept_all: |
23 | skip |
24 | } |
25 | |
26 | #ifdef NOTES |
27 | Some other properties: |
28 | ![] noLeader |
29 | <> elected |
30 | [] (noLeader U oneLeader) |
31 | |
32 | |
33 | |
34 | |
35 | |
36 | |
37 | #endif |
38 | #ifdef RESULT |
39 | warning: for p.o. reduction to be valid the never claim must be stutter-closed |
40 | (never claims generated from LTL formulae are stutter-closed) |
41 | (Spin Version 3.1.2 -- 14 March 1998) |
42 | + Partial Order Reduction |
43 | |
44 | Full statespace search for: |
45 | never-claim + |
46 | assertion violations + (if within scope of claim) |
47 | acceptance cycles + (fairness disabled) |
48 | invalid endstates - (disabled by never-claim) |
49 | |
50 | State-vector 200 byte, depth reached 233, errors: 0 |
51 | 202 states, stored (402 visited) |
52 | 281 states, matched |
53 | 683 transitions (= visited+matched) |
54 | 36 atomic steps |
55 | hash conflicts: 0 (resolved) |
56 | (max size 2^19 states) |
57 | |
58 | 2.542 memory usage (Mbyte) |
59 | |
60 | unreached in proctype node |
61 | line 105, state 28, "out!two,nr" |
62 | (1 of 49 states) |
63 | unreached in proctype :init: |
64 | (0 of 11 states) |
65 | |
66 | real 0.13 |
67 | user 0.04 |
68 | sys 0.09 |
69 | |
70 | #endif |