NO Initial ITS Start location: l8 Program variables: __rho_1_^0 c^0 curr_serv^0 resp^0 servers^0 serversdiv2^0 tmp1^0 0: l0 -> l1 : __rho_1_^0'=__rho_1_^post1, c^0'=c^post1, curr_serv^0'=curr_serv^post1, resp^0'=resp^post1, servers^0'=servers^post1, serversdiv2^0'=serversdiv2^post1, tmp1^0'=tmp1^post1, (c^0-c^post1 == 0 /\ -resp^post1+resp^0 == 0 /\ serversdiv2^0-serversdiv2^post1 == 0 /\ servers^0-servers^post1 == 0 /\ -curr_serv^post1+curr_serv^0 == 0 /\ -__rho_1_^post1+__rho_1_^0 == 0 /\ -tmp1^post1+tmp1^0 == 0), cost: 1 6: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, c^0'=c^post7, curr_serv^0'=curr_serv^post7, resp^0'=resp^post7, servers^0'=servers^post7, serversdiv2^0'=serversdiv2^post7, tmp1^0'=tmp1^post7, (0 == 0 /\ servers^0-servers^post7 == 0 /\ c^0-c^post7 == 0 /\ -resp^post7+resp^0 == 0 /\ -serversdiv2^post7+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post7 == 0 /\ 1-curr_serv^0 <= 0 /\ -curr_serv^post7+curr_serv^0 == 0), cost: 1 7: l1 -> l4 : __rho_1_^0'=__rho_1_^post8, c^0'=c^post8, curr_serv^0'=curr_serv^post8, resp^0'=resp^post8, servers^0'=servers^post8, serversdiv2^0'=serversdiv2^post8, tmp1^0'=tmp1^post8, (__rho_1_^0-__rho_1_^post8 == 0 /\ -serversdiv2^post8+serversdiv2^0 == 0 /\ -c^post8+c^0 == 0 /\ tmp1^0-tmp1^post8 == 0 /\ resp^0-resp^post8 == 0 /\ curr_serv^0 <= 0 /\ -servers^post8+servers^0 == 0 /\ -curr_serv^post8+curr_serv^0 == 0), cost: 1 1: l2 -> l3 : __rho_1_^0'=__rho_1_^post2, c^0'=c^post2, curr_serv^0'=curr_serv^post2, resp^0'=resp^post2, servers^0'=servers^post2, serversdiv2^0'=serversdiv2^post2, tmp1^0'=tmp1^post2, (-serversdiv2^post2+serversdiv2^0 == 0 /\ -__rho_1_^post2+__rho_1_^0 == 0 /\ -resp^post2+resp^0 == 0 /\ -curr_serv^post2+curr_serv^0 == 0 /\ tmp1^0-tmp1^post2 == 0 /\ servers^0-servers^post2 == 0 /\ c^0-c^post2 == 0), cost: 1 2: l4 -> l5 : __rho_1_^0'=__rho_1_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, serversdiv2^0'=serversdiv2^post3, tmp1^0'=tmp1^post3, (-serversdiv2^post3+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post3 == 0 /\ servers^0-servers^post3 == 0 /\ resp^0-resp^post3 == 0 /\ c^0-c^post3 == 0 /\ -curr_serv^post3+curr_serv^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0), cost: 1 3: l5 -> l4 : __rho_1_^0'=__rho_1_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, serversdiv2^0'=serversdiv2^post4, tmp1^0'=tmp1^post4, (resp^0-resp^post4 == 0 /\ -servers^post4+servers^0 == 0 /\ __rho_1_^0-__rho_1_^post4 == 0 /\ -curr_serv^post4+curr_serv^0 == 0 /\ tmp1^0-tmp1^post4 == 0 /\ -c^post4+c^0 == 0 /\ -serversdiv2^post4+serversdiv2^0 == 0), cost: 1 4: l6 -> l0 : __rho_1_^0'=__rho_1_^post5, c^0'=c^post5, curr_serv^0'=curr_serv^post5, resp^0'=resp^post5, servers^0'=servers^post5, serversdiv2^0'=serversdiv2^post5, tmp1^0'=tmp1^post5, (__rho_1_^0-__rho_1_^post5 == 0 /\ tmp1^0-tmp1^post5 == 0 /\ 1+curr_serv^post5-curr_serv^0 == 0 /\ servers^0-servers^post5 == 0 /\ resp^0-resp^post5 == 0 /\ 1+c^0-curr_serv^0 <= 0 /\ -c^post5+c^0 == 0 /\ __rho_1_^0 <= 0 /\ -serversdiv2^post5+serversdiv2^0 == 0), cost: 1 5: l6 -> l0 : __rho_1_^0'=__rho_1_^post6, c^0'=c^post6, curr_serv^0'=curr_serv^post6, resp^0'=resp^post6, servers^0'=servers^post6, serversdiv2^0'=serversdiv2^post6, tmp1^0'=tmp1^post6, (servers^0-servers^post6 == 0 /\ 1-c^0+c^post6 == 0 /\ -1+resp^post6-resp^0 == 0 /\ 1-__rho_1_^0 <= 0 /\ -__rho_1_^post6+__rho_1_^0 == 0 /\ -tmp1^post6+tmp1^0 == 0 /\ 1+curr_serv^post6-curr_serv^0 == 0 /\ serversdiv2^0-serversdiv2^post6 == 0), cost: 1 8: l7 -> l0 : __rho_1_^0'=__rho_1_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 == 0 /\ -__rho_1_^post9+__rho_1_^0 == 0 /\ -servers^post9+curr_serv^post9 == 0 /\ -1+servers^post9-2*serversdiv2^post9 <= 0 /\ 1-servers^post9+2*serversdiv2^post9 <= 0 /\ -tmp1^post9+c^post9 == 0 /\ 1-servers^post9 <= 0 /\ 1-c^post9 <= 0 /\ resp^post9 == 0), cost: 1 9: l8 -> l7 : __rho_1_^0'=__rho_1_^post10, c^0'=c^post10, curr_serv^0'=curr_serv^post10, resp^0'=resp^post10, servers^0'=servers^post10, serversdiv2^0'=serversdiv2^post10, tmp1^0'=tmp1^post10, (c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ servers^0-servers^post10 == 0), cost: 1 Chained Linear Paths Start location: l8 Program variables: __rho_1_^0 c^0 curr_serv^0 resp^0 servers^0 serversdiv2^0 tmp1^0 0: l0 -> l1 : __rho_1_^0'=__rho_1_^post1, c^0'=c^post1, curr_serv^0'=curr_serv^post1, resp^0'=resp^post1, servers^0'=servers^post1, serversdiv2^0'=serversdiv2^post1, tmp1^0'=tmp1^post1, (c^0-c^post1 == 0 /\ -resp^post1+resp^0 == 0 /\ serversdiv2^0-serversdiv2^post1 == 0 /\ servers^0-servers^post1 == 0 /\ -curr_serv^post1+curr_serv^0 == 0 /\ -__rho_1_^post1+__rho_1_^0 == 0 /\ -tmp1^post1+tmp1^0 == 0), cost: 1 6: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, c^0'=c^post7, curr_serv^0'=curr_serv^post7, resp^0'=resp^post7, servers^0'=servers^post7, serversdiv2^0'=serversdiv2^post7, tmp1^0'=tmp1^post7, (0 == 0 /\ servers^0-servers^post7 == 0 /\ c^0-c^post7 == 0 /\ -resp^post7+resp^0 == 0 /\ -serversdiv2^post7+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post7 == 0 /\ 1-curr_serv^0 <= 0 /\ -curr_serv^post7+curr_serv^0 == 0), cost: 1 7: l1 -> l4 : __rho_1_^0'=__rho_1_^post8, c^0'=c^post8, curr_serv^0'=curr_serv^post8, resp^0'=resp^post8, servers^0'=servers^post8, serversdiv2^0'=serversdiv2^post8, tmp1^0'=tmp1^post8, (__rho_1_^0-__rho_1_^post8 == 0 /\ -serversdiv2^post8+serversdiv2^0 == 0 /\ -c^post8+c^0 == 0 /\ tmp1^0-tmp1^post8 == 0 /\ resp^0-resp^post8 == 0 /\ curr_serv^0 <= 0 /\ -servers^post8+servers^0 == 0 /\ -curr_serv^post8+curr_serv^0 == 0), cost: 1 1: l2 -> l3 : __rho_1_^0'=__rho_1_^post2, c^0'=c^post2, curr_serv^0'=curr_serv^post2, resp^0'=resp^post2, servers^0'=servers^post2, serversdiv2^0'=serversdiv2^post2, tmp1^0'=tmp1^post2, (-serversdiv2^post2+serversdiv2^0 == 0 /\ -__rho_1_^post2+__rho_1_^0 == 0 /\ -resp^post2+resp^0 == 0 /\ -curr_serv^post2+curr_serv^0 == 0 /\ tmp1^0-tmp1^post2 == 0 /\ servers^0-servers^post2 == 0 /\ c^0-c^post2 == 0), cost: 1 11: l4 -> l4 : __rho_1_^0'=__rho_1_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, serversdiv2^0'=serversdiv2^post4, tmp1^0'=tmp1^post4, (-serversdiv2^post3+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post3 == 0 /\ resp^post3-resp^post4 == 0 /\ servers^0-servers^post3 == 0 /\ resp^0-resp^post3 == 0 /\ __rho_1_^post3-__rho_1_^post4 == 0 /\ serversdiv2^post3-serversdiv2^post4 == 0 /\ c^0-c^post3 == 0 /\ -c^post4+c^post3 == 0 /\ curr_serv^post3-curr_serv^post4 == 0 /\ -servers^post4+servers^post3 == 0 /\ tmp1^post3-tmp1^post4 == 0 /\ -curr_serv^post3+curr_serv^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0), cost: 1 4: l6 -> l0 : __rho_1_^0'=__rho_1_^post5, c^0'=c^post5, curr_serv^0'=curr_serv^post5, resp^0'=resp^post5, servers^0'=servers^post5, serversdiv2^0'=serversdiv2^post5, tmp1^0'=tmp1^post5, (__rho_1_^0-__rho_1_^post5 == 0 /\ tmp1^0-tmp1^post5 == 0 /\ 1+curr_serv^post5-curr_serv^0 == 0 /\ servers^0-servers^post5 == 0 /\ resp^0-resp^post5 == 0 /\ 1+c^0-curr_serv^0 <= 0 /\ -c^post5+c^0 == 0 /\ __rho_1_^0 <= 0 /\ -serversdiv2^post5+serversdiv2^0 == 0), cost: 1 5: l6 -> l0 : __rho_1_^0'=__rho_1_^post6, c^0'=c^post6, curr_serv^0'=curr_serv^post6, resp^0'=resp^post6, servers^0'=servers^post6, serversdiv2^0'=serversdiv2^post6, tmp1^0'=tmp1^post6, (servers^0-servers^post6 == 0 /\ 1-c^0+c^post6 == 0 /\ -1+resp^post6-resp^0 == 0 /\ 1-__rho_1_^0 <= 0 /\ -__rho_1_^post6+__rho_1_^0 == 0 /\ -tmp1^post6+tmp1^0 == 0 /\ 1+curr_serv^post6-curr_serv^0 == 0 /\ serversdiv2^0-serversdiv2^post6 == 0), cost: 1 10: l8 -> l0 : __rho_1_^0'=__rho_1_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 == 0 /\ c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -servers^post9+curr_serv^post9 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ -1+servers^post9-2*serversdiv2^post9 <= 0 /\ 1-servers^post9+2*serversdiv2^post9 <= 0 /\ -tmp1^post9+c^post9 == 0 /\ 1-servers^post9 <= 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ 1-c^post9 <= 0 /\ -__rho_1_^post9+__rho_1_^post10 == 0 /\ servers^0-servers^post10 == 0 /\ resp^post9 == 0), cost: 1 Eliminating location l7 by chaining: Applied chaining First rule: l8 -> l7 : __rho_1_^0'=__rho_1_^post10, c^0'=c^post10, curr_serv^0'=curr_serv^post10, resp^0'=resp^post10, servers^0'=servers^post10, serversdiv2^0'=serversdiv2^post10, tmp1^0'=tmp1^post10, (c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ servers^0-servers^post10 == 0), cost: 1 Second rule: l7 -> l0 : __rho_1_^0'=__rho_1_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 == 0 /\ -__rho_1_^post9+__rho_1_^0 == 0 /\ -servers^post9+curr_serv^post9 == 0 /\ -1+servers^post9-2*serversdiv2^post9 <= 0 /\ 1-servers^post9+2*serversdiv2^post9 <= 0 /\ -tmp1^post9+c^post9 == 0 /\ 1-servers^post9 <= 0 /\ 1-c^post9 <= 0 /\ resp^post9 == 0), cost: 1 New rule: l8 -> l0 : __rho_1_^0'=__rho_1_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 == 0 /\ c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -servers^post9+curr_serv^post9 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ -1+servers^post9-2*serversdiv2^post9 <= 0 /\ 1-servers^post9+2*serversdiv2^post9 <= 0 /\ -tmp1^post9+c^post9 == 0 /\ 1-servers^post9 <= 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ 1-c^post9 <= 0 /\ -__rho_1_^post9+__rho_1_^post10 == 0 /\ servers^0-servers^post10 == 0 /\ resp^post9 == 0), cost: 1 Applied deletion Removed the following rules: 8 9 Eliminating location l5 by chaining: Applied chaining First rule: l4 -> l5 : __rho_1_^0'=__rho_1_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, serversdiv2^0'=serversdiv2^post3, tmp1^0'=tmp1^post3, (-serversdiv2^post3+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post3 == 0 /\ servers^0-servers^post3 == 0 /\ resp^0-resp^post3 == 0 /\ c^0-c^post3 == 0 /\ -curr_serv^post3+curr_serv^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0), cost: 1 Second rule: l5 -> l4 : __rho_1_^0'=__rho_1_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, serversdiv2^0'=serversdiv2^post4, tmp1^0'=tmp1^post4, (resp^0-resp^post4 == 0 /\ -servers^post4+servers^0 == 0 /\ __rho_1_^0-__rho_1_^post4 == 0 /\ -curr_serv^post4+curr_serv^0 == 0 /\ tmp1^0-tmp1^post4 == 0 /\ -c^post4+c^0 == 0 /\ -serversdiv2^post4+serversdiv2^0 == 0), cost: 1 New rule: l4 -> l4 : __rho_1_^0'=__rho_1_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, serversdiv2^0'=serversdiv2^post4, tmp1^0'=tmp1^post4, (-serversdiv2^post3+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post3 == 0 /\ resp^post3-resp^post4 == 0 /\ servers^0-servers^post3 == 0 /\ resp^0-resp^post3 == 0 /\ __rho_1_^post3-__rho_1_^post4 == 0 /\ serversdiv2^post3-serversdiv2^post4 == 0 /\ c^0-c^post3 == 0 /\ -c^post4+c^post3 == 0 /\ curr_serv^post3-curr_serv^post4 == 0 /\ -servers^post4+servers^post3 == 0 /\ tmp1^post3-tmp1^post4 == 0 /\ -curr_serv^post3+curr_serv^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0), cost: 1 Applied deletion Removed the following rules: 2 3 Simplified Transitions Start location: l8 Program variables: __rho_1_^0 c^0 curr_serv^0 resp^0 servers^0 serversdiv2^0 tmp1^0 12: l0 -> l1 : T, cost: 1 16: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1 17: l1 -> l4 : curr_serv^0 <= 0, cost: 1 13: l2 -> l3 : T, cost: 1 19: l4 -> l4 : T, cost: 1 14: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 15: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1 18: l8 -> l0 : c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 Propagated Equalities Original rule: l0 -> l1 : __rho_1_^0'=__rho_1_^post1, c^0'=c^post1, curr_serv^0'=curr_serv^post1, resp^0'=resp^post1, servers^0'=servers^post1, serversdiv2^0'=serversdiv2^post1, tmp1^0'=tmp1^post1, (c^0-c^post1 == 0 /\ -resp^post1+resp^0 == 0 /\ serversdiv2^0-serversdiv2^post1 == 0 /\ servers^0-servers^post1 == 0 /\ -curr_serv^post1+curr_serv^0 == 0 /\ -__rho_1_^post1+__rho_1_^0 == 0 /\ -tmp1^post1+tmp1^0 == 0), cost: 1 New rule: l0 -> l1 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 0 == 0, cost: 1 propagated equality c^post1 = c^0 propagated equality resp^post1 = resp^0 propagated equality serversdiv2^post1 = serversdiv2^0 propagated equality servers^post1 = servers^0 propagated equality curr_serv^post1 = curr_serv^0 propagated equality __rho_1_^post1 = __rho_1_^0 propagated equality tmp1^post1 = tmp1^0 Simplified Guard Original rule: l0 -> l1 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 0 == 0, cost: 1 New rule: l0 -> l1 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : __rho_1_^0'=__rho_1_^post2, c^0'=c^post2, curr_serv^0'=curr_serv^post2, resp^0'=resp^post2, servers^0'=servers^post2, serversdiv2^0'=serversdiv2^post2, tmp1^0'=tmp1^post2, (-serversdiv2^post2+serversdiv2^0 == 0 /\ -__rho_1_^post2+__rho_1_^0 == 0 /\ -resp^post2+resp^0 == 0 /\ -curr_serv^post2+curr_serv^0 == 0 /\ tmp1^0-tmp1^post2 == 0 /\ servers^0-servers^post2 == 0 /\ c^0-c^post2 == 0), cost: 1 New rule: l2 -> l3 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 0 == 0, cost: 1 propagated equality serversdiv2^post2 = serversdiv2^0 propagated equality __rho_1_^post2 = __rho_1_^0 propagated equality resp^post2 = resp^0 propagated equality curr_serv^post2 = curr_serv^0 propagated equality tmp1^post2 = tmp1^0 propagated equality servers^post2 = servers^0 propagated equality c^post2 = c^0 Simplified Guard Original rule: l2 -> l3 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 0 == 0, cost: 1 New rule: l2 -> l3 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, T, cost: 1 New rule: l2 -> l3 : T, cost: 1 Propagated Equalities Original rule: l6 -> l0 : __rho_1_^0'=__rho_1_^post5, c^0'=c^post5, curr_serv^0'=curr_serv^post5, resp^0'=resp^post5, servers^0'=servers^post5, serversdiv2^0'=serversdiv2^post5, tmp1^0'=tmp1^post5, (__rho_1_^0-__rho_1_^post5 == 0 /\ tmp1^0-tmp1^post5 == 0 /\ 1+curr_serv^post5-curr_serv^0 == 0 /\ servers^0-servers^post5 == 0 /\ resp^0-resp^post5 == 0 /\ 1+c^0-curr_serv^0 <= 0 /\ -c^post5+c^0 == 0 /\ __rho_1_^0 <= 0 /\ -serversdiv2^post5+serversdiv2^0 == 0), cost: 1 New rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ 1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 propagated equality __rho_1_^post5 = __rho_1_^0 propagated equality tmp1^post5 = tmp1^0 propagated equality curr_serv^post5 = -1+curr_serv^0 propagated equality servers^post5 = servers^0 propagated equality resp^post5 = resp^0 propagated equality c^post5 = c^0 propagated equality serversdiv2^post5 = serversdiv2^0 Simplified Guard Original rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ 1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 New rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 New rule: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 Propagated Equalities Original rule: l6 -> l0 : __rho_1_^0'=__rho_1_^post6, c^0'=c^post6, curr_serv^0'=curr_serv^post6, resp^0'=resp^post6, servers^0'=servers^post6, serversdiv2^0'=serversdiv2^post6, tmp1^0'=tmp1^post6, (servers^0-servers^post6 == 0 /\ 1-c^0+c^post6 == 0 /\ -1+resp^post6-resp^0 == 0 /\ 1-__rho_1_^0 <= 0 /\ -__rho_1_^post6+__rho_1_^0 == 0 /\ -tmp1^post6+tmp1^0 == 0 /\ 1+curr_serv^post6-curr_serv^0 == 0 /\ serversdiv2^0-serversdiv2^post6 == 0), cost: 1 New rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ 1-__rho_1_^0 <= 0), cost: 1 propagated equality servers^post6 = servers^0 propagated equality c^post6 = -1+c^0 propagated equality resp^post6 = 1+resp^0 propagated equality __rho_1_^post6 = __rho_1_^0 propagated equality tmp1^post6 = tmp1^0 propagated equality curr_serv^post6 = -1+curr_serv^0 propagated equality serversdiv2^post6 = serversdiv2^0 Simplified Guard Original rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ 1-__rho_1_^0 <= 0), cost: 1 New rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 1-__rho_1_^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 1-__rho_1_^0 <= 0, cost: 1 New rule: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, c^0'=c^post7, curr_serv^0'=curr_serv^post7, resp^0'=resp^post7, servers^0'=servers^post7, serversdiv2^0'=serversdiv2^post7, tmp1^0'=tmp1^post7, (0 == 0 /\ servers^0-servers^post7 == 0 /\ c^0-c^post7 == 0 /\ -resp^post7+resp^0 == 0 /\ -serversdiv2^post7+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post7 == 0 /\ 1-curr_serv^0 <= 0 /\ -curr_serv^post7+curr_serv^0 == 0), cost: 1 New rule: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ 1-curr_serv^0 <= 0), cost: 1 propagated equality servers^post7 = servers^0 propagated equality c^post7 = c^0 propagated equality resp^post7 = resp^0 propagated equality serversdiv2^post7 = serversdiv2^0 propagated equality tmp1^post7 = tmp1^0 propagated equality curr_serv^post7 = curr_serv^0 Simplified Guard Original rule: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ 1-curr_serv^0 <= 0), cost: 1 New rule: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 1-curr_serv^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 1-curr_serv^0 <= 0, cost: 1 New rule: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l4 : __rho_1_^0'=__rho_1_^post8, c^0'=c^post8, curr_serv^0'=curr_serv^post8, resp^0'=resp^post8, servers^0'=servers^post8, serversdiv2^0'=serversdiv2^post8, tmp1^0'=tmp1^post8, (__rho_1_^0-__rho_1_^post8 == 0 /\ -serversdiv2^post8+serversdiv2^0 == 0 /\ -c^post8+c^0 == 0 /\ tmp1^0-tmp1^post8 == 0 /\ resp^0-resp^post8 == 0 /\ curr_serv^0 <= 0 /\ -servers^post8+servers^0 == 0 /\ -curr_serv^post8+curr_serv^0 == 0), cost: 1 New rule: l1 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ curr_serv^0 <= 0), cost: 1 propagated equality __rho_1_^post8 = __rho_1_^0 propagated equality serversdiv2^post8 = serversdiv2^0 propagated equality c^post8 = c^0 propagated equality tmp1^post8 = tmp1^0 propagated equality resp^post8 = resp^0 propagated equality servers^post8 = servers^0 propagated equality curr_serv^post8 = curr_serv^0 Simplified Guard Original rule: l1 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, (0 == 0 /\ curr_serv^0 <= 0), cost: 1 New rule: l1 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, curr_serv^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, curr_serv^0 <= 0, cost: 1 New rule: l1 -> l4 : curr_serv^0 <= 0, cost: 1 made implied equalities explicit Original rule: l8 -> l0 : __rho_1_^0'=__rho_1_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 == 0 /\ c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -servers^post9+curr_serv^post9 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ -1+servers^post9-2*serversdiv2^post9 <= 0 /\ 1-servers^post9+2*serversdiv2^post9 <= 0 /\ -tmp1^post9+c^post9 == 0 /\ 1-servers^post9 <= 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ 1-c^post9 <= 0 /\ -__rho_1_^post9+__rho_1_^post10 == 0 /\ servers^0-servers^post10 == 0 /\ resp^post9 == 0), cost: 1 New rule: l8 -> l0 : __rho_1_^0'=__rho_1_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 == 0 /\ c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -servers^post9+curr_serv^post9 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ -1+servers^post9-2*serversdiv2^post9 <= 0 /\ -1+servers^post9-2*serversdiv2^post9 == 0 /\ 1-servers^post9+2*serversdiv2^post9 <= 0 /\ -tmp1^post9+c^post9 == 0 /\ 1-servers^post9 <= 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ 1-c^post9 <= 0 /\ -__rho_1_^post9+__rho_1_^post10 == 0 /\ servers^0-servers^post10 == 0 /\ resp^post9 == 0), cost: 1 Propagated Equalities Original rule: l8 -> l0 : __rho_1_^0'=__rho_1_^post9, c^0'=c^post9, curr_serv^0'=curr_serv^post9, resp^0'=resp^post9, servers^0'=servers^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 == 0 /\ c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -servers^post9+curr_serv^post9 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ -1+servers^post9-2*serversdiv2^post9 <= 0 /\ -1+servers^post9-2*serversdiv2^post9 == 0 /\ 1-servers^post9+2*serversdiv2^post9 <= 0 /\ -tmp1^post9+c^post9 == 0 /\ 1-servers^post9 <= 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ 1-c^post9 <= 0 /\ -__rho_1_^post9+__rho_1_^post10 == 0 /\ servers^0-servers^post10 == 0 /\ resp^post9 == 0), cost: 1 New rule: l8 -> l0 : __rho_1_^0'=__rho_1_^post10, c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 <= 0 /\ 0 == 0 /\ 1-tmp1^post9 <= 0 /\ c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ -2*serversdiv2^post9 <= 0 /\ servers^0-servers^post10 == 0), cost: 1 propagated equality curr_serv^post9 = servers^post9 propagated equality servers^post9 = 1+2*serversdiv2^post9 propagated equality c^post9 = tmp1^post9 propagated equality __rho_1_^post9 = __rho_1_^post10 propagated equality resp^post9 = 0 Propagated Equalities Original rule: l8 -> l0 : __rho_1_^0'=__rho_1_^post10, c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 <= 0 /\ 0 == 0 /\ 1-tmp1^post9 <= 0 /\ c^0-c^post10 == 0 /\ curr_serv^0-curr_serv^post10 == 0 /\ -resp^post10+resp^0 == 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -tmp1^post10+tmp1^0 == 0 /\ serversdiv2^0-serversdiv2^post10 == 0 /\ -2*serversdiv2^post9 <= 0 /\ servers^0-servers^post10 == 0), cost: 1 New rule: l8 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 <= 0 /\ 0 == 0 /\ 1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 propagated equality c^post10 = c^0 propagated equality curr_serv^post10 = curr_serv^0 propagated equality resp^post10 = resp^0 propagated equality __rho_1_^post10 = __rho_1_^0 propagated equality tmp1^post10 = tmp1^0 propagated equality serversdiv2^post10 = serversdiv2^0 propagated equality servers^post10 = servers^0 Simplified Guard Original rule: l8 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (0 <= 0 /\ 0 == 0 /\ 1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 New rule: l8 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 Removed Trivial Updates Original rule: l8 -> l0 : __rho_1_^0'=__rho_1_^0, c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 New rule: l8 -> l0 : c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l4 : __rho_1_^0'=__rho_1_^post4, c^0'=c^post4, curr_serv^0'=curr_serv^post4, resp^0'=resp^post4, servers^0'=servers^post4, serversdiv2^0'=serversdiv2^post4, tmp1^0'=tmp1^post4, (-serversdiv2^post3+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post3 == 0 /\ resp^post3-resp^post4 == 0 /\ servers^0-servers^post3 == 0 /\ resp^0-resp^post3 == 0 /\ __rho_1_^post3-__rho_1_^post4 == 0 /\ serversdiv2^post3-serversdiv2^post4 == 0 /\ c^0-c^post3 == 0 /\ -c^post4+c^post3 == 0 /\ curr_serv^post3-curr_serv^post4 == 0 /\ -servers^post4+servers^post3 == 0 /\ tmp1^post3-tmp1^post4 == 0 /\ -curr_serv^post3+curr_serv^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0), cost: 1 New rule: l4 -> l4 : __rho_1_^0'=__rho_1_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, serversdiv2^0'=serversdiv2^post3, tmp1^0'=tmp1^post3, (0 == 0 /\ -serversdiv2^post3+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post3 == 0 /\ servers^0-servers^post3 == 0 /\ resp^0-resp^post3 == 0 /\ c^0-c^post3 == 0 /\ -curr_serv^post3+curr_serv^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0), cost: 1 propagated equality resp^post4 = resp^post3 propagated equality __rho_1_^post4 = __rho_1_^post3 propagated equality serversdiv2^post4 = serversdiv2^post3 propagated equality c^post4 = c^post3 propagated equality curr_serv^post4 = curr_serv^post3 propagated equality servers^post4 = servers^post3 propagated equality tmp1^post4 = tmp1^post3 Propagated Equalities Original rule: l4 -> l4 : __rho_1_^0'=__rho_1_^post3, c^0'=c^post3, curr_serv^0'=curr_serv^post3, resp^0'=resp^post3, servers^0'=servers^post3, serversdiv2^0'=serversdiv2^post3, tmp1^0'=tmp1^post3, (0 == 0 /\ -serversdiv2^post3+serversdiv2^0 == 0 /\ tmp1^0-tmp1^post3 == 0 /\ servers^0-servers^post3 == 0 /\ resp^0-resp^post3 == 0 /\ c^0-c^post3 == 0 /\ -curr_serv^post3+curr_serv^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0), cost: 1 New rule: l4 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 0 == 0, cost: 1 propagated equality serversdiv2^post3 = serversdiv2^0 propagated equality tmp1^post3 = tmp1^0 propagated equality servers^post3 = servers^0 propagated equality resp^post3 = resp^0 propagated equality c^post3 = c^0 propagated equality curr_serv^post3 = curr_serv^0 propagated equality __rho_1_^post3 = __rho_1_^0 Simplified Guard Original rule: l4 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, 0 == 0, cost: 1 New rule: l4 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l4 : __rho_1_^0'=__rho_1_^0, c^0'=c^0, curr_serv^0'=curr_serv^0, resp^0'=resp^0, servers^0'=servers^0, serversdiv2^0'=serversdiv2^0, tmp1^0'=tmp1^0, T, cost: 1 New rule: l4 -> l4 : T, cost: 1 Step with 18 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)] Blocked [{}, {}] Step with 12 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 12[T] Blocked [{}, {}, {}] Step with 16 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 12[T], 16[(1-curr_serv^0 <= 0)] Blocked [{}, {}, {17[T]}, {}] Step with 14 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 12[T], 16[(1-curr_serv^0 <= 0)], 14[(1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0)] Blocked [{}, {}, {17[T]}, {}, {}] Accelerate Start location: l8 Program variables: __rho_1_^0 c^0 curr_serv^0 resp^0 servers^0 serversdiv2^0 tmp1^0 12: l0 -> l1 : T, cost: 1 20: l0 -> l0 : __rho_1_^0'=__rho_1_^post71, curr_serv^0'=-n+curr_serv^0, (-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0), cost: 1 16: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1 17: l1 -> l4 : curr_serv^0 <= 0, cost: 1 13: l2 -> l3 : T, cost: 1 19: l4 -> l4 : T, cost: 1 14: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 15: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1 18: l8 -> l0 : c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 Loop Acceleration Original rule: l0 -> l0 : __rho_1_^0'=__rho_1_^post71, curr_serv^0'=-1+curr_serv^0, (__rho_1_^post71 <= 0 /\ 1+c^0-curr_serv^0 <= 0 /\ 1-curr_serv^0 <= 0), cost: 1 New rule: l0 -> l0 : __rho_1_^0'=__rho_1_^post71, curr_serv^0'=-n+curr_serv^0, (-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0), cost: 1 -1-c^0+curr_serv^0 >= 0 [0]: montonic decrease yields -c^0-n+curr_serv^0 >= 0 -1-c^0+curr_serv^0 >= 0 [1]: eventual increase yields (-1-c^0+curr_serv^0 >= 0 /\ 1 <= 0) -1+curr_serv^0 >= 0 [0]: montonic decrease yields -n+curr_serv^0 >= 0 -1+curr_serv^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+curr_serv^0 >= 0) -__rho_1_^post71 >= 0 [0]: monotonic increase yields -__rho_1_^post71 >= 0 Replacement map: {-1-c^0+curr_serv^0 >= 0 -> -c^0-n+curr_serv^0 >= 0, -1+curr_serv^0 >= 0 -> -n+curr_serv^0 >= 0, -__rho_1_^post71 >= 0 -> -__rho_1_^post71 >= 0} Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 20[(-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0)] Blocked [{}, {}, {20[T]}] Step with 12 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 20[(-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0)], 12[T] Blocked [{}, {}, {20[T]}, {}] Step with 16 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 20[(-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {}] Step with 14 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 20[(-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)], 14[(1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {}, {}] Covered Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 20[(-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {14[T]}] Step with 15 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 20[(-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)], 15[(1-__rho_1_^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {14[T]}, {}] Accelerate Start location: l8 Program variables: __rho_1_^0 c^0 curr_serv^0 resp^0 servers^0 serversdiv2^0 tmp1^0 12: l0 -> l1 : T, cost: 1 20: l0 -> l0 : __rho_1_^0'=__rho_1_^post71, curr_serv^0'=-n+curr_serv^0, (-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0), cost: 1 21: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n2, curr_serv^0'=-n2+curr_serv^0, resp^0'=n2+resp^0, (-1+__rho_1_^post72 >= 0 /\ -n2+curr_serv^0 >= 0 /\ -1+n2 >= 0), cost: 1 16: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1 17: l1 -> l4 : curr_serv^0 <= 0, cost: 1 13: l2 -> l3 : T, cost: 1 19: l4 -> l4 : T, cost: 1 14: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 15: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1 18: l8 -> l0 : c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 Loop Acceleration Original rule: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, (1-__rho_1_^post72 <= 0 /\ 1-curr_serv^0 <= 0), cost: 1 New rule: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n2, curr_serv^0'=-n2+curr_serv^0, resp^0'=n2+resp^0, (-1+__rho_1_^post72 >= 0 /\ -n2+curr_serv^0 >= 0 /\ -1+n2 >= 0), cost: 1 -1+__rho_1_^post72 >= 0 [0]: monotonic increase yields -1+__rho_1_^post72 >= 0 -1+curr_serv^0 >= 0 [0]: montonic decrease yields -n2+curr_serv^0 >= 0 -1+curr_serv^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+curr_serv^0 >= 0) Replacement map: {-1+__rho_1_^post72 >= 0 -> -1+__rho_1_^post72 >= 0, -1+curr_serv^0 >= 0 -> -n2+curr_serv^0 >= 0} Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 20[(-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0)], 21[(-1+__rho_1_^post72 >= 0 /\ -n2+curr_serv^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {20[T]}, {21[T]}] Accelerate Start location: l8 Program variables: __rho_1_^0 c^0 curr_serv^0 resp^0 servers^0 serversdiv2^0 tmp1^0 12: l0 -> l1 : T, cost: 1 20: l0 -> l0 : __rho_1_^0'=__rho_1_^post71, curr_serv^0'=-n+curr_serv^0, (-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0), cost: 1 21: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n2, curr_serv^0'=-n2+curr_serv^0, resp^0'=n2+resp^0, (-1+__rho_1_^post72 >= 0 /\ -n2+curr_serv^0 >= 0 /\ -1+n2 >= 0), cost: 1 22: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n3*n2, curr_serv^0'=-n3*n1-n3*n2+curr_serv^0, resp^0'=resp^0+n3*n2, (-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0), cost: 1 16: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1 17: l1 -> l4 : curr_serv^0 <= 0, cost: 1 13: l2 -> l3 : T, cost: 1 19: l4 -> l4 : T, cost: 1 14: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 15: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1 18: l8 -> l0 : c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 Loop Acceleration Original rule: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n2, curr_serv^0'=-n1-n2+curr_serv^0, resp^0'=n2+resp^0, (-1+__rho_1_^post72 >= 0 /\ -n1-c^0+curr_serv^0 >= 0 /\ -1+n1 >= 0 /\ -n1-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -n1+curr_serv^0 >= 0), cost: 1 New rule: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n3*n2, curr_serv^0'=-n3*n1-n3*n2+curr_serv^0, resp^0'=resp^0+n3*n2, (-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0), cost: 1 -1+__rho_1_^post72 >= 0 [0]: monotonic increase yields -1+__rho_1_^post72 >= 0 -n1-c^0+curr_serv^0 >= 0 [0]: montonic decrease yields -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0, dependencies: -1+n1 >= 0 -n1-c^0+curr_serv^0 >= 0 [1]: eventual decrease yields (-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0) -n1-c^0+curr_serv^0 >= 0 [2]: eventual increase yields (-n1-c^0+curr_serv^0 >= 0 /\ n1 <= 0) -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -n1-n2+curr_serv^0 >= 0 [0]: montonic decrease yields -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 -n1-n2+curr_serv^0 >= 0 [1]: eventual decrease yields (-(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -n1-n2+curr_serv^0 >= 0) -n1-n2+curr_serv^0 >= 0 [2]: eventual increase yields (n1+n2 <= 0 /\ -n1-n2+curr_serv^0 >= 0) -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 -n1+curr_serv^0 >= 0 [0]: montonic decrease yields -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 -n1+curr_serv^0 >= 0 [1]: eventual increase yields (n1+n2 <= 0 /\ -n1+curr_serv^0 >= 0) Replacement map: {-1+__rho_1_^post72 >= 0 -> -1+__rho_1_^post72 >= 0, -n1-c^0+curr_serv^0 >= 0 -> -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0, -1+n1 >= 0 -> -1+n1 >= 0, -n1-n2+curr_serv^0 >= 0 -> -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0, -1+n2 >= 0 -> -1+n2 >= 0, -n1+curr_serv^0 >= 0 -> -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0} Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)] Blocked [{}, {}, {22[T]}] Step with 12 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T] Blocked [{}, {}, {22[T]}, {}] Step with 16 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)] Blocked [{}, {}, {22[T]}, {}, {}] Step with 15 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)], 15[(1-__rho_1_^0 <= 0)] Blocked [{}, {}, {22[T]}, {}, {}, {}] Covered Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)] Blocked [{}, {}, {22[T]}, {}, {15[T]}] Step with 14 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)], 14[(1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0)] Blocked [{}, {}, {22[T]}, {}, {15[T]}, {}] Covered Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 16[(1-curr_serv^0 <= 0)] Blocked [{}, {}, {22[T]}, {}, {14[T], 15[T]}] Backtrack Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T] Blocked [{}, {}, {22[T]}, {16[T]}] Step with 17 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 17[(curr_serv^0 <= 0)] Blocked [{}, {}, {22[T]}, {16[T]}, {}] Step with 19 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 17[(curr_serv^0 <= 0)], 19[T] Blocked [{}, {}, {22[T]}, {16[T]}, {}, {}] Nonterm Start location: l8 Program variables: __rho_1_^0 c^0 curr_serv^0 resp^0 servers^0 serversdiv2^0 tmp1^0 12: l0 -> l1 : T, cost: 1 20: l0 -> l0 : __rho_1_^0'=__rho_1_^post71, curr_serv^0'=-n+curr_serv^0, (-n+curr_serv^0 >= 0 /\ -c^0-n+curr_serv^0 >= 0 /\ -1+n >= 0 /\ -__rho_1_^post71 >= 0), cost: 1 21: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n2, curr_serv^0'=-n2+curr_serv^0, resp^0'=n2+resp^0, (-1+__rho_1_^post72 >= 0 /\ -n2+curr_serv^0 >= 0 /\ -1+n2 >= 0), cost: 1 22: l0 -> l0 : __rho_1_^0'=__rho_1_^post72, c^0'=c^0-n3*n2, curr_serv^0'=-n3*n1-n3*n2+curr_serv^0, resp^0'=resp^0+n3*n2, (-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0), cost: 1 16: l1 -> l6 : __rho_1_^0'=__rho_1_^post7, 1-curr_serv^0 <= 0, cost: 1 17: l1 -> l4 : curr_serv^0 <= 0, cost: 1 13: l2 -> l3 : T, cost: 1 19: l4 -> l4 : T, cost: 1 23: l4 -> LoAT_sink : -1+n4 >= 0, cost: NONTERM 14: l6 -> l0 : curr_serv^0'=-1+curr_serv^0, (1+c^0-curr_serv^0 <= 0 /\ __rho_1_^0 <= 0), cost: 1 15: l6 -> l0 : c^0'=-1+c^0, curr_serv^0'=-1+curr_serv^0, resp^0'=1+resp^0, 1-__rho_1_^0 <= 0, cost: 1 18: l8 -> l0 : c^0'=tmp1^post9, curr_serv^0'=1+2*serversdiv2^post9, resp^0'=0, servers^0'=1+2*serversdiv2^post9, serversdiv2^0'=serversdiv2^post9, tmp1^0'=tmp1^post9, (1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0), cost: 1 Certificate of Non-Termination Original rule: l4 -> l4 : T, cost: 1 New rule: l4 -> LoAT_sink : -1+n4 >= 0, cost: NONTERM Replacement map: {} Step with 23 Trace 18[(1-tmp1^post9 <= 0 /\ -2*serversdiv2^post9 <= 0)], 22[(-1+__rho_1_^post72 >= 0 /\ -1+n3 >= 0 /\ -1+n1 >= 0 /\ -(-1+n3)*n1-n1-c^0+curr_serv^0 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2-n2+curr_serv^0 >= 0 /\ -1+n2 >= 0 /\ -(-1+n3)*n1-n1-(-1+n3)*n2+curr_serv^0 >= 0)], 12[T], 17[(curr_serv^0 <= 0)], 23[-1+n4 >= 0] Blocked [{}, {}, {22[T]}, {16[T]}, {}, {23[T]}] Refute Counterexample [ __rho_1_^0=0 c^0=1 curr_serv^0=3 resp^0=0 servers^0=3 serversdiv2^0=1 tmp1^0=1 ] 18 [ __rho_1_^0=1 c^0=-1 curr_serv^0=0 resp^0=2 servers^0=3 serversdiv2^0=1 tmp1^0=1 ] 22 [ __rho_1_^0=1 c^0=-1 curr_serv^0=0 resp^0=2 servers^0=3 serversdiv2^0=1 tmp1^0=1 ] 12 [ __rho_1_^0=1 c^0=-1 curr_serv^0=0 resp^0=2 servers^0=3 serversdiv2^0=1 tmp1^0=1 ] 17 [ __rho_1_^0=0 c^0=c^0 curr_serv^0=curr_serv^0 resp^0=resp^0 servers^0=servers^0 serversdiv2^0=serversdiv2^0 tmp1^0=tmp1^0 ] 23 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b