leaderelection_inductive_withLoopB.spec 1.07 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, b), leader(a)
    AxiomPredicates:    next(a, b), leq(a, b), btw(a, b, c)
    As:                 -
    Bs:                 B(a,b)
    Constants:          -

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

Invariant
    ∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
    ∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
    ∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬leq(n1, n2)),
    ∀n1,n2,n3. (¬btw(n1,n2,n3) ∨ ¬msg(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)))