%% Verification conditions for a leader-election algorithm, %% courtesy of Nikolaj Bjorner. type loc == lCrit | lElect | lMsg %Generated from the above data type definition: %value lCrit : loc %value lElect : loc %value lMsg : loc % lCrit, lElect and lMsg are distinct % and the only elements of the type loc. in N : int local J : array [1..N] of [1..N] local l : array [1..N] of loc local b : array [1..N] of bool local b0 : array [1..N] of bool local alive : array [1..N] of bool AXIOM: Forall m,k,t : [1..N] . l[m] = lMsg /\ J[m]=k /\ t < m /\ m <= k --> ~alive[t] GOAL 1 ====== 1 < N /\ (Forall i : [1..N] . l[i] = lElect) /\ (Forall i : [1..N] . b[i]) /\ (Forall i : [1..N] . alive[i]) --> (Forall x, y : [1..N] . l[x] = lCrit /\ l[y] = lCrit --> x = y) /\ (Forall k, m : [1..N] . alive[k] /\ l[m] = lMsg /\ J[m] = k --> (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] = b0[m]) else ~(b[k] = b0[m]) --> (Forall r : [1..k], n : [1..N] . alive[r] /\ (l[n] = lMsg /\ J[n] = r) /\ b[r] = b0[n] --> (if r < m then r < n /\ n <= m else r < n \/ n <= m)) /\ (Forall z : [1..N] . ~(l[z] = lCrit)))) GOAL 2 ====== (Forall i : [1..N] . ((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(if i = y then lCrit = lElect else l[y] = lCrit)) \/ ~(if i = x then lCrit = lElect else l[x] = lCrit)) \/ (1 <= N --> N < 1)) /\ ((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ (if i = j then lCrit = lElect else l[j] = lCrit) then ~((if i = k then ~b[i] else b[k]) <--> b0[m]) else ~((if i = k then ~b[i] else b[k]) <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(if i = n then lElect = lMsg else l[n] = lMsg) \/ ~(r = J[n]) \/ ~((if i = r then ~b[i] else b[r]) <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(if i = z then lCrit = lElect else l[z] = lCrit))) \/ ~(if i = m then lElect = lMsg else l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1)) \/ ~(l[i] = lCrit) \/ ~(l[if N = i then 1 else i + 1] = lElect)) \/ (1 <= N --> ~((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(l[y] = lCrit)) \/ ~(l[x] = lCrit)) \/ (1 <= N --> N < 1)) \/ ~((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1))) GOAL 3 ====== (Forall i : [1..N] . ((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(if i = y then lCrit = lElect else (if N = i then y = 1 else y = i + 1) \/ l[y] = lCrit)) \/ ~(if i = x then lCrit = lElect else (if N = i then x = 1 else x = i + 1) \/ l[x] = lCrit)) \/ (1 <= N --> N < 1)) /\ ((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ (if i = j then lCrit = lElect else (if N = i then j = 1 else j = i + 1) \/ l[j] = lCrit) then ~((if i = k then ~b[i] else b[k]) <--> b0[m]) else ~((if i = k then ~b[i] else b[k]) <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(if i = n then lElect = lMsg else (if if N = i then n = 1 else n = i + 1 then lCrit = lMsg else l[n] = lMsg)) \/ ~(r = J[n]) \/ ~((if i = r then ~b[i] else b[r]) <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(if i = z then lCrit = lElect else (if N = i then z = 1 else z = i + 1) \/ l[z] = lCrit))) \/ ~(if i = m then lElect = lMsg else (if if N = i then m = 1 else m = i + 1 then lCrit = lMsg else l[m] = lMsg)) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1)) \/ ~(l[i] = lCrit) \/ ~(l[if N = i then 1 else i + 1] = lElect)) \/ (1 <= N --> ~((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(l[y] = lCrit)) \/ ~(l[x] = lCrit)) \/ (1 <= N --> N < 1)) \/ ~((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1))) GOAL 4 ====== (Forall i : [1..N] . ((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(if if N = i then y = 1 else y = i + 1 then lCrit = lMsg else l[y] = lCrit)) \/ ~(if if N = i then x = 1 else x = i + 1 then lCrit = lMsg else l[x] = lCrit)) \/ (1 <= N --> N < 1)) /\ ((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ (if if N = i then j = 1 else j = i + 1 then lCrit = lMsg else l[j] = lCrit) then ~(b[k] <--> (if if N = i then m = 1 else m = i + 1 then b[i] else b0[m])) else ~(b[k] <--> (if if N = i then m = 1 else m = i + 1 then b[i] else b0[m])) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~((if N = i then n = 1 else n = i + 1) \/ l[n] = lMsg) \/ ~(if if N = i then n = 1 else n = i + 1 then i = r else r = J[n]) \/ ~(b[r] <--> (if if N = i then n = 1 else n = i + 1 then b[i] else b0[n]))) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(if if N = i then z = 1 else z = i + 1 then lCrit = lMsg else l[z] = lCrit))) \/ ~((if N = i then m = 1 else m = i + 1) \/ l[m] = lMsg) \/ ~(if if N = i then m = 1 else m = i + 1 then i = k else k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1)) \/ ~(l[i] = lElect) \/ ~(l[if N = i then 1 else i + 1] = lElect) \/ ~alive[i]) \/ (1 <= N --> ~((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(l[y] = lCrit)) \/ ~(l[x] = lCrit)) \/ (1 <= N --> N < 1)) \/ ~((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1))) GOAL 5 ====== (Forall i : [1..N] . ((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(i = y \/ l[y] = lCrit)) \/ ~(i = x \/ l[x] = lCrit)) \/ (1 <= N --> N < 1)) /\ ((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ (i = j \/ l[j] = lCrit) then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(if i = n then lCrit = lMsg else l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ ~(1 <= i /\ i <= N) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(if i = m then lCrit = lMsg else l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1)) \/ ~(l[i] = lMsg) \/ ~(b0[i] <--> b[i]) \/ ~(i = J[i]) \/ ~alive[i]) \/ (1 <= N --> ~((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(l[y] = lCrit)) \/ ~(l[x] = lCrit)) \/ (1 <= N --> N < 1)) \/ ~((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1))) GOAL 6 ====== (Forall i : [1..N] . ((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(if i = y then lCrit = lElect else l[y] = lCrit)) \/ ~(if i = x then lCrit = lElect else l[x] = lCrit)) \/ (1 <= N --> N < 1)) /\ ((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ (if i = j then lCrit = lElect else l[j] = lCrit) then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(if i = n then lElect = lMsg else l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(if i = z then lCrit = lElect else l[z] = lCrit))) \/ ~(if i = m then lElect = lMsg else l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1)) \/ ~(l[i] = lMsg) \/ (b0[i] <--> b[i]) /\ i = J[i] /\ alive[i] \/ ~(alive[i] /\ i < J[i] \/ i = J[i] \/ l[if N = i then 1 else i + 1] = lElect)) \/ (1 <= N --> ~((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(l[y] = lCrit)) \/ ~(l[x] = lCrit)) \/ (1 <= N --> N < 1)) \/ ~((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1))) GOAL 7 ====== (Forall i : [1..N] . ((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(if i = y then lCrit = lElect else (if if N = i then y = 1 else y = i + 1 then lCrit = lMsg else l[y] = lCrit))) \/ ~(if i = x then lCrit = lElect else (if if N = i then x = 1 else x = i + 1 then lCrit = lMsg else l[x] = lCrit))) \/ (1 <= N --> N < 1)) /\ ((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ (if i = j then lCrit = lElect else (if if N = i then j = 1 else j = i + 1 then lCrit = lMsg else l[j] = lCrit)) then ~(b[k] <--> (if if N = i then m = 1 else m = i + 1 then b0[i] else b0[m])) else ~(b[k] <--> (if if N = i then m = 1 else m = i + 1 then b0[i] else b0[m])) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(if i = n then lElect = lMsg else (if N = i then n = 1 else n = i + 1) \/ l[n] = lMsg) \/ ~(if if N = i then n = 1 else n = i + 1 then r = J[i] else r = J[n]) \/ ~(b[r] <--> (if if N = i then n = 1 else n = i + 1 then b0[i] else b0[n]))) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(if i = z then lCrit = lElect else (if if N = i then z = 1 else z = i + 1 then lCrit = lMsg else l[z] = lCrit)))) \/ ~(if i = m then lElect = lMsg else (if N = i then m = 1 else m = i + 1) \/ l[m] = lMsg) \/ ~(if if N = i then m = 1 else m = i + 1 then k = J[i] else k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1)) \/ ~(l[i] = lMsg) \/ ~(alive[i] --> J[i] < i) \/ ~(l[if N = i then 1 else i + 1] = lElect) \/ i = J[i]) \/ (1 <= N --> ~((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(l[y] = lCrit)) \/ ~(l[x] = lCrit)) \/ (1 <= N --> N < 1)) \/ ~((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1))) GOAL 8 ====== (Forall i : [1..N] . ((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(if i = y then lCrit = lElect else l[y] = lCrit)) \/ ~(if i = x then lCrit = lElect else l[x] = lCrit)) \/ (1 <= N --> N < 1)) /\ ((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ (if i = j then lCrit = lElect else l[j] = lCrit) then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(if i = n then lElect = lMsg else l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ i = r \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(if i = z then lCrit = lElect else l[z] = lCrit))) \/ ~(if i = m then lElect = lMsg else l[m] = lMsg) \/ ~(k = J[m])) \/ i = k \/ ~alive[k]) \/ (1 <= N --> N < 1)) \/ ~alive[i]) \/ (1 <= N --> ~((Forall x : [1..N] . (Forall y : [1..N] . x = y \/ ~(l[y] = lCrit)) \/ ~(l[x] = lCrit)) \/ (1 <= N --> N < 1)) \/ ~((Forall k : [1..N] . (Forall m : [1..N] . (if Exists j : [1..N] . (if k < m then k < j /\ j <= m else k < j \/ j <= m) /\ l[j] = lCrit then ~(b[k] <--> b0[m]) else ~(b[k] <--> b0[m]) --> ((Forall r : [1..k] . (Forall n : [1..N] . (if r < m then r < n /\ n <= m else r < n \/ n <= m) \/ ~(l[n] = lMsg) \/ ~(r = J[n]) \/ ~(b[r] <--> b0[n])) \/ ~alive[r]) \/ (1 <= k --> N < 1)) /\ (Forall z : [1..N] . ~(l[z] = lCrit))) \/ ~(l[m] = lMsg) \/ ~(k = J[m])) \/ ~alive[k]) \/ (1 <= N --> N < 1)))