title: Counter Loops in Transition Systems - Z3
body: <p>I use the PDR engine of Z3 to prove invariants in transition systems.
  When a transition system includes a counter loop which has to be passed to reach a specific state the performance is slow.</p>
  
  <p>In the following source code you see an example of a transition system containing 3 states and 3 transitions implemented with the Transition System Python Class on the <a href="http://rise4fun.com/z3py/tutorial/fixedpoints" rel="nofollow">Z3 Fixedpoint Homepage</a>. In the last line there is a query to reach state L2 beginning from state L0. Therefore transition t2 has to be passed y times.</p>
  
  <p>If I initialize y==10 the answer is computed fast. But with initialization y==1000 the performance is slow.</p>
  
  <pre><code>L0 = L.L0 
  L1 = L.L1
  L2 = L.L2
  y=Int('y')
  i = Int('i')
  state  = Const('state', L)
  
  t1 = { "guard" : state == L0,
     "effect" : [ L1, i ] }
  t2 = { "guard" : And(state == L1),
     "effect" : [ L1, i+1 ] }
  t3 = { "guard" : And(state == L1,i&gt;y),
     "effect" : [ L2, i]}
  
  ptr = TransitionSystem( And(state == L0, i == 0, y==10),[t1, t2, t3],[state, i])
  ptr.query(state==L2)
  </code></pre>
  
  <p>Is there a possibility to compute the path from L0 to L2 in other way with Z3 achieving better performance ?</p>