: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 :initial :var x :cnj (= a[x] 1) (= c[x] false) (= d[x] false) (= e[x] false) (= f[x] false) (= g[x] false) :u_cnj (= c[z1] true) (= c[z2] true) (not (= h[z1] h[z2]) ) :comment T 1 :transition :var x :var y :var j :guard (= a[x] 1) (= f[x] false) (= c[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 true :val h[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val true :val h[j] :comment T 2 :transition :var x :var j :guard (= a[x] 1) (= d[x] true) (= f[x] false) (= c[x] false) :numcases 2 :case (= x j) :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val true :val true :val h[j] :case :val a[j] :val b[j] :val c[j] :val d[j] :val e[j] :val f[j] :val true :val h[j] :comment T 3 :transition :var x :var j :guard (= a[x] 1) (= g[x] true) (= d[x] true) (= f[x] true) :uguard (= f[j] true) :numcases 2 :case (= x j) :val 2 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :case :val 2 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :comment T 4 :transition :var x :var j :guard (= a[x] 1) (= g[x] false) (= d[x] true) (= f[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] :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] :comment T 5 :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] :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] :comment T 6 :transition :var x :var j :guard (= a[x] 2) (= c[x] false) (= 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] :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] :comment T 7 :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] :case :val 3 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :comment T 8 :transition :var x :var y :var j :guard (= a[x] 3) (= 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] :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] :comment T 9 :transition :var x :var j :guard (= a[x] 3) (= 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] :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] :comment T 10 :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 false :val g[j] :val h[j] :case :val 4 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val g[j] :val h[j] :comment T 11 :transition :var x :var y :var j :guard (= a[x] 4) (= d[x] true) (= d[y] false) (= e[y] false) :numcases 3 :case (= x j) :val 1 :val b[j] :val c[j] :val false :val true :val false :val false :val h[j] :case (= y j) (not(= x j)) :val 1 :val b[j] :val c[j] :val true :val e[j] :val false :val false :val h[j] :case (not (= x j)) (not (= y j) ) :val 1 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val false :val h[j] :comment T 12 :transition :var x :var j :guard (= d[x] false) (= e[x] false) :uguard (= d[j] false) :numcases 2 :case (= x j) :val 1 :val b[j] :val c[j] :val true :val e[j] :val false :val false :val h[j] :case :val 1 :val b[j] :val c[j] :val d[j] :val e[j] :val false :val false :val h[j] :comment T 13 :transition :var x :var j :guard (= c[x] true) (= f[x] false) :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] :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]