| 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 |