: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]