NO Initial ITS Start location: l6 Program variables: conditional^0 critical^0 increase^0 j_min^0 max^0 max_min^0 min^0 noncritical^0 num^0 num_min^0 p^0 pid^0 q^0 0: l0 -> l1 : conditional^0'=conditional^post1, critical^0'=critical^post1, increase^0'=increase^post1, j_min^0'=j_min^post1, max^0'=max^post1, max_min^0'=max_min^post1, min^0'=min^post1, noncritical^0'=noncritical^post1, num^0'=num^post1, num_min^0'=num_min^post1, p^0'=p^post1, pid^0'=pid^post1, q^0'=q^post1, (0 == 0 /\ -j_min^post1+j_min^0 == 0 /\ -max^post1+max^0 == 0 /\ -p^post1+p^0 == 0 /\ -noncritical^post1+noncritical^0 == 0 /\ -1+conditional^0 <= 0 /\ q^0-q^post1 == 0 /\ pid^0-pid^post1 == 0 /\ -increase^post1+increase^0 == 0 /\ critical^0-critical^post1 == 0 /\ num_min^0-num_min^post1 == 0 /\ min^0-min^post1 == 0 /\ max_min^0-max_min^post1 == 0 /\ -num^post1+num^0 == 0), cost: 1 1: l0 -> l1 : conditional^0'=conditional^post2, critical^0'=critical^post2, increase^0'=increase^post2, j_min^0'=j_min^post2, max^0'=max^post2, max_min^0'=max_min^post2, min^0'=min^post2, noncritical^0'=noncritical^post2, num^0'=num^post2, num_min^0'=num_min^post2, p^0'=p^post2, pid^0'=pid^post2, q^0'=q^post2, (0 == 0 /\ num^0-num^post2 == 0 /\ 2-conditional^0 <= 0 /\ -max^post2+max^0 == 0 /\ 1-increase^post2 <= 0 /\ -increase^post2+j_min^post2-j_min^0 == 0 /\ min^0-min^post2 == 0 /\ max_min^0-max_min^post2 == 0 /\ q^0-q^post2 == 0 /\ -p^post2+p^0 == 0 /\ pid^0-pid^post2 == 0 /\ num_min^0-num_min^post2 == 0 /\ -noncritical^post2+noncritical^0 == 0 /\ critical^0-critical^post2 == 0), cost: 1 6: l1 -> l3 : conditional^0'=conditional^post7, critical^0'=critical^post7, increase^0'=increase^post7, j_min^0'=j_min^post7, max^0'=max^post7, max_min^0'=max_min^post7, min^0'=min^post7, noncritical^0'=noncritical^post7, num^0'=num^post7, num_min^0'=num_min^post7, p^0'=p^post7, pid^0'=pid^post7, q^0'=q^post7, (0 == 0 /\ p^0-p^post7 == 0 /\ -pid^post7+pid^0 == 0 /\ 1-pid^0+j_min^0 <= 0 /\ -j_min^post7+j_min^0 == 0 /\ -increase^post7+increase^0 == 0 /\ noncritical^0-noncritical^post7 == 0 /\ max_min^0-max_min^post7 == 0 /\ -num^post7+num^0 == 0 /\ max^0-max^post7 == 0 /\ -min^post7+min^0 == 0 /\ q^0-q^post7 == 0 /\ num_min^0-num_min^post7 == 0 /\ -num^0+min^0 <= 0 /\ critical^0-critical^post7 == 0), cost: 1 7: l1 -> l4 : conditional^0'=conditional^post8, critical^0'=critical^post8, increase^0'=increase^post8, j_min^0'=j_min^post8, max^0'=max^post8, max_min^0'=max_min^post8, min^0'=min^post8, noncritical^0'=noncritical^post8, num^0'=num^post8, num_min^0'=num_min^post8, p^0'=p^post8, pid^0'=pid^post8, q^0'=q^post8, (-1+critical^post8 == 0 /\ p^post8 == 0 /\ -noncritical^post8+noncritical^0 == 0 /\ pid^0-j_min^0 <= 0 /\ pid^0-pid^post8 == 0 /\ max_min^0-max_min^post8 == 0 /\ -min^post8+min^0 == 0 /\ num_min^0-num_min^post8 == 0 /\ max^0-max^post8 == 0 /\ conditional^0-conditional^post8 == 0 /\ -j_min^post8+j_min^0 == 0 /\ q^post8 == 0 /\ -increase^post8+increase^0 == 0 /\ -num^post8+num^0 == 0), cost: 1 8: l1 -> l4 : conditional^0'=conditional^post9, critical^0'=critical^post9, increase^0'=increase^post9, j_min^0'=j_min^post9, max^0'=max^post9, max_min^0'=max_min^post9, min^0'=min^post9, noncritical^0'=noncritical^post9, num^0'=num^post9, num_min^0'=num_min^post9, p^0'=p^post9, pid^0'=pid^post9, q^0'=q^post9, (-num^post9+num^0 == 0 /\ -noncritical^post9+noncritical^0 == 0 /\ -max^post9+max^0 == 0 /\ p^post9 == 0 /\ j_min^0-j_min^post9 == 0 /\ -increase^post9+increase^0 == 0 /\ -conditional^post9+conditional^0 == 0 /\ min^0-min^post9 == 0 /\ 1+num^0-min^0 <= 0 /\ num_min^0-num_min^post9 == 0 /\ pid^0-pid^post9 == 0 /\ -1+critical^post9 == 0 /\ max_min^0-max_min^post9 == 0 /\ q^post9 == 0), cost: 1 2: l2 -> l0 : conditional^0'=conditional^post3, critical^0'=critical^post3, increase^0'=increase^post3, j_min^0'=j_min^post3, max^0'=max^post3, max_min^0'=max_min^post3, min^0'=min^post3, noncritical^0'=noncritical^post3, num^0'=num^post3, num_min^0'=num_min^post3, p^0'=p^post3, pid^0'=pid^post3, q^0'=q^post3, (0 == 0 /\ -1+p^post3 == 0 /\ -q^post3+q^0 == 0 /\ -1+conditional^0 <= 0 /\ pid^0-pid^post3 == 0 /\ num_min^0-num_min^post3 == 0 /\ -j_min^post3+j_min^0 == 0 /\ max_min^0-max_min^post3 == 0 /\ -min^post3+min^0 == 0 /\ -noncritical^post3+noncritical^0 == 0 /\ -max^post3+max^0 == 0 /\ critical^0-critical^post3 == 0 /\ num^0-num^post3 == 0 /\ -increase^post3+increase^0 == 0), cost: 1 3: l2 -> l1 : conditional^0'=conditional^post4, critical^0'=critical^post4, increase^0'=increase^post4, j_min^0'=j_min^post4, max^0'=max^post4, max_min^0'=max_min^post4, min^0'=min^post4, noncritical^0'=noncritical^post4, num^0'=num^post4, num_min^0'=num_min^post4, p^0'=p^post4, pid^0'=pid^post4, q^0'=q^post4, (0 == 0 /\ max^0-max^post4 == 0 /\ 2-conditional^0 <= 0 /\ max_min^post4-max^0+min^0 == 0 /\ -p^post4+p^0 == 0 /\ increase^post4-max^0+min^0 <= 0 /\ num_min^post4-num^0+min^0 == 0 /\ -pid^post4+pid^0 == 0 /\ -increase^post4+min^post4-min^0 == 0 /\ increase^post4-num_min^post4 <= 0 /\ -increase^post4+num^0 <= 0 /\ -1+q^post4 == 0 /\ noncritical^0-noncritical^post4 == 0 /\ num^0-num^post4 == 0 /\ critical^0-critical^post4 == 0 /\ 1-j_min^post4 <= 0), cost: 1 4: l3 -> l2 : conditional^0'=conditional^post5, critical^0'=critical^post5, increase^0'=increase^post5, j_min^0'=j_min^post5, max^0'=max^post5, max_min^0'=max_min^post5, min^0'=min^post5, noncritical^0'=noncritical^post5, num^0'=num^post5, num_min^0'=num_min^post5, p^0'=p^post5, pid^0'=pid^post5, q^0'=q^post5, (0 == 0 /\ -min^post5+min^0 == 0 /\ -1+conditional^0 <= 0 /\ -pid^post5+pid^0 == 0 /\ noncritical^0-noncritical^post5 == 0 /\ -num^post5+num^0 == 0 /\ -j_min^post5+j_min^0 == 0 /\ critical^0-critical^post5 == 0 /\ max_min^0-max_min^post5 == 0 /\ q^0-q^post5 == 0 /\ max^0-max^post5 == 0 /\ num_min^0-num_min^post5 == 0 /\ p^0-p^post5 == 0 /\ -increase^post5+increase^0 == 0), cost: 1 5: l3 -> l2 : conditional^0'=conditional^post6, critical^0'=critical^post6, increase^0'=increase^post6, j_min^0'=j_min^post6, max^0'=max^post6, max_min^0'=max_min^post6, min^0'=min^post6, noncritical^0'=noncritical^post6, num^0'=num^post6, num_min^0'=num_min^post6, p^0'=p^post6, pid^0'=pid^post6, q^0'=q^post6, (0 == 0 /\ -increase^post6-max^0+max^post6 == 0 /\ -num^post6+num^0 == 0 /\ 2-conditional^0 <= 0 /\ -j_min^post6+j_min^0 == 0 /\ -max_min^post6+max_min^0 == 0 /\ -min^post6+min^0 == 0 /\ pid^0-pid^post6 == 0 /\ 1-increase^post6 <= 0 /\ noncritical^0-noncritical^post6 == 0 /\ -q^post6+q^0 == 0 /\ num_min^0-num_min^post6 == 0 /\ -p^post6+p^0 == 0 /\ critical^0-critical^post6 == 0), cost: 1 9: l4 -> l1 : conditional^0'=conditional^post10, critical^0'=critical^post10, increase^0'=increase^post10, j_min^0'=j_min^post10, max^0'=max^post10, max_min^0'=max_min^post10, min^0'=min^post10, noncritical^0'=noncritical^post10, num^0'=num^post10, num_min^0'=num_min^post10, p^0'=p^post10, pid^0'=pid^post10, q^0'=q^post10, (-1+max^post10-max^0 == 0 /\ -p^post10+p^0 == 0 /\ critical^post10 == 0 /\ pid^0-pid^post10 == 0 /\ max_min^0-max_min^post10 == 0 /\ -1-max^0+num^post10 == 0 /\ -1+noncritical^post10 == 0 /\ -j_min^post10+j_min^0 == 0 /\ -min^post10+min^0 == 0 /\ -conditional^post10+conditional^0 == 0 /\ q^0-q^post10 == 0 /\ -increase^post10+increase^0 == 0 /\ num_min^0-num_min^post10 == 0), cost: 1 10: l5 -> l4 : conditional^0'=conditional^post11, critical^0'=critical^post11, increase^0'=increase^post11, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^post11, min^0'=min^post11, noncritical^0'=noncritical^post11, num^0'=num^post11, num_min^0'=num_min^post11, p^0'=p^post11, pid^0'=pid^post11, q^0'=q^post11, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -conditional^post11+conditional^0 == 0 /\ p^post11 == 0 /\ -num^post11+num^0 == 0 /\ -increase^post11+increase^0 == 0 /\ critical^post11 == 0 /\ -1+noncritical^post11 == 0 /\ num_min^0-num_min^post11 == 0 /\ -max^post11+min^post11 <= 0 /\ q^post11 == 0 /\ max_min^0-max_min^post11 == 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 11: l6 -> l5 : conditional^0'=conditional^post12, critical^0'=critical^post12, increase^0'=increase^post12, j_min^0'=j_min^post12, max^0'=max^post12, max_min^0'=max_min^post12, min^0'=min^post12, noncritical^0'=noncritical^post12, num^0'=num^post12, num_min^0'=num_min^post12, p^0'=p^post12, pid^0'=pid^post12, q^0'=q^post12, (-conditional^post12+conditional^0 == 0 /\ -increase^post12+increase^0 == 0 /\ -j_min^post12+j_min^0 == 0 /\ -p^post12+p^0 == 0 /\ num^0-num^post12 == 0 /\ max_min^0-max_min^post12 == 0 /\ critical^0-critical^post12 == 0 /\ -min^post12+min^0 == 0 /\ pid^0-pid^post12 == 0 /\ -noncritical^post12+noncritical^0 == 0 /\ q^0-q^post12 == 0 /\ -max^post12+max^0 == 0 /\ num_min^0-num_min^post12 == 0), cost: 1 Chained Linear Paths Start location: l6 Program variables: conditional^0 critical^0 increase^0 j_min^0 max^0 max_min^0 min^0 noncritical^0 num^0 num_min^0 p^0 pid^0 q^0 0: l0 -> l1 : conditional^0'=conditional^post1, critical^0'=critical^post1, increase^0'=increase^post1, j_min^0'=j_min^post1, max^0'=max^post1, max_min^0'=max_min^post1, min^0'=min^post1, noncritical^0'=noncritical^post1, num^0'=num^post1, num_min^0'=num_min^post1, p^0'=p^post1, pid^0'=pid^post1, q^0'=q^post1, (0 == 0 /\ -j_min^post1+j_min^0 == 0 /\ -max^post1+max^0 == 0 /\ -p^post1+p^0 == 0 /\ -noncritical^post1+noncritical^0 == 0 /\ -1+conditional^0 <= 0 /\ q^0-q^post1 == 0 /\ pid^0-pid^post1 == 0 /\ -increase^post1+increase^0 == 0 /\ critical^0-critical^post1 == 0 /\ num_min^0-num_min^post1 == 0 /\ min^0-min^post1 == 0 /\ max_min^0-max_min^post1 == 0 /\ -num^post1+num^0 == 0), cost: 1 1: l0 -> l1 : conditional^0'=conditional^post2, critical^0'=critical^post2, increase^0'=increase^post2, j_min^0'=j_min^post2, max^0'=max^post2, max_min^0'=max_min^post2, min^0'=min^post2, noncritical^0'=noncritical^post2, num^0'=num^post2, num_min^0'=num_min^post2, p^0'=p^post2, pid^0'=pid^post2, q^0'=q^post2, (0 == 0 /\ num^0-num^post2 == 0 /\ 2-conditional^0 <= 0 /\ -max^post2+max^0 == 0 /\ 1-increase^post2 <= 0 /\ -increase^post2+j_min^post2-j_min^0 == 0 /\ min^0-min^post2 == 0 /\ max_min^0-max_min^post2 == 0 /\ q^0-q^post2 == 0 /\ -p^post2+p^0 == 0 /\ pid^0-pid^post2 == 0 /\ num_min^0-num_min^post2 == 0 /\ -noncritical^post2+noncritical^0 == 0 /\ critical^0-critical^post2 == 0), cost: 1 6: l1 -> l3 : conditional^0'=conditional^post7, critical^0'=critical^post7, increase^0'=increase^post7, j_min^0'=j_min^post7, max^0'=max^post7, max_min^0'=max_min^post7, min^0'=min^post7, noncritical^0'=noncritical^post7, num^0'=num^post7, num_min^0'=num_min^post7, p^0'=p^post7, pid^0'=pid^post7, q^0'=q^post7, (0 == 0 /\ p^0-p^post7 == 0 /\ -pid^post7+pid^0 == 0 /\ 1-pid^0+j_min^0 <= 0 /\ -j_min^post7+j_min^0 == 0 /\ -increase^post7+increase^0 == 0 /\ noncritical^0-noncritical^post7 == 0 /\ max_min^0-max_min^post7 == 0 /\ -num^post7+num^0 == 0 /\ max^0-max^post7 == 0 /\ -min^post7+min^0 == 0 /\ q^0-q^post7 == 0 /\ num_min^0-num_min^post7 == 0 /\ -num^0+min^0 <= 0 /\ critical^0-critical^post7 == 0), cost: 1 7: l1 -> l4 : conditional^0'=conditional^post8, critical^0'=critical^post8, increase^0'=increase^post8, j_min^0'=j_min^post8, max^0'=max^post8, max_min^0'=max_min^post8, min^0'=min^post8, noncritical^0'=noncritical^post8, num^0'=num^post8, num_min^0'=num_min^post8, p^0'=p^post8, pid^0'=pid^post8, q^0'=q^post8, (-1+critical^post8 == 0 /\ p^post8 == 0 /\ -noncritical^post8+noncritical^0 == 0 /\ pid^0-j_min^0 <= 0 /\ pid^0-pid^post8 == 0 /\ max_min^0-max_min^post8 == 0 /\ -min^post8+min^0 == 0 /\ num_min^0-num_min^post8 == 0 /\ max^0-max^post8 == 0 /\ conditional^0-conditional^post8 == 0 /\ -j_min^post8+j_min^0 == 0 /\ q^post8 == 0 /\ -increase^post8+increase^0 == 0 /\ -num^post8+num^0 == 0), cost: 1 8: l1 -> l4 : conditional^0'=conditional^post9, critical^0'=critical^post9, increase^0'=increase^post9, j_min^0'=j_min^post9, max^0'=max^post9, max_min^0'=max_min^post9, min^0'=min^post9, noncritical^0'=noncritical^post9, num^0'=num^post9, num_min^0'=num_min^post9, p^0'=p^post9, pid^0'=pid^post9, q^0'=q^post9, (-num^post9+num^0 == 0 /\ -noncritical^post9+noncritical^0 == 0 /\ -max^post9+max^0 == 0 /\ p^post9 == 0 /\ j_min^0-j_min^post9 == 0 /\ -increase^post9+increase^0 == 0 /\ -conditional^post9+conditional^0 == 0 /\ min^0-min^post9 == 0 /\ 1+num^0-min^0 <= 0 /\ num_min^0-num_min^post9 == 0 /\ pid^0-pid^post9 == 0 /\ -1+critical^post9 == 0 /\ max_min^0-max_min^post9 == 0 /\ q^post9 == 0), cost: 1 2: l2 -> l0 : conditional^0'=conditional^post3, critical^0'=critical^post3, increase^0'=increase^post3, j_min^0'=j_min^post3, max^0'=max^post3, max_min^0'=max_min^post3, min^0'=min^post3, noncritical^0'=noncritical^post3, num^0'=num^post3, num_min^0'=num_min^post3, p^0'=p^post3, pid^0'=pid^post3, q^0'=q^post3, (0 == 0 /\ -1+p^post3 == 0 /\ -q^post3+q^0 == 0 /\ -1+conditional^0 <= 0 /\ pid^0-pid^post3 == 0 /\ num_min^0-num_min^post3 == 0 /\ -j_min^post3+j_min^0 == 0 /\ max_min^0-max_min^post3 == 0 /\ -min^post3+min^0 == 0 /\ -noncritical^post3+noncritical^0 == 0 /\ -max^post3+max^0 == 0 /\ critical^0-critical^post3 == 0 /\ num^0-num^post3 == 0 /\ -increase^post3+increase^0 == 0), cost: 1 3: l2 -> l1 : conditional^0'=conditional^post4, critical^0'=critical^post4, increase^0'=increase^post4, j_min^0'=j_min^post4, max^0'=max^post4, max_min^0'=max_min^post4, min^0'=min^post4, noncritical^0'=noncritical^post4, num^0'=num^post4, num_min^0'=num_min^post4, p^0'=p^post4, pid^0'=pid^post4, q^0'=q^post4, (0 == 0 /\ max^0-max^post4 == 0 /\ 2-conditional^0 <= 0 /\ max_min^post4-max^0+min^0 == 0 /\ -p^post4+p^0 == 0 /\ increase^post4-max^0+min^0 <= 0 /\ num_min^post4-num^0+min^0 == 0 /\ -pid^post4+pid^0 == 0 /\ -increase^post4+min^post4-min^0 == 0 /\ increase^post4-num_min^post4 <= 0 /\ -increase^post4+num^0 <= 0 /\ -1+q^post4 == 0 /\ noncritical^0-noncritical^post4 == 0 /\ num^0-num^post4 == 0 /\ critical^0-critical^post4 == 0 /\ 1-j_min^post4 <= 0), cost: 1 4: l3 -> l2 : conditional^0'=conditional^post5, critical^0'=critical^post5, increase^0'=increase^post5, j_min^0'=j_min^post5, max^0'=max^post5, max_min^0'=max_min^post5, min^0'=min^post5, noncritical^0'=noncritical^post5, num^0'=num^post5, num_min^0'=num_min^post5, p^0'=p^post5, pid^0'=pid^post5, q^0'=q^post5, (0 == 0 /\ -min^post5+min^0 == 0 /\ -1+conditional^0 <= 0 /\ -pid^post5+pid^0 == 0 /\ noncritical^0-noncritical^post5 == 0 /\ -num^post5+num^0 == 0 /\ -j_min^post5+j_min^0 == 0 /\ critical^0-critical^post5 == 0 /\ max_min^0-max_min^post5 == 0 /\ q^0-q^post5 == 0 /\ max^0-max^post5 == 0 /\ num_min^0-num_min^post5 == 0 /\ p^0-p^post5 == 0 /\ -increase^post5+increase^0 == 0), cost: 1 5: l3 -> l2 : conditional^0'=conditional^post6, critical^0'=critical^post6, increase^0'=increase^post6, j_min^0'=j_min^post6, max^0'=max^post6, max_min^0'=max_min^post6, min^0'=min^post6, noncritical^0'=noncritical^post6, num^0'=num^post6, num_min^0'=num_min^post6, p^0'=p^post6, pid^0'=pid^post6, q^0'=q^post6, (0 == 0 /\ -increase^post6-max^0+max^post6 == 0 /\ -num^post6+num^0 == 0 /\ 2-conditional^0 <= 0 /\ -j_min^post6+j_min^0 == 0 /\ -max_min^post6+max_min^0 == 0 /\ -min^post6+min^0 == 0 /\ pid^0-pid^post6 == 0 /\ 1-increase^post6 <= 0 /\ noncritical^0-noncritical^post6 == 0 /\ -q^post6+q^0 == 0 /\ num_min^0-num_min^post6 == 0 /\ -p^post6+p^0 == 0 /\ critical^0-critical^post6 == 0), cost: 1 9: l4 -> l1 : conditional^0'=conditional^post10, critical^0'=critical^post10, increase^0'=increase^post10, j_min^0'=j_min^post10, max^0'=max^post10, max_min^0'=max_min^post10, min^0'=min^post10, noncritical^0'=noncritical^post10, num^0'=num^post10, num_min^0'=num_min^post10, p^0'=p^post10, pid^0'=pid^post10, q^0'=q^post10, (-1+max^post10-max^0 == 0 /\ -p^post10+p^0 == 0 /\ critical^post10 == 0 /\ pid^0-pid^post10 == 0 /\ max_min^0-max_min^post10 == 0 /\ -1-max^0+num^post10 == 0 /\ -1+noncritical^post10 == 0 /\ -j_min^post10+j_min^0 == 0 /\ -min^post10+min^0 == 0 /\ -conditional^post10+conditional^0 == 0 /\ q^0-q^post10 == 0 /\ -increase^post10+increase^0 == 0 /\ num_min^0-num_min^post10 == 0), cost: 1 12: l6 -> l4 : conditional^0'=conditional^post11, critical^0'=critical^post11, increase^0'=increase^post11, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^post11, min^0'=min^post11, noncritical^0'=noncritical^post11, num^0'=num^post11, num_min^0'=num_min^post11, p^0'=p^post11, pid^0'=pid^post11, q^0'=q^post11, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -conditional^post12+conditional^0 == 0 /\ p^post11 == 0 /\ -increase^post12+increase^0 == 0 /\ -j_min^post12+j_min^0 == 0 /\ -conditional^post11+conditional^post12 == 0 /\ -num^post11+num^post12 == 0 /\ -p^post12+p^0 == 0 /\ critical^post11 == 0 /\ num^0-num^post12 == 0 /\ max_min^0-max_min^post12 == 0 /\ -1+noncritical^post11 == 0 /\ critical^0-critical^post12 == 0 /\ -increase^post11+increase^post12 == 0 /\ -min^post12+min^0 == 0 /\ pid^0-pid^post12 == 0 /\ -noncritical^post12+noncritical^0 == 0 /\ -num_min^post11+num_min^post12 == 0 /\ -max^post11+min^post11 <= 0 /\ q^post11 == 0 /\ q^0-q^post12 == 0 /\ 1-min^post11 <= 0 /\ -max_min^post11+max_min^post12 == 0 /\ -max^post12+max^0 == 0 /\ num_min^0-num_min^post12 == 0 /\ 1-pid^post11 <= 0), cost: 1 Eliminating location l5 by chaining: Applied chaining First rule: l6 -> l5 : conditional^0'=conditional^post12, critical^0'=critical^post12, increase^0'=increase^post12, j_min^0'=j_min^post12, max^0'=max^post12, max_min^0'=max_min^post12, min^0'=min^post12, noncritical^0'=noncritical^post12, num^0'=num^post12, num_min^0'=num_min^post12, p^0'=p^post12, pid^0'=pid^post12, q^0'=q^post12, (-conditional^post12+conditional^0 == 0 /\ -increase^post12+increase^0 == 0 /\ -j_min^post12+j_min^0 == 0 /\ -p^post12+p^0 == 0 /\ num^0-num^post12 == 0 /\ max_min^0-max_min^post12 == 0 /\ critical^0-critical^post12 == 0 /\ -min^post12+min^0 == 0 /\ pid^0-pid^post12 == 0 /\ -noncritical^post12+noncritical^0 == 0 /\ q^0-q^post12 == 0 /\ -max^post12+max^0 == 0 /\ num_min^0-num_min^post12 == 0), cost: 1 Second rule: l5 -> l4 : conditional^0'=conditional^post11, critical^0'=critical^post11, increase^0'=increase^post11, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^post11, min^0'=min^post11, noncritical^0'=noncritical^post11, num^0'=num^post11, num_min^0'=num_min^post11, p^0'=p^post11, pid^0'=pid^post11, q^0'=q^post11, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -conditional^post11+conditional^0 == 0 /\ p^post11 == 0 /\ -num^post11+num^0 == 0 /\ -increase^post11+increase^0 == 0 /\ critical^post11 == 0 /\ -1+noncritical^post11 == 0 /\ num_min^0-num_min^post11 == 0 /\ -max^post11+min^post11 <= 0 /\ q^post11 == 0 /\ max_min^0-max_min^post11 == 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 New rule: l6 -> l4 : conditional^0'=conditional^post11, critical^0'=critical^post11, increase^0'=increase^post11, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^post11, min^0'=min^post11, noncritical^0'=noncritical^post11, num^0'=num^post11, num_min^0'=num_min^post11, p^0'=p^post11, pid^0'=pid^post11, q^0'=q^post11, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -conditional^post12+conditional^0 == 0 /\ p^post11 == 0 /\ -increase^post12+increase^0 == 0 /\ -j_min^post12+j_min^0 == 0 /\ -conditional^post11+conditional^post12 == 0 /\ -num^post11+num^post12 == 0 /\ -p^post12+p^0 == 0 /\ critical^post11 == 0 /\ num^0-num^post12 == 0 /\ max_min^0-max_min^post12 == 0 /\ -1+noncritical^post11 == 0 /\ critical^0-critical^post12 == 0 /\ -increase^post11+increase^post12 == 0 /\ -min^post12+min^0 == 0 /\ pid^0-pid^post12 == 0 /\ -noncritical^post12+noncritical^0 == 0 /\ -num_min^post11+num_min^post12 == 0 /\ -max^post11+min^post11 <= 0 /\ q^post11 == 0 /\ q^0-q^post12 == 0 /\ 1-min^post11 <= 0 /\ -max_min^post11+max_min^post12 == 0 /\ -max^post12+max^0 == 0 /\ num_min^0-num_min^post12 == 0 /\ 1-pid^post11 <= 0), cost: 1 Applied deletion Removed the following rules: 10 11 Simplified Transitions Start location: l6 Program variables: conditional^0 critical^0 increase^0 j_min^0 max^0 max_min^0 min^0 noncritical^0 num^0 num_min^0 p^0 pid^0 q^0 13: l0 -> l1 : conditional^0'=conditional^post1, -1+conditional^0 <= 0, cost: 1 14: l0 -> l1 : conditional^0'=conditional^post2, increase^0'=j_min^post2-j_min^0, j_min^0'=j_min^post2, (1-j_min^post2+j_min^0 <= 0 /\ 2-conditional^0 <= 0), cost: 1 19: l1 -> l3 : conditional^0'=conditional^post7, (1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 20: l1 -> l4 : critical^0'=1, p^0'=0, q^0'=0, pid^0-j_min^0 <= 0, cost: 1 21: l1 -> l4 : critical^0'=1, p^0'=0, q^0'=0, 1+num^0-min^0 <= 0, cost: 1 15: l2 -> l0 : conditional^0'=conditional^post3, p^0'=1, -1+conditional^0 <= 0, cost: 1 16: l2 -> l1 : conditional^0'=conditional^post4, increase^0'=min^post4-min^0, j_min^0'=j_min^post4, max_min^0'=max^0-min^0, min^0'=min^post4, num_min^0'=num^0-min^0, q^0'=1, (min^post4-max^0 <= 0 /\ 2-conditional^0 <= 0 /\ min^post4-num^0 <= 0 /\ -min^post4+num^0+min^0 <= 0 /\ 1-j_min^post4 <= 0), cost: 1 17: l3 -> l2 : conditional^0'=conditional^post5, -1+conditional^0 <= 0, cost: 1 18: l3 -> l2 : conditional^0'=conditional^post6, increase^0'=-max^0+max^post6, max^0'=max^post6, (2-conditional^0 <= 0 /\ 1+max^0-max^post6 <= 0), cost: 1 22: l4 -> l1 : critical^0'=0, max^0'=1+max^0, noncritical^0'=1, num^0'=1+max^0, T, cost: 1 23: l6 -> l4 : critical^0'=0, j_min^0'=j_min^post11, max^0'=max^post11, min^0'=min^post11, noncritical^0'=1, p^0'=0, pid^0'=pid^post11, q^0'=0, (1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 Propagated Equalities Original rule: l0 -> l1 : conditional^0'=conditional^post1, critical^0'=critical^post1, increase^0'=increase^post1, j_min^0'=j_min^post1, max^0'=max^post1, max_min^0'=max_min^post1, min^0'=min^post1, noncritical^0'=noncritical^post1, num^0'=num^post1, num_min^0'=num_min^post1, p^0'=p^post1, pid^0'=pid^post1, q^0'=q^post1, (0 == 0 /\ -j_min^post1+j_min^0 == 0 /\ -max^post1+max^0 == 0 /\ -p^post1+p^0 == 0 /\ -noncritical^post1+noncritical^0 == 0 /\ -1+conditional^0 <= 0 /\ q^0-q^post1 == 0 /\ pid^0-pid^post1 == 0 /\ -increase^post1+increase^0 == 0 /\ critical^0-critical^post1 == 0 /\ num_min^0-num_min^post1 == 0 /\ min^0-min^post1 == 0 /\ max_min^0-max_min^post1 == 0 /\ -num^post1+num^0 == 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^post1, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 propagated equality j_min^post1 = j_min^0 propagated equality max^post1 = max^0 propagated equality p^post1 = p^0 propagated equality noncritical^post1 = noncritical^0 propagated equality q^post1 = q^0 propagated equality pid^post1 = pid^0 propagated equality increase^post1 = increase^0 propagated equality critical^post1 = critical^0 propagated equality num_min^post1 = num_min^0 propagated equality min^post1 = min^0 propagated equality max_min^post1 = max_min^0 propagated equality num^post1 = num^0 Simplified Guard Original rule: l0 -> l1 : conditional^0'=conditional^post1, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^post1, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, -1+conditional^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : conditional^0'=conditional^post1, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, -1+conditional^0 <= 0, cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^post1, -1+conditional^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l1 : conditional^0'=conditional^post2, critical^0'=critical^post2, increase^0'=increase^post2, j_min^0'=j_min^post2, max^0'=max^post2, max_min^0'=max_min^post2, min^0'=min^post2, noncritical^0'=noncritical^post2, num^0'=num^post2, num_min^0'=num_min^post2, p^0'=p^post2, pid^0'=pid^post2, q^0'=q^post2, (0 == 0 /\ num^0-num^post2 == 0 /\ 2-conditional^0 <= 0 /\ -max^post2+max^0 == 0 /\ 1-increase^post2 <= 0 /\ -increase^post2+j_min^post2-j_min^0 == 0 /\ min^0-min^post2 == 0 /\ max_min^0-max_min^post2 == 0 /\ q^0-q^post2 == 0 /\ -p^post2+p^0 == 0 /\ pid^0-pid^post2 == 0 /\ num_min^0-num_min^post2 == 0 /\ -noncritical^post2+noncritical^0 == 0 /\ critical^0-critical^post2 == 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^post2, critical^0'=critical^0, increase^0'=j_min^post2-j_min^0, j_min^0'=j_min^post2, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ 1-j_min^post2+j_min^0 <= 0 /\ 2-conditional^0 <= 0), cost: 1 propagated equality num^post2 = num^0 propagated equality max^post2 = max^0 propagated equality increase^post2 = j_min^post2-j_min^0 propagated equality min^post2 = min^0 propagated equality max_min^post2 = max_min^0 propagated equality q^post2 = q^0 propagated equality p^post2 = p^0 propagated equality pid^post2 = pid^0 propagated equality num_min^post2 = num_min^0 propagated equality noncritical^post2 = noncritical^0 propagated equality critical^post2 = critical^0 Simplified Guard Original rule: l0 -> l1 : conditional^0'=conditional^post2, critical^0'=critical^0, increase^0'=j_min^post2-j_min^0, j_min^0'=j_min^post2, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ 1-j_min^post2+j_min^0 <= 0 /\ 2-conditional^0 <= 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^post2, critical^0'=critical^0, increase^0'=j_min^post2-j_min^0, j_min^0'=j_min^post2, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (1-j_min^post2+j_min^0 <= 0 /\ 2-conditional^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : conditional^0'=conditional^post2, critical^0'=critical^0, increase^0'=j_min^post2-j_min^0, j_min^0'=j_min^post2, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (1-j_min^post2+j_min^0 <= 0 /\ 2-conditional^0 <= 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^post2, increase^0'=j_min^post2-j_min^0, j_min^0'=j_min^post2, (1-j_min^post2+j_min^0 <= 0 /\ 2-conditional^0 <= 0), cost: 1 Propagated Equalities Original rule: l2 -> l0 : conditional^0'=conditional^post3, critical^0'=critical^post3, increase^0'=increase^post3, j_min^0'=j_min^post3, max^0'=max^post3, max_min^0'=max_min^post3, min^0'=min^post3, noncritical^0'=noncritical^post3, num^0'=num^post3, num_min^0'=num_min^post3, p^0'=p^post3, pid^0'=pid^post3, q^0'=q^post3, (0 == 0 /\ -1+p^post3 == 0 /\ -q^post3+q^0 == 0 /\ -1+conditional^0 <= 0 /\ pid^0-pid^post3 == 0 /\ num_min^0-num_min^post3 == 0 /\ -j_min^post3+j_min^0 == 0 /\ max_min^0-max_min^post3 == 0 /\ -min^post3+min^0 == 0 /\ -noncritical^post3+noncritical^0 == 0 /\ -max^post3+max^0 == 0 /\ critical^0-critical^post3 == 0 /\ num^0-num^post3 == 0 /\ -increase^post3+increase^0 == 0), cost: 1 New rule: l2 -> l0 : conditional^0'=conditional^post3, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=1, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 propagated equality p^post3 = 1 propagated equality q^post3 = q^0 propagated equality pid^post3 = pid^0 propagated equality num_min^post3 = num_min^0 propagated equality j_min^post3 = j_min^0 propagated equality max_min^post3 = max_min^0 propagated equality min^post3 = min^0 propagated equality noncritical^post3 = noncritical^0 propagated equality max^post3 = max^0 propagated equality critical^post3 = critical^0 propagated equality num^post3 = num^0 propagated equality increase^post3 = increase^0 Simplified Guard Original rule: l2 -> l0 : conditional^0'=conditional^post3, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=1, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 New rule: l2 -> l0 : conditional^0'=conditional^post3, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=1, pid^0'=pid^0, q^0'=q^0, -1+conditional^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : conditional^0'=conditional^post3, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=1, pid^0'=pid^0, q^0'=q^0, -1+conditional^0 <= 0, cost: 1 New rule: l2 -> l0 : conditional^0'=conditional^post3, p^0'=1, -1+conditional^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l1 : conditional^0'=conditional^post4, critical^0'=critical^post4, increase^0'=increase^post4, j_min^0'=j_min^post4, max^0'=max^post4, max_min^0'=max_min^post4, min^0'=min^post4, noncritical^0'=noncritical^post4, num^0'=num^post4, num_min^0'=num_min^post4, p^0'=p^post4, pid^0'=pid^post4, q^0'=q^post4, (0 == 0 /\ max^0-max^post4 == 0 /\ 2-conditional^0 <= 0 /\ max_min^post4-max^0+min^0 == 0 /\ -p^post4+p^0 == 0 /\ increase^post4-max^0+min^0 <= 0 /\ num_min^post4-num^0+min^0 == 0 /\ -pid^post4+pid^0 == 0 /\ -increase^post4+min^post4-min^0 == 0 /\ increase^post4-num_min^post4 <= 0 /\ -increase^post4+num^0 <= 0 /\ -1+q^post4 == 0 /\ noncritical^0-noncritical^post4 == 0 /\ num^0-num^post4 == 0 /\ critical^0-critical^post4 == 0 /\ 1-j_min^post4 <= 0), cost: 1 New rule: l2 -> l1 : conditional^0'=conditional^post4, critical^0'=critical^0, increase^0'=min^post4-min^0, j_min^0'=j_min^post4, max^0'=max^0, max_min^0'=max^0-min^0, min^0'=min^post4, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num^0-min^0, p^0'=p^0, pid^0'=pid^0, q^0'=1, (0 == 0 /\ min^post4-max^0 <= 0 /\ 2-conditional^0 <= 0 /\ min^post4-num^0 <= 0 /\ -min^post4+num^0+min^0 <= 0 /\ 1-j_min^post4 <= 0), cost: 1 propagated equality max^post4 = max^0 propagated equality max_min^post4 = max^0-min^0 propagated equality p^post4 = p^0 propagated equality num_min^post4 = num^0-min^0 propagated equality pid^post4 = pid^0 propagated equality increase^post4 = min^post4-min^0 propagated equality q^post4 = 1 propagated equality noncritical^post4 = noncritical^0 propagated equality num^post4 = num^0 propagated equality critical^post4 = critical^0 Simplified Guard Original rule: l2 -> l1 : conditional^0'=conditional^post4, critical^0'=critical^0, increase^0'=min^post4-min^0, j_min^0'=j_min^post4, max^0'=max^0, max_min^0'=max^0-min^0, min^0'=min^post4, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num^0-min^0, p^0'=p^0, pid^0'=pid^0, q^0'=1, (0 == 0 /\ min^post4-max^0 <= 0 /\ 2-conditional^0 <= 0 /\ min^post4-num^0 <= 0 /\ -min^post4+num^0+min^0 <= 0 /\ 1-j_min^post4 <= 0), cost: 1 New rule: l2 -> l1 : conditional^0'=conditional^post4, critical^0'=critical^0, increase^0'=min^post4-min^0, j_min^0'=j_min^post4, max^0'=max^0, max_min^0'=max^0-min^0, min^0'=min^post4, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num^0-min^0, p^0'=p^0, pid^0'=pid^0, q^0'=1, (min^post4-max^0 <= 0 /\ 2-conditional^0 <= 0 /\ min^post4-num^0 <= 0 /\ -min^post4+num^0+min^0 <= 0 /\ 1-j_min^post4 <= 0), cost: 1 Removed Trivial Updates Original rule: l2 -> l1 : conditional^0'=conditional^post4, critical^0'=critical^0, increase^0'=min^post4-min^0, j_min^0'=j_min^post4, max^0'=max^0, max_min^0'=max^0-min^0, min^0'=min^post4, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num^0-min^0, p^0'=p^0, pid^0'=pid^0, q^0'=1, (min^post4-max^0 <= 0 /\ 2-conditional^0 <= 0 /\ min^post4-num^0 <= 0 /\ -min^post4+num^0+min^0 <= 0 /\ 1-j_min^post4 <= 0), cost: 1 New rule: l2 -> l1 : conditional^0'=conditional^post4, increase^0'=min^post4-min^0, j_min^0'=j_min^post4, max_min^0'=max^0-min^0, min^0'=min^post4, num_min^0'=num^0-min^0, q^0'=1, (min^post4-max^0 <= 0 /\ 2-conditional^0 <= 0 /\ min^post4-num^0 <= 0 /\ -min^post4+num^0+min^0 <= 0 /\ 1-j_min^post4 <= 0), cost: 1 Propagated Equalities Original rule: l3 -> l2 : conditional^0'=conditional^post5, critical^0'=critical^post5, increase^0'=increase^post5, j_min^0'=j_min^post5, max^0'=max^post5, max_min^0'=max_min^post5, min^0'=min^post5, noncritical^0'=noncritical^post5, num^0'=num^post5, num_min^0'=num_min^post5, p^0'=p^post5, pid^0'=pid^post5, q^0'=q^post5, (0 == 0 /\ -min^post5+min^0 == 0 /\ -1+conditional^0 <= 0 /\ -pid^post5+pid^0 == 0 /\ noncritical^0-noncritical^post5 == 0 /\ -num^post5+num^0 == 0 /\ -j_min^post5+j_min^0 == 0 /\ critical^0-critical^post5 == 0 /\ max_min^0-max_min^post5 == 0 /\ q^0-q^post5 == 0 /\ max^0-max^post5 == 0 /\ num_min^0-num_min^post5 == 0 /\ p^0-p^post5 == 0 /\ -increase^post5+increase^0 == 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^post5, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 propagated equality min^post5 = min^0 propagated equality pid^post5 = pid^0 propagated equality noncritical^post5 = noncritical^0 propagated equality num^post5 = num^0 propagated equality j_min^post5 = j_min^0 propagated equality critical^post5 = critical^0 propagated equality max_min^post5 = max_min^0 propagated equality q^post5 = q^0 propagated equality max^post5 = max^0 propagated equality num_min^post5 = num_min^0 propagated equality p^post5 = p^0 propagated equality increase^post5 = increase^0 Simplified Guard Original rule: l3 -> l2 : conditional^0'=conditional^post5, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^post5, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, -1+conditional^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : conditional^0'=conditional^post5, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, -1+conditional^0 <= 0, cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^post5, -1+conditional^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : conditional^0'=conditional^post6, critical^0'=critical^post6, increase^0'=increase^post6, j_min^0'=j_min^post6, max^0'=max^post6, max_min^0'=max_min^post6, min^0'=min^post6, noncritical^0'=noncritical^post6, num^0'=num^post6, num_min^0'=num_min^post6, p^0'=p^post6, pid^0'=pid^post6, q^0'=q^post6, (0 == 0 /\ -increase^post6-max^0+max^post6 == 0 /\ -num^post6+num^0 == 0 /\ 2-conditional^0 <= 0 /\ -j_min^post6+j_min^0 == 0 /\ -max_min^post6+max_min^0 == 0 /\ -min^post6+min^0 == 0 /\ pid^0-pid^post6 == 0 /\ 1-increase^post6 <= 0 /\ noncritical^0-noncritical^post6 == 0 /\ -q^post6+q^0 == 0 /\ num_min^0-num_min^post6 == 0 /\ -p^post6+p^0 == 0 /\ critical^0-critical^post6 == 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^post6, critical^0'=critical^0, increase^0'=-max^0+max^post6, j_min^0'=j_min^0, max^0'=max^post6, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ 2-conditional^0 <= 0 /\ 1+max^0-max^post6 <= 0), cost: 1 propagated equality increase^post6 = -max^0+max^post6 propagated equality num^post6 = num^0 propagated equality j_min^post6 = j_min^0 propagated equality max_min^post6 = max_min^0 propagated equality min^post6 = min^0 propagated equality pid^post6 = pid^0 propagated equality noncritical^post6 = noncritical^0 propagated equality q^post6 = q^0 propagated equality num_min^post6 = num_min^0 propagated equality p^post6 = p^0 propagated equality critical^post6 = critical^0 Simplified Guard Original rule: l3 -> l2 : conditional^0'=conditional^post6, critical^0'=critical^0, increase^0'=-max^0+max^post6, j_min^0'=j_min^0, max^0'=max^post6, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ 2-conditional^0 <= 0 /\ 1+max^0-max^post6 <= 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^post6, critical^0'=critical^0, increase^0'=-max^0+max^post6, j_min^0'=j_min^0, max^0'=max^post6, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (2-conditional^0 <= 0 /\ 1+max^0-max^post6 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : conditional^0'=conditional^post6, critical^0'=critical^0, increase^0'=-max^0+max^post6, j_min^0'=j_min^0, max^0'=max^post6, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (2-conditional^0 <= 0 /\ 1+max^0-max^post6 <= 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^post6, increase^0'=-max^0+max^post6, max^0'=max^post6, (2-conditional^0 <= 0 /\ 1+max^0-max^post6 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l3 : conditional^0'=conditional^post7, critical^0'=critical^post7, increase^0'=increase^post7, j_min^0'=j_min^post7, max^0'=max^post7, max_min^0'=max_min^post7, min^0'=min^post7, noncritical^0'=noncritical^post7, num^0'=num^post7, num_min^0'=num_min^post7, p^0'=p^post7, pid^0'=pid^post7, q^0'=q^post7, (0 == 0 /\ p^0-p^post7 == 0 /\ -pid^post7+pid^0 == 0 /\ 1-pid^0+j_min^0 <= 0 /\ -j_min^post7+j_min^0 == 0 /\ -increase^post7+increase^0 == 0 /\ noncritical^0-noncritical^post7 == 0 /\ max_min^0-max_min^post7 == 0 /\ -num^post7+num^0 == 0 /\ max^0-max^post7 == 0 /\ -min^post7+min^0 == 0 /\ q^0-q^post7 == 0 /\ num_min^0-num_min^post7 == 0 /\ -num^0+min^0 <= 0 /\ critical^0-critical^post7 == 0), cost: 1 New rule: l1 -> l3 : conditional^0'=conditional^post7, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ 1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 propagated equality p^post7 = p^0 propagated equality pid^post7 = pid^0 propagated equality j_min^post7 = j_min^0 propagated equality increase^post7 = increase^0 propagated equality noncritical^post7 = noncritical^0 propagated equality max_min^post7 = max_min^0 propagated equality num^post7 = num^0 propagated equality max^post7 = max^0 propagated equality min^post7 = min^0 propagated equality q^post7 = q^0 propagated equality num_min^post7 = num_min^0 propagated equality critical^post7 = critical^0 Simplified Guard Original rule: l1 -> l3 : conditional^0'=conditional^post7, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (0 == 0 /\ 1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 New rule: l1 -> l3 : conditional^0'=conditional^post7, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l1 -> l3 : conditional^0'=conditional^post7, critical^0'=critical^0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, (1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 New rule: l1 -> l3 : conditional^0'=conditional^post7, (1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l4 : conditional^0'=conditional^post8, critical^0'=critical^post8, increase^0'=increase^post8, j_min^0'=j_min^post8, max^0'=max^post8, max_min^0'=max_min^post8, min^0'=min^post8, noncritical^0'=noncritical^post8, num^0'=num^post8, num_min^0'=num_min^post8, p^0'=p^post8, pid^0'=pid^post8, q^0'=q^post8, (-1+critical^post8 == 0 /\ p^post8 == 0 /\ -noncritical^post8+noncritical^0 == 0 /\ pid^0-j_min^0 <= 0 /\ pid^0-pid^post8 == 0 /\ max_min^0-max_min^post8 == 0 /\ -min^post8+min^0 == 0 /\ num_min^0-num_min^post8 == 0 /\ max^0-max^post8 == 0 /\ conditional^0-conditional^post8 == 0 /\ -j_min^post8+j_min^0 == 0 /\ q^post8 == 0 /\ -increase^post8+increase^0 == 0 /\ -num^post8+num^0 == 0), cost: 1 New rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, (0 == 0 /\ pid^0-j_min^0 <= 0), cost: 1 propagated equality critical^post8 = 1 propagated equality p^post8 = 0 propagated equality noncritical^post8 = noncritical^0 propagated equality pid^post8 = pid^0 propagated equality max_min^post8 = max_min^0 propagated equality min^post8 = min^0 propagated equality num_min^post8 = num_min^0 propagated equality max^post8 = max^0 propagated equality conditional^post8 = conditional^0 propagated equality j_min^post8 = j_min^0 propagated equality q^post8 = 0 propagated equality increase^post8 = increase^0 propagated equality num^post8 = num^0 Simplified Guard Original rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, (0 == 0 /\ pid^0-j_min^0 <= 0), cost: 1 New rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, pid^0-j_min^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, pid^0-j_min^0 <= 0, cost: 1 New rule: l1 -> l4 : critical^0'=1, p^0'=0, q^0'=0, pid^0-j_min^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l4 : conditional^0'=conditional^post9, critical^0'=critical^post9, increase^0'=increase^post9, j_min^0'=j_min^post9, max^0'=max^post9, max_min^0'=max_min^post9, min^0'=min^post9, noncritical^0'=noncritical^post9, num^0'=num^post9, num_min^0'=num_min^post9, p^0'=p^post9, pid^0'=pid^post9, q^0'=q^post9, (-num^post9+num^0 == 0 /\ -noncritical^post9+noncritical^0 == 0 /\ -max^post9+max^0 == 0 /\ p^post9 == 0 /\ j_min^0-j_min^post9 == 0 /\ -increase^post9+increase^0 == 0 /\ -conditional^post9+conditional^0 == 0 /\ min^0-min^post9 == 0 /\ 1+num^0-min^0 <= 0 /\ num_min^0-num_min^post9 == 0 /\ pid^0-pid^post9 == 0 /\ -1+critical^post9 == 0 /\ max_min^0-max_min^post9 == 0 /\ q^post9 == 0), cost: 1 New rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, (0 == 0 /\ 1+num^0-min^0 <= 0), cost: 1 propagated equality num^post9 = num^0 propagated equality noncritical^post9 = noncritical^0 propagated equality max^post9 = max^0 propagated equality p^post9 = 0 propagated equality j_min^post9 = j_min^0 propagated equality increase^post9 = increase^0 propagated equality conditional^post9 = conditional^0 propagated equality min^post9 = min^0 propagated equality num_min^post9 = num_min^0 propagated equality pid^post9 = pid^0 propagated equality critical^post9 = 1 propagated equality max_min^post9 = max_min^0 propagated equality q^post9 = 0 Simplified Guard Original rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, (0 == 0 /\ 1+num^0-min^0 <= 0), cost: 1 New rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, 1+num^0-min^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : conditional^0'=conditional^0, critical^0'=1, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=noncritical^0, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^0, q^0'=0, 1+num^0-min^0 <= 0, cost: 1 New rule: l1 -> l4 : critical^0'=1, p^0'=0, q^0'=0, 1+num^0-min^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l1 : conditional^0'=conditional^post10, critical^0'=critical^post10, increase^0'=increase^post10, j_min^0'=j_min^post10, max^0'=max^post10, max_min^0'=max_min^post10, min^0'=min^post10, noncritical^0'=noncritical^post10, num^0'=num^post10, num_min^0'=num_min^post10, p^0'=p^post10, pid^0'=pid^post10, q^0'=q^post10, (-1+max^post10-max^0 == 0 /\ -p^post10+p^0 == 0 /\ critical^post10 == 0 /\ pid^0-pid^post10 == 0 /\ max_min^0-max_min^post10 == 0 /\ -1-max^0+num^post10 == 0 /\ -1+noncritical^post10 == 0 /\ -j_min^post10+j_min^0 == 0 /\ -min^post10+min^0 == 0 /\ -conditional^post10+conditional^0 == 0 /\ q^0-q^post10 == 0 /\ -increase^post10+increase^0 == 0 /\ num_min^0-num_min^post10 == 0), cost: 1 New rule: l4 -> l1 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=1+max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=1, num^0'=1+max^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, 0 == 0, cost: 1 propagated equality max^post10 = 1+max^0 propagated equality p^post10 = p^0 propagated equality critical^post10 = 0 propagated equality pid^post10 = pid^0 propagated equality max_min^post10 = max_min^0 propagated equality num^post10 = 1+max^0 propagated equality noncritical^post10 = 1 propagated equality j_min^post10 = j_min^0 propagated equality min^post10 = min^0 propagated equality conditional^post10 = conditional^0 propagated equality q^post10 = q^0 propagated equality increase^post10 = increase^0 propagated equality num_min^post10 = num_min^0 Simplified Guard Original rule: l4 -> l1 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=1+max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=1, num^0'=1+max^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, 0 == 0, cost: 1 New rule: l4 -> l1 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=1+max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=1, num^0'=1+max^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l1 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^0, max^0'=1+max^0, max_min^0'=max_min^0, min^0'=min^0, noncritical^0'=1, num^0'=1+max^0, num_min^0'=num_min^0, p^0'=p^0, pid^0'=pid^0, q^0'=q^0, T, cost: 1 New rule: l4 -> l1 : critical^0'=0, max^0'=1+max^0, noncritical^0'=1, num^0'=1+max^0, T, cost: 1 Propagated Equalities Original rule: l6 -> l4 : conditional^0'=conditional^post11, critical^0'=critical^post11, increase^0'=increase^post11, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^post11, min^0'=min^post11, noncritical^0'=noncritical^post11, num^0'=num^post11, num_min^0'=num_min^post11, p^0'=p^post11, pid^0'=pid^post11, q^0'=q^post11, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -conditional^post12+conditional^0 == 0 /\ p^post11 == 0 /\ -increase^post12+increase^0 == 0 /\ -j_min^post12+j_min^0 == 0 /\ -conditional^post11+conditional^post12 == 0 /\ -num^post11+num^post12 == 0 /\ -p^post12+p^0 == 0 /\ critical^post11 == 0 /\ num^0-num^post12 == 0 /\ max_min^0-max_min^post12 == 0 /\ -1+noncritical^post11 == 0 /\ critical^0-critical^post12 == 0 /\ -increase^post11+increase^post12 == 0 /\ -min^post12+min^0 == 0 /\ pid^0-pid^post12 == 0 /\ -noncritical^post12+noncritical^0 == 0 /\ -num_min^post11+num_min^post12 == 0 /\ -max^post11+min^post11 <= 0 /\ q^post11 == 0 /\ q^0-q^post12 == 0 /\ 1-min^post11 <= 0 /\ -max_min^post11+max_min^post12 == 0 /\ -max^post12+max^0 == 0 /\ num_min^0-num_min^post12 == 0 /\ 1-pid^post11 <= 0), cost: 1 New rule: l6 -> l4 : conditional^0'=conditional^post12, critical^0'=0, increase^0'=increase^post12, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^post12, min^0'=min^post11, noncritical^0'=1, num^0'=num^post12, num_min^0'=num_min^post12, p^0'=0, pid^0'=pid^post11, q^0'=0, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -conditional^post12+conditional^0 == 0 /\ -increase^post12+increase^0 == 0 /\ -j_min^post12+j_min^0 == 0 /\ -p^post12+p^0 == 0 /\ num^0-num^post12 == 0 /\ max_min^0-max_min^post12 == 0 /\ critical^0-critical^post12 == 0 /\ -min^post12+min^0 == 0 /\ pid^0-pid^post12 == 0 /\ -noncritical^post12+noncritical^0 == 0 /\ -max^post11+min^post11 <= 0 /\ q^0-q^post12 == 0 /\ 1-min^post11 <= 0 /\ -max^post12+max^0 == 0 /\ num_min^0-num_min^post12 == 0 /\ 1-pid^post11 <= 0), cost: 1 propagated equality p^post11 = 0 propagated equality conditional^post11 = conditional^post12 propagated equality num^post11 = num^post12 propagated equality critical^post11 = 0 propagated equality noncritical^post11 = 1 propagated equality increase^post11 = increase^post12 propagated equality num_min^post11 = num_min^post12 propagated equality q^post11 = 0 propagated equality max_min^post11 = max_min^post12 Propagated Equalities Original rule: l6 -> l4 : conditional^0'=conditional^post12, critical^0'=0, increase^0'=increase^post12, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^post12, min^0'=min^post11, noncritical^0'=1, num^0'=num^post12, num_min^0'=num_min^post12, p^0'=0, pid^0'=pid^post11, q^0'=0, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -conditional^post12+conditional^0 == 0 /\ -increase^post12+increase^0 == 0 /\ -j_min^post12+j_min^0 == 0 /\ -p^post12+p^0 == 0 /\ num^0-num^post12 == 0 /\ max_min^0-max_min^post12 == 0 /\ critical^0-critical^post12 == 0 /\ -min^post12+min^0 == 0 /\ pid^0-pid^post12 == 0 /\ -noncritical^post12+noncritical^0 == 0 /\ -max^post11+min^post11 <= 0 /\ q^0-q^post12 == 0 /\ 1-min^post11 <= 0 /\ -max^post12+max^0 == 0 /\ num_min^0-num_min^post12 == 0 /\ 1-pid^post11 <= 0), cost: 1 New rule: l6 -> l4 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^0, min^0'=min^post11, noncritical^0'=1, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^post11, q^0'=0, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 propagated equality conditional^post12 = conditional^0 propagated equality increase^post12 = increase^0 propagated equality j_min^post12 = j_min^0 propagated equality p^post12 = p^0 propagated equality num^post12 = num^0 propagated equality max_min^post12 = max_min^0 propagated equality critical^post12 = critical^0 propagated equality min^post12 = min^0 propagated equality pid^post12 = pid^0 propagated equality noncritical^post12 = noncritical^0 propagated equality q^post12 = q^0 propagated equality max^post12 = max^0 propagated equality num_min^post12 = num_min^0 Simplified Guard Original rule: l6 -> l4 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^0, min^0'=min^post11, noncritical^0'=1, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^post11, q^0'=0, (0 == 0 /\ 1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 New rule: l6 -> l4 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^0, min^0'=min^post11, noncritical^0'=1, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^post11, q^0'=0, (1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 Removed Trivial Updates Original rule: l6 -> l4 : conditional^0'=conditional^0, critical^0'=0, increase^0'=increase^0, j_min^0'=j_min^post11, max^0'=max^post11, max_min^0'=max_min^0, min^0'=min^post11, noncritical^0'=1, num^0'=num^0, num_min^0'=num_min^0, p^0'=0, pid^0'=pid^post11, q^0'=0, (1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 New rule: l6 -> l4 : critical^0'=0, j_min^0'=j_min^post11, max^0'=max^post11, min^0'=min^post11, noncritical^0'=1, p^0'=0, pid^0'=pid^post11, q^0'=0, (1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 Step with 23 Trace 23[(1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0)] Blocked [{}, {}] Step with 22 Trace 23[(1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0)], 22[T] Blocked [{}, {}, {}] Step with 19 Trace 23[(1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0)], 22[T], 19[(1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 17 Trace 23[(1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0)], 22[T], 19[(1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0)], 17[(-1+conditional^0 <= 0)] Blocked [{}, {}, {}, {}, {}] Step with 15 Trace 23[(1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0)], 22[T], 19[(1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0)], 17[(-1+conditional^0 <= 0)], 15[(-1+conditional^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}] Step with 13 Trace 23[(1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0)], 22[T], 19[(1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0)], 17[(-1+conditional^0 <= 0)], 15[(-1+conditional^0 <= 0)], 13[(-1+conditional^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {}] Nonterm Start location: l6 Program variables: conditional^0 critical^0 increase^0 j_min^0 max^0 max_min^0 min^0 noncritical^0 num^0 num_min^0 p^0 pid^0 q^0 13: l0 -> l1 : conditional^0'=conditional^post1, -1+conditional^0 <= 0, cost: 1 14: l0 -> l1 : conditional^0'=conditional^post2, increase^0'=j_min^post2-j_min^0, j_min^0'=j_min^post2, (1-j_min^post2+j_min^0 <= 0 /\ 2-conditional^0 <= 0), cost: 1 19: l1 -> l3 : conditional^0'=conditional^post7, (1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 20: l1 -> l4 : critical^0'=1, p^0'=0, q^0'=0, pid^0-j_min^0 <= 0, cost: 1 21: l1 -> l4 : critical^0'=1, p^0'=0, q^0'=0, 1+num^0-min^0 <= 0, cost: 1 24: l1 -> LoAT_sink : (-1+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ num^0-min^0 >= 0), cost: NONTERM 15: l2 -> l0 : conditional^0'=conditional^post3, p^0'=1, -1+conditional^0 <= 0, cost: 1 16: l2 -> l1 : conditional^0'=conditional^post4, increase^0'=min^post4-min^0, j_min^0'=j_min^post4, max_min^0'=max^0-min^0, min^0'=min^post4, num_min^0'=num^0-min^0, q^0'=1, (min^post4-max^0 <= 0 /\ 2-conditional^0 <= 0 /\ min^post4-num^0 <= 0 /\ -min^post4+num^0+min^0 <= 0 /\ 1-j_min^post4 <= 0), cost: 1 17: l3 -> l2 : conditional^0'=conditional^post5, -1+conditional^0 <= 0, cost: 1 18: l3 -> l2 : conditional^0'=conditional^post6, increase^0'=-max^0+max^post6, max^0'=max^post6, (2-conditional^0 <= 0 /\ 1+max^0-max^post6 <= 0), cost: 1 22: l4 -> l1 : critical^0'=0, max^0'=1+max^0, noncritical^0'=1, num^0'=1+max^0, T, cost: 1 23: l6 -> l4 : critical^0'=0, j_min^0'=j_min^post11, max^0'=max^post11, min^0'=min^post11, noncritical^0'=1, p^0'=0, pid^0'=pid^post11, q^0'=0, (1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0), cost: 1 Certificate of Non-Termination Original rule: l1 -> l1 : conditional^0'=conditional^post1, p^0'=1, (1-pid^0+j_min^0 <= 0 /\ -num^0+min^0 <= 0), cost: 1 New rule: l1 -> LoAT_sink : (-1+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ num^0-min^0 >= 0), cost: NONTERM -1+pid^0-j_min^0 >= 0 [0]: monotonic increase yields -1+pid^0-j_min^0 >= 0 num^0-min^0 >= 0 [0]: monotonic increase yields num^0-min^0 >= 0 Replacement map: {-1+pid^0-j_min^0 >= 0 -> -1+pid^0-j_min^0 >= 0, num^0-min^0 >= 0 -> num^0-min^0 >= 0} Step with 24 Trace 23[(1-j_min^post11 <= 0 /\ -max^post11+min^post11 <= 0 /\ 1-min^post11 <= 0 /\ 1-pid^post11 <= 0)], 22[T], 24[(-1+pid^0-j_min^0 >= 0 /\ -1+n >= 0 /\ num^0-min^0 >= 0)] Blocked [{}, {}, {}, {24[T]}] Refute Counterexample [ conditional^0=0 critical^0=0 increase^0=0 j_min^0=1 max^0=1 max_min^0=0 min^0=1 noncritical^0=1 num^0=0 num_min^0=0 p^0=0 pid^0=2 q^0=0 ] 23 [ conditional^0=0 critical^0=0 increase^0=0 j_min^0=1 max^0=2 max_min^0=0 min^0=1 noncritical^0=1 num^0=2 num_min^0=0 p^0=0 pid^0=2 q^0=0 ] 22 [ conditional^0=0 critical^0=critical^0 increase^0=0 j_min^0=j_min^0 max^0=max^0 max_min^0=0 min^0=min^0 noncritical^0=noncritical^0 num^0=0 num_min^0=0 p^0=p^0 pid^0=pid^0 q^0=q^0 ] 24 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b