leaderelection_inductive_withNegB2.spec 1.13 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
Signature
    EmptyPredicates:    msg(a, i, b), leader(a)
    AxiomPredicates:    next(a, b), leq(a, b), btw(a, b, c)
    As:                 A(a)
    Bs:                 B(a,i,b)
    Constants:          -

Transition System
    msg(a,i,b) := (next(a,b) ∧ B(a,i,b))
    loop {
        leader(b) := ∃a. msg(a, b, b)
        msg(a,i,b) := (A(a) ∧ next(a, b) ∧ ∃c. msg(c, i, a) ∧ leq(a, i))
    }

Invariant
    ∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
    ∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
    ∀n1,n2,n3. (n1 = n2 ∨ ¬msg(n3, n1, n1) ∨ ¬leq(n1, n2)),
    ∀n1,n2,n3,n4. (¬btw(n1,n2,n3) ∨ ¬msg(n4,n2,n1) ∨ ¬leq(n2,n3))

Axioms
    ∀x. leq(x,x),
    ∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)),
    ∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y),
    ∀x,y. (leq(x,y) ∨ leq(y,x)),

    ∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)),
    ∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)),
    ∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)),
    ∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)),

    ∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))