:index nat :comment ---------- FUNCTIONS and PREDICATES ----------- :map_back round :global a nat :map_back estimate :local b bool :map_back state :local c bool :map_back coord :local d bool :map_back aCoord :local e bool :map_back done :local f bool :map_back request :global g bool :map_back decisionValue :local h bool :map_back faulty :local i bool :map_back received :local k bool :map_back nack :local l bool :map_back id :local m int :map_back maxId :global n int :map_back tmpEstimate :global o bool :map_back processReceivedEstimate :local p bool :key_search a :comment ----------------------axioms-------------------------- :system_axiom :var x :cnj (and (< a[x] 8) (> (+ n[x] 3) 0) (> (+ m[x] 2) 0) ) :comment ----------------------axioms-------------------------- :suggested_negated_invariants :var z1 :var z2 :cnj (= d[z1] true) (= d[z2] true) :cnj (= d[z1] true) (= e[z2] false) (< z2 z1) :cnj (= d[z1] true) (> m[z1] z1) :cnj (= d[z1] true) (> m[z2] z1) :cnj (= a[z1] 1) (= d[z1] true) (= m[z2] z1) :cnj (= i[z1] false) (= l[z1] true) :cnj (= d[z1] true) (= e[z2] true) (> z2 z1) :end_of_suggested_negated_invariants :initial :var x :cnj (= a[x] 1) (= c[x] false) (= d[x] false) (= e[x] false) (= f[x] false) (= k[x] false) (= l[x] false) (= m[x] -1) (= n[x] -2) (= p[x] false) :u_cnj (= c[z1] true) (= k[z1] true) (= d[z2] true) (= c[z3] false) (= i[z3] false) (not (= b[z2] b[z3]) ) :u_cnj (> a[z1] 1) (= c[z1] false) (= i[z1] false) (= p[z1] true) (= d[z2] true) (not (= b[z1] b[z2]) ) :u_cnj (= d[z1] true) (= i[z1] false) (= a[z1] 6) (= c[z2] false) (= i[z2] false) :u_cnj (= c[z1] true) (= i[z1] false) (= c[z2] true) (= i[z2] false) (not (= h[z1] h[z2]) ) :inv_search_max_index_var 4 :comment T 1 :transition :var x :var y :var j :guard (= a[x] 1) (= f[x] false) (= c[x] false) (= d[y] true) (> m[x] n[x]) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val m[x] :val b[x] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val m[x] :val b[x] :val p[j] :comment T 2 :transition :var x :var y :var j :guard (= a[x] 1) (= f[x] false) (= c[x] false) (= d[y] true) (<= m[x] n[x]) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 3 :transition :var x :var y :var j :guard (= a[x] 1) (= f[x] false) (= c[x] false) (= d[y] true) (= i[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 4 :transition :var x :var j :guard (= a[x] 1) (= f[x] false) (= c[x] false) (= d[x] true) (> m[x] n[x]) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val m[x] :val b[x] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val m[x] :val b[x] :val p[j] :comment T 5 :transition :var x :var j :guard (= a[x] 1) (= f[x] false) (= c[x] false) (= d[x] true) (<= m[x] n[x]) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 6 :transition :var x :var j :guard (= a[x] 1) (= f[x] false) (= c[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 7 :transition :var x :var j :guard (= a[x] 1) (> n[x] -2) (= f[x] true) (= d[x] true) :uguard (= f[j] true) :numcases 2 :case (= x j) :val 2 :val o[x] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val 2 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 8 :transition :var x :var j :guard (= a[x] 1) (= n[x] -2) (= f[x] true) (= d[x] true) :uguard (= f[j] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val false :val true :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 9 :transition :var x :var y :var j :guard (= a[x] 2) (= f[x] false) (= c[x] false) (= d[y] true) :numcases 2 :case (= x j) :val a[j] :val b[y] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val true :val l[j] :val y :val n[j] :val o[j] :val true :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 10 :transition :var x :var y :var j :guard (= a[x] 2) (= f[x] false) (= c[x] false) (= d[y] true) (= i[y] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 11 :transition :var x :var j :guard (= a[x] 2) (= f[x] false) (= c[x] false) (= d[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val true :val l[j] :val x :val n[j] :val o[j] :val true :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 12 :transition :var x :var j :guard (= a[x] 2) (= f[x] false) (= c[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 13 :transition :var x :var j :guard (= a[x] 2) (= f[x] true) (= d[x] true) :uguard (= f[j] true) :numcases 2 :case (= x j) :val 3 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val 3 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 14 :transition :var x :var y :var j :guard (= a[x] 3) (= c[x] false) (= f[x] false) (= k[x] false) (= d[y] true) :numcases 3 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case (= j y) (not(= x j)) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val true :val m[j] :val n[j] :val o[j] :val p[j] :case (not (= x j)) (not (= j y) ) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 15 :transition :var x :var y :var j :guard (= a[x] 3) (= c[x] false) (= f[x] false) (= k[x] false) (= d[y] true) (= i[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 16 :transition :var x :var y :var j :guard (= a[x] 3) (= c[x] false) (= f[x] false) (= k[x] true) (= d[y] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 17 :transition :var x :var j :guard (= a[x] 3) (= f[x] false) (= d[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 18 :transition :var x :var y :var j :guard (= a[x] 3) (= c[x] true) (= f[x] false) (= d[y] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 19 :transition :var x :var j :guard (= a[x] 3) (= f[x] true) (= d[x] true) :uguard (= f[j] true) :numcases 2 :case (= x j) :val 4 :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val 4 :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 20 :transition :var x :var j :guard (= a[x] 4) (= d[x] false) :uguard (= l[j] false) :numcases 2 :case (= x j) :val 5 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val 5 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 21 :transition :var x :var y :var j :guard (= a[x] 5) (= f[x] false) (= c[x] false) (= d[y] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val true :val d[j] :val e[j] :val true :val g[j] :val b[x] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 22 :transition :var x :var y :var j :guard (= a[x] 5) (= f[x] false) (= c[x] false) (= d[y] true) (= i[y] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 23 :transition :var x :var j :guard (= a[x] 5) (= f[x] false) (= c[x] false) (= d[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val true :val d[j] :val e[j] :val true :val g[j] :val b[x] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 24 :transition :var x :var j :guard (= a[x] 5) (= f[x] false) (= c[x] true) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 25 :transition :var x :var j :guard (= a[x] 5) (= f[x] true) (= d[x] true) :uguard (= f[j] true) :numcases 2 :case (= x j) :val 6 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val 6 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 26 :transition :var x :var j :guard (= a[x] 6) (= d[x] true) :numcases 2 :case (= x j) :val 7 :val b[j] :val c[j] :val false :val true :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val 7 :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 27 :transition :var x :var j :guard (= d[x] false) :uguard (= d[j] false) :numcases 2 :case (= x j) :val 7 :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :case :val 7 :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val g[j] :val h[j] :val i[j] :val k[j] :val l[j] :val m[j] :val n[j] :val o[j] :val p[j] :comment T 28 :transition :var x :var j :guard (= d[x] false) (= e[x] false) (= a[x] 7) :uguard (>= j x) :uguard (< j x) (= e[j] true) :numcases 2 :case (= x j) :val 1 :val b[j] :val c[j] :val true :val e[j] :val false :val g[j] :val h[j] :val i[j] :val false :val false :val m[j] :val -2 :val o[j] :val p[j] :case :val 1 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :val i[j] :val false :val false :val m[j] :val -2 :val o[j] :val p[j]