1 #define elected (nr_leaders > 0)
2 #define noLeader (nr_leaders == 0)
3 #define oneLeader (nr_leaders == 1)
6 * Formula As Typed: <>[]oneLeader
7 * The Never Claim Below Corresponds
8 * To The Negated Formula !(<>[]oneLeader)
9 * (formalizing violations of the original)
12 never { /* !(<>[]oneLeader) */
15 :: (1) -> goto T0_init
16 :: (! ((oneLeader))) -> goto accept_S5
20 :: (1) -> goto T0_init
27 Some other properties:
30 [] (noLeader U oneLeader)
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
44 Full statespace search for:
46 assertion violations + (if within scope of claim)
47 acceptance cycles + (fairness disabled)
48 invalid endstates - (disabled by never-claim)
50 State-vector 200 byte, depth reached 233, errors: 0
51 202 states, stored (402 visited)
53 683 transitions (= visited+matched)
55 hash conflicts: 0 (resolved)
56 (max size 2^19 states)
58 2.542 memory usage (Mbyte)
60 unreached in proctype node
61 line 105, state 28, "out!two,nr"
63 unreached in proctype :init: