NO Initial ITS Start location: l7 Program variables: conditional^0 dname^0 i^0 iocreatedevice^0 num^0 pdo^0 pdolen^0 ppblockinits^0 ppbunlockinits^0 status^0 0: l0 -> l1 : conditional^0'=conditional^post1, dname^0'=dname^post1, i^0'=i^post1, iocreatedevice^0'=iocreatedevice^post1, num^0'=num^post1, pdo^0'=pdo^post1, pdolen^0'=pdolen^post1, ppblockinits^0'=ppblockinits^post1, ppbunlockinits^0'=ppbunlockinits^post1, status^0'=status^post1, (-ppbunlockinits^post1+ppbunlockinits^0 == 0 /\ pdo^0-pdo^post1 == 0 /\ -1+conditional^0 <= 0 /\ -num^post1+num^0 == 0 /\ ppblockinits^0-ppblockinits^post1 == 0 /\ -conditional^post1+conditional^0 == 0 /\ pdolen^0-pdolen^post1 == 0 /\ -dname^post1+dname^0 == 0 /\ i^0-i^post1 == 0 /\ -iocreatedevice^post1+iocreatedevice^0 == 0 /\ status^0-status^post1 == 0), cost: 1 1: l0 -> l2 : conditional^0'=conditional^post2, dname^0'=dname^post2, i^0'=i^post2, iocreatedevice^0'=iocreatedevice^post2, num^0'=num^post2, pdo^0'=pdo^post2, pdolen^0'=pdolen^post2, ppblockinits^0'=ppblockinits^post2, ppbunlockinits^0'=ppbunlockinits^post2, status^0'=status^post2, (pdolen^0-pdolen^post2 == 0 /\ 2-conditional^0 <= 0 /\ -1+num^post2-num^0 == 0 /\ pdo^0-pdo^post2 == 0 /\ -ppbunlockinits^post2+ppbunlockinits^0 == 0 /\ ppblockinits^0-ppblockinits^post2 == 0 /\ -conditional^post2+conditional^0 == 0 /\ -iocreatedevice^post2+iocreatedevice^0 == 0 /\ i^0-i^post2 == 0 /\ -status^post2+status^0 == 0 /\ -dname^post2+dname^0 == 0), cost: 1 4: l1 -> l4 : conditional^0'=conditional^post5, dname^0'=dname^post5, i^0'=i^post5, iocreatedevice^0'=iocreatedevice^post5, num^0'=num^post5, pdo^0'=pdo^post5, pdolen^0'=pdolen^post5, ppblockinits^0'=ppblockinits^post5, ppbunlockinits^0'=ppbunlockinits^post5, status^0'=status^post5, (i^0-i^post5 == 0 /\ conditional^0-conditional^post5 == 0 /\ num^post5 == 0 /\ status^0-status^post5 == 0 /\ pdolen^0-pdolen^post5 == 0 /\ pdo^0-pdo^post5 == 0 /\ -dname^post5+dname^0 == 0 /\ iocreatedevice^0-iocreatedevice^post5 == 0 /\ -ppblockinits^post5+ppblockinits^0 == 0 /\ -1+ppbunlockinits^post5 == 0), cost: 1 7: l2 -> l1 : conditional^0'=conditional^post8, dname^0'=dname^post8, i^0'=i^post8, iocreatedevice^0'=iocreatedevice^post8, num^0'=num^post8, pdo^0'=pdo^post8, pdolen^0'=pdolen^post8, ppblockinits^0'=ppblockinits^post8, ppbunlockinits^0'=ppbunlockinits^post8, status^0'=status^post8, (pdolen^0-pdolen^post8 == 0 /\ status^post8 == 0 /\ -conditional^post8+conditional^0 == 0 /\ pdolen^0-i^0 <= 0 /\ pdo^0-pdo^post8 == 0 /\ -ppbunlockinits^post8+ppbunlockinits^0 == 0 /\ -dname^post8+dname^0 == 0 /\ ppblockinits^0-ppblockinits^post8 == 0 /\ -num^post8+num^0 == 0 /\ -iocreatedevice^post8+iocreatedevice^0 == 0 /\ i^0-i^post8 == 0), cost: 1 8: l2 -> l5 : conditional^0'=conditional^post9, dname^0'=dname^post9, i^0'=i^post9, iocreatedevice^0'=iocreatedevice^post9, num^0'=num^post9, pdo^0'=pdo^post9, pdolen^0'=pdolen^post9, ppblockinits^0'=ppblockinits^post9, ppbunlockinits^0'=ppbunlockinits^post9, status^0'=status^post9, (0 == 0 /\ -iocreatedevice^post9+iocreatedevice^0 == 0 /\ -num^post9+num^0 == 0 /\ pdo^0-pdo^post9 == 0 /\ status^post9 == 0 /\ -conditional^post9+conditional^0 == 0 /\ 1-pdolen^0+i^0 <= 0 /\ pdolen^0-pdolen^post9 == 0 /\ ppbunlockinits^0-ppbunlockinits^post9 == 0 /\ i^0-i^post9 == 0 /\ -1+ppblockinits^post9 == 0), cost: 1 2: l3 -> l2 : conditional^0'=conditional^post3, dname^0'=dname^post3, i^0'=i^post3, iocreatedevice^0'=iocreatedevice^post3, num^0'=num^post3, pdo^0'=pdo^post3, pdolen^0'=pdolen^post3, ppblockinits^0'=ppblockinits^post3, ppbunlockinits^0'=ppbunlockinits^post3, status^0'=status^post3, (-conditional^post3+conditional^0 == 0 /\ iocreatedevice^post3 == 0 /\ -dname^post3+dname^0 == 0 /\ pdo^0-pdo^post3 == 0 /\ -1+conditional^0 <= 0 /\ -1-i^0+i^post3 == 0 /\ -1+status^post3 == 0 /\ ppblockinits^0-ppblockinits^post3 == 0 /\ -num^post3+num^0 == 0 /\ pdolen^0-pdolen^post3 == 0 /\ ppbunlockinits^0-ppbunlockinits^post3 == 0), cost: 1 3: l3 -> l0 : conditional^0'=conditional^post4, dname^0'=dname^post4, i^0'=i^post4, iocreatedevice^0'=iocreatedevice^post4, num^0'=num^post4, pdo^0'=pdo^post4, pdolen^0'=pdolen^post4, ppblockinits^0'=ppblockinits^post4, ppbunlockinits^0'=ppbunlockinits^post4, status^0'=status^post4, (0 == 0 /\ num^0-num^post4 == 0 /\ pdo^post4 == 0 /\ 2-conditional^0 <= 0 /\ i^0-i^post4 == 0 /\ iocreatedevice^post4 == 0 /\ -ppbunlockinits^post4+ppbunlockinits^0 == 0 /\ -dname^post4+dname^0 == 0 /\ ppblockinits^0-ppblockinits^post4 == 0 /\ -status^post4+status^0 == 0 /\ pdolen^0-pdolen^post4 == 0), cost: 1 5: l5 -> l1 : conditional^0'=conditional^post6, dname^0'=dname^post6, i^0'=i^post6, iocreatedevice^0'=iocreatedevice^post6, num^0'=num^post6, pdo^0'=pdo^post6, pdolen^0'=pdolen^post6, ppblockinits^0'=ppblockinits^post6, ppbunlockinits^0'=ppbunlockinits^post6, status^0'=status^post6, (ppblockinits^0-ppblockinits^post6 == 0 /\ -pdolen^post6+pdolen^0 == 0 /\ -ppbunlockinits^post6+ppbunlockinits^0 == 0 /\ -conditional^post6+conditional^0 == 0 /\ i^0-i^post6 == 0 /\ -num^post6+num^0 == 0 /\ pdo^0-pdo^post6 == 0 /\ -dname^post6+dname^0 == 0 /\ status^0-status^post6 == 0 /\ iocreatedevice^0-iocreatedevice^post6 == 0 /\ dname^0 <= 0), cost: 1 6: l5 -> l3 : conditional^0'=conditional^post7, dname^0'=dname^post7, i^0'=i^post7, iocreatedevice^0'=iocreatedevice^post7, num^0'=num^post7, pdo^0'=pdo^post7, pdolen^0'=pdolen^post7, ppblockinits^0'=ppblockinits^post7, ppbunlockinits^0'=ppbunlockinits^post7, status^0'=status^post7, (0 == 0 /\ pdolen^0-pdolen^post7 == 0 /\ pdo^0-pdo^post7 == 0 /\ -1+iocreatedevice^post7 == 0 /\ -ppbunlockinits^post7+ppbunlockinits^0 == 0 /\ ppblockinits^0-ppblockinits^post7 == 0 /\ -dname^post7+dname^0 == 0 /\ -num^post7+num^0 == 0 /\ -status^post7+status^0 == 0 /\ i^0-i^post7 == 0 /\ 1-dname^0 <= 0), cost: 1 9: l6 -> l2 : conditional^0'=conditional^post10, dname^0'=dname^post10, i^0'=i^post10, iocreatedevice^0'=iocreatedevice^post10, num^0'=num^post10, pdo^0'=pdo^post10, pdolen^0'=pdolen^post10, ppblockinits^0'=ppblockinits^post10, ppbunlockinits^0'=ppbunlockinits^post10, status^0'=status^post10, (0 == 0 /\ ppbunlockinits^post10 == 0 /\ num^0-num^post10 == 0 /\ status^post10 == 0 /\ -1+ppblockinits^post10 == 0 /\ -conditional^post10+conditional^0 == 0 /\ iocreatedevice^post10 == 0 /\ -dname^post10+dname^0 == 0 /\ -pdo^post10+pdo^0 == 0), cost: 1 10: l7 -> l6 : conditional^0'=conditional^post11, dname^0'=dname^post11, i^0'=i^post11, iocreatedevice^0'=iocreatedevice^post11, num^0'=num^post11, pdo^0'=pdo^post11, pdolen^0'=pdolen^post11, ppblockinits^0'=ppblockinits^post11, ppbunlockinits^0'=ppbunlockinits^post11, status^0'=status^post11, (-conditional^post11+conditional^0 == 0 /\ -iocreatedevice^post11+iocreatedevice^0 == 0 /\ -ppblockinits^post11+ppblockinits^0 == 0 /\ -ppbunlockinits^post11+ppbunlockinits^0 == 0 /\ pdo^0-pdo^post11 == 0 /\ -dname^post11+dname^0 == 0 /\ i^0-i^post11 == 0 /\ status^0-status^post11 == 0 /\ -num^post11+num^0 == 0 /\ pdolen^0-pdolen^post11 == 0), cost: 1 Chained Linear Paths Start location: l7 Program variables: conditional^0 dname^0 i^0 iocreatedevice^0 num^0 pdo^0 pdolen^0 ppblockinits^0 ppbunlockinits^0 status^0 0: l0 -> l1 : conditional^0'=conditional^post1, dname^0'=dname^post1, i^0'=i^post1, iocreatedevice^0'=iocreatedevice^post1, num^0'=num^post1, pdo^0'=pdo^post1, pdolen^0'=pdolen^post1, ppblockinits^0'=ppblockinits^post1, ppbunlockinits^0'=ppbunlockinits^post1, status^0'=status^post1, (-ppbunlockinits^post1+ppbunlockinits^0 == 0 /\ pdo^0-pdo^post1 == 0 /\ -1+conditional^0 <= 0 /\ -num^post1+num^0 == 0 /\ ppblockinits^0-ppblockinits^post1 == 0 /\ -conditional^post1+conditional^0 == 0 /\ pdolen^0-pdolen^post1 == 0 /\ -dname^post1+dname^0 == 0 /\ i^0-i^post1 == 0 /\ -iocreatedevice^post1+iocreatedevice^0 == 0 /\ status^0-status^post1 == 0), cost: 1 1: l0 -> l2 : conditional^0'=conditional^post2, dname^0'=dname^post2, i^0'=i^post2, iocreatedevice^0'=iocreatedevice^post2, num^0'=num^post2, pdo^0'=pdo^post2, pdolen^0'=pdolen^post2, ppblockinits^0'=ppblockinits^post2, ppbunlockinits^0'=ppbunlockinits^post2, status^0'=status^post2, (pdolen^0-pdolen^post2 == 0 /\ 2-conditional^0 <= 0 /\ -1+num^post2-num^0 == 0 /\ pdo^0-pdo^post2 == 0 /\ -ppbunlockinits^post2+ppbunlockinits^0 == 0 /\ ppblockinits^0-ppblockinits^post2 == 0 /\ -conditional^post2+conditional^0 == 0 /\ -iocreatedevice^post2+iocreatedevice^0 == 0 /\ i^0-i^post2 == 0 /\ -status^post2+status^0 == 0 /\ -dname^post2+dname^0 == 0), cost: 1 4: l1 -> l4 : conditional^0'=conditional^post5, dname^0'=dname^post5, i^0'=i^post5, iocreatedevice^0'=iocreatedevice^post5, num^0'=num^post5, pdo^0'=pdo^post5, pdolen^0'=pdolen^post5, ppblockinits^0'=ppblockinits^post5, ppbunlockinits^0'=ppbunlockinits^post5, status^0'=status^post5, (i^0-i^post5 == 0 /\ conditional^0-conditional^post5 == 0 /\ num^post5 == 0 /\ status^0-status^post5 == 0 /\ pdolen^0-pdolen^post5 == 0 /\ pdo^0-pdo^post5 == 0 /\ -dname^post5+dname^0 == 0 /\ iocreatedevice^0-iocreatedevice^post5 == 0 /\ -ppblockinits^post5+ppblockinits^0 == 0 /\ -1+ppbunlockinits^post5 == 0), cost: 1 7: l2 -> l1 : conditional^0'=conditional^post8, dname^0'=dname^post8, i^0'=i^post8, iocreatedevice^0'=iocreatedevice^post8, num^0'=num^post8, pdo^0'=pdo^post8, pdolen^0'=pdolen^post8, ppblockinits^0'=ppblockinits^post8, ppbunlockinits^0'=ppbunlockinits^post8, status^0'=status^post8, (pdolen^0-pdolen^post8 == 0 /\ status^post8 == 0 /\ -conditional^post8+conditional^0 == 0 /\ pdolen^0-i^0 <= 0 /\ pdo^0-pdo^post8 == 0 /\ -ppbunlockinits^post8+ppbunlockinits^0 == 0 /\ -dname^post8+dname^0 == 0 /\ ppblockinits^0-ppblockinits^post8 == 0 /\ -num^post8+num^0 == 0 /\ -iocreatedevice^post8+iocreatedevice^0 == 0 /\ i^0-i^post8 == 0), cost: 1 8: l2 -> l5 : conditional^0'=conditional^post9, dname^0'=dname^post9, i^0'=i^post9, iocreatedevice^0'=iocreatedevice^post9, num^0'=num^post9, pdo^0'=pdo^post9, pdolen^0'=pdolen^post9, ppblockinits^0'=ppblockinits^post9, ppbunlockinits^0'=ppbunlockinits^post9, status^0'=status^post9, (0 == 0 /\ -iocreatedevice^post9+iocreatedevice^0 == 0 /\ -num^post9+num^0 == 0 /\ pdo^0-pdo^post9 == 0 /\ status^post9 == 0 /\ -conditional^post9+conditional^0 == 0 /\ 1-pdolen^0+i^0 <= 0 /\ pdolen^0-pdolen^post9 == 0 /\ ppbunlockinits^0-ppbunlockinits^post9 == 0 /\ i^0-i^post9 == 0 /\ -1+ppblockinits^post9 == 0), cost: 1 2: l3 -> l2 : conditional^0'=conditional^post3, dname^0'=dname^post3, i^0'=i^post3, iocreatedevice^0'=iocreatedevice^post3, num^0'=num^post3, pdo^0'=pdo^post3, pdolen^0'=pdolen^post3, ppblockinits^0'=ppblockinits^post3, ppbunlockinits^0'=ppbunlockinits^post3, status^0'=status^post3, (-conditional^post3+conditional^0 == 0 /\ iocreatedevice^post3 == 0 /\ -dname^post3+dname^0 == 0 /\ pdo^0-pdo^post3 == 0 /\ -1+conditional^0 <= 0 /\ -1-i^0+i^post3 == 0 /\ -1+status^post3 == 0 /\ ppblockinits^0-ppblockinits^post3 == 0 /\ -num^post3+num^0 == 0 /\ pdolen^0-pdolen^post3 == 0 /\ ppbunlockinits^0-ppbunlockinits^post3 == 0), cost: 1 3: l3 -> l0 : conditional^0'=conditional^post4, dname^0'=dname^post4, i^0'=i^post4, iocreatedevice^0'=iocreatedevice^post4, num^0'=num^post4, pdo^0'=pdo^post4, pdolen^0'=pdolen^post4, ppblockinits^0'=ppblockinits^post4, ppbunlockinits^0'=ppbunlockinits^post4, status^0'=status^post4, (0 == 0 /\ num^0-num^post4 == 0 /\ pdo^post4 == 0 /\ 2-conditional^0 <= 0 /\ i^0-i^post4 == 0 /\ iocreatedevice^post4 == 0 /\ -ppbunlockinits^post4+ppbunlockinits^0 == 0 /\ -dname^post4+dname^0 == 0 /\ ppblockinits^0-ppblockinits^post4 == 0 /\ -status^post4+status^0 == 0 /\ pdolen^0-pdolen^post4 == 0), cost: 1 5: l5 -> l1 : conditional^0'=conditional^post6, dname^0'=dname^post6, i^0'=i^post6, iocreatedevice^0'=iocreatedevice^post6, num^0'=num^post6, pdo^0'=pdo^post6, pdolen^0'=pdolen^post6, ppblockinits^0'=ppblockinits^post6, ppbunlockinits^0'=ppbunlockinits^post6, status^0'=status^post6, (ppblockinits^0-ppblockinits^post6 == 0 /\ -pdolen^post6+pdolen^0 == 0 /\ -ppbunlockinits^post6+ppbunlockinits^0 == 0 /\ -conditional^post6+conditional^0 == 0 /\ i^0-i^post6 == 0 /\ -num^post6+num^0 == 0 /\ pdo^0-pdo^post6 == 0 /\ -dname^post6+dname^0 == 0 /\ status^0-status^post6 == 0 /\ iocreatedevice^0-iocreatedevice^post6 == 0 /\ dname^0 <= 0), cost: 1 6: l5 -> l3 : conditional^0'=conditional^post7, dname^0'=dname^post7, i^0'=i^post7, iocreatedevice^0'=iocreatedevice^post7, num^0'=num^post7, pdo^0'=pdo^post7, pdolen^0'=pdolen^post7, ppblockinits^0'=ppblockinits^post7, ppbunlockinits^0'=ppbunlockinits^post7, status^0'=status^post7, (0 == 0 /\ pdolen^0-pdolen^post7 == 0 /\ pdo^0-pdo^post7 == 0 /\ -1+iocreatedevice^post7 == 0 /\ -ppbunlockinits^post7+ppbunlockinits^0 == 0 /\ ppblockinits^0-ppblockinits^post7 == 0 /\ -dname^post7+dname^0 == 0 /\ -num^post7+num^0 == 0 /\ -status^post7+status^0 == 0 /\ i^0-i^post7 == 0 /\ 1-dname^0 <= 0), cost: 1 11: l7 -> l2 : conditional^0'=conditional^post10, dname^0'=dname^post10, i^0'=i^post10, iocreatedevice^0'=iocreatedevice^post10, num^0'=num^post10, pdo^0'=pdo^post10, pdolen^0'=pdolen^post10, ppblockinits^0'=ppblockinits^post10, ppbunlockinits^0'=ppbunlockinits^post10, status^0'=status^post10, (0 == 0 /\ ppbunlockinits^post10 == 0 /\ -conditional^post10+conditional^post11 == 0 /\ -conditional^post11+conditional^0 == 0 /\ -iocreatedevice^post11+iocreatedevice^0 == 0 /\ num^post11-num^post10 == 0 /\ -ppblockinits^post11+ppblockinits^0 == 0 /\ -ppbunlockinits^post11+ppbunlockinits^0 == 0 /\ status^post10 == 0 /\ pdo^0-pdo^post11 == 0 /\ -dname^post11+dname^0 == 0 /\ -1+ppblockinits^post10 == 0 /\ i^0-i^post11 == 0 /\ iocreatedevice^post10 == 0 /\ status^0-status^post11 == 0 /\ -num^post11+num^0 == 0 /\ -pdo^post10+pdo^post11 == 0 /\ -dname^post10+dname^post11 == 0 /\ pdolen^0-pdolen^post11 == 0), cost: 1 Eliminating location l6 by chaining: Applied chaining First rule: l7 -> l6 : conditional^0'=conditional^post11, dname^0'=dname^post11, i^0'=i^post11, iocreatedevice^0'=iocreatedevice^post11, num^0'=num^post11, pdo^0'=pdo^post11, pdolen^0'=pdolen^post11, ppblockinits^0'=ppblockinits^post11, ppbunlockinits^0'=ppbunlockinits^post11, status^0'=status^post11, (-conditional^post11+conditional^0 == 0 /\ -iocreatedevice^post11+iocreatedevice^0 == 0 /\ -ppblockinits^post11+ppblockinits^0 == 0 /\ -ppbunlockinits^post11+ppbunlockinits^0 == 0 /\ pdo^0-pdo^post11 == 0 /\ -dname^post11+dname^0 == 0 /\ i^0-i^post11 == 0 /\ status^0-status^post11 == 0 /\ -num^post11+num^0 == 0 /\ pdolen^0-pdolen^post11 == 0), cost: 1 Second rule: l6 -> l2 : conditional^0'=conditional^post10, dname^0'=dname^post10, i^0'=i^post10, iocreatedevice^0'=iocreatedevice^post10, num^0'=num^post10, pdo^0'=pdo^post10, pdolen^0'=pdolen^post10, ppblockinits^0'=ppblockinits^post10, ppbunlockinits^0'=ppbunlockinits^post10, status^0'=status^post10, (0 == 0 /\ ppbunlockinits^post10 == 0 /\ num^0-num^post10 == 0 /\ status^post10 == 0 /\ -1+ppblockinits^post10 == 0 /\ -conditional^post10+conditional^0 == 0 /\ iocreatedevice^post10 == 0 /\ -dname^post10+dname^0 == 0 /\ -pdo^post10+pdo^0 == 0), cost: 1 New rule: l7 -> l2 : conditional^0'=conditional^post10, dname^0'=dname^post10, i^0'=i^post10, iocreatedevice^0'=iocreatedevice^post10, num^0'=num^post10, pdo^0'=pdo^post10, pdolen^0'=pdolen^post10, ppblockinits^0'=ppblockinits^post10, ppbunlockinits^0'=ppbunlockinits^post10, status^0'=status^post10, (0 == 0 /\ ppbunlockinits^post10 == 0 /\ -conditional^post10+conditional^post11 == 0 /\ -conditional^post11+conditional^0 == 0 /\ -iocreatedevice^post11+iocreatedevice^0 == 0 /\ num^post11-num^post10 == 0 /\ -ppblockinits^post11+ppblockinits^0 == 0 /\ -ppbunlockinits^post11+ppbunlockinits^0 == 0 /\ status^post10 == 0 /\ pdo^0-pdo^post11 == 0 /\ -dname^post11+dname^0 == 0 /\ -1+ppblockinits^post10 == 0 /\ i^0-i^post11 == 0 /\ iocreatedevice^post10 == 0 /\ status^0-status^post11 == 0 /\ -num^post11+num^0 == 0 /\ -pdo^post10+pdo^post11 == 0 /\ -dname^post10+dname^post11 == 0 /\ pdolen^0-pdolen^post11 == 0), cost: 1 Applied deletion Removed the following rules: 9 10 Simplified Transitions Start location: l7 Program variables: conditional^0 dname^0 i^0 iocreatedevice^0 num^0 pdo^0 pdolen^0 ppblockinits^0 ppbunlockinits^0 status^0 12: l0 -> l1 : -1+conditional^0 <= 0, cost: 1 13: l0 -> l2 : num^0'=1+num^0, 2-conditional^0 <= 0, cost: 1 16: l1 -> l4 : num^0'=0, ppbunlockinits^0'=1, T, cost: 1 19: l2 -> l1 : status^0'=0, pdolen^0-i^0 <= 0, cost: 1 20: l2 -> l5 : dname^0'=dname^post9, ppblockinits^0'=1, status^0'=0, 1-pdolen^0+i^0 <= 0, cost: 1 14: l3 -> l2 : i^0'=1+i^0, iocreatedevice^0'=0, status^0'=1, -1+conditional^0 <= 0, cost: 1 15: l3 -> l0 : conditional^0'=conditional^post4, iocreatedevice^0'=0, pdo^0'=0, 2-conditional^0 <= 0, cost: 1 17: l5 -> l1 : dname^0 <= 0, cost: 1 18: l5 -> l3 : conditional^0'=conditional^post7, iocreatedevice^0'=1, 1-dname^0 <= 0, cost: 1 21: l7 -> l2 : i^0'=i^post10, iocreatedevice^0'=0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : conditional^0'=conditional^post1, dname^0'=dname^post1, i^0'=i^post1, iocreatedevice^0'=iocreatedevice^post1, num^0'=num^post1, pdo^0'=pdo^post1, pdolen^0'=pdolen^post1, ppblockinits^0'=ppblockinits^post1, ppbunlockinits^0'=ppbunlockinits^post1, status^0'=status^post1, (-ppbunlockinits^post1+ppbunlockinits^0 == 0 /\ pdo^0-pdo^post1 == 0 /\ -1+conditional^0 <= 0 /\ -num^post1+num^0 == 0 /\ ppblockinits^0-ppblockinits^post1 == 0 /\ -conditional^post1+conditional^0 == 0 /\ pdolen^0-pdolen^post1 == 0 /\ -dname^post1+dname^0 == 0 /\ i^0-i^post1 == 0 /\ -iocreatedevice^post1+iocreatedevice^0 == 0 /\ status^0-status^post1 == 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 propagated equality ppbunlockinits^post1 = ppbunlockinits^0 propagated equality pdo^post1 = pdo^0 propagated equality num^post1 = num^0 propagated equality ppblockinits^post1 = ppblockinits^0 propagated equality conditional^post1 = conditional^0 propagated equality pdolen^post1 = pdolen^0 propagated equality dname^post1 = dname^0 propagated equality i^post1 = i^0 propagated equality iocreatedevice^post1 = iocreatedevice^0 propagated equality status^post1 = status^0 Simplified Guard Original rule: l0 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 New rule: l0 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, -1+conditional^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, -1+conditional^0 <= 0, cost: 1 New rule: l0 -> l1 : -1+conditional^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : conditional^0'=conditional^post2, dname^0'=dname^post2, i^0'=i^post2, iocreatedevice^0'=iocreatedevice^post2, num^0'=num^post2, pdo^0'=pdo^post2, pdolen^0'=pdolen^post2, ppblockinits^0'=ppblockinits^post2, ppbunlockinits^0'=ppbunlockinits^post2, status^0'=status^post2, (pdolen^0-pdolen^post2 == 0 /\ 2-conditional^0 <= 0 /\ -1+num^post2-num^0 == 0 /\ pdo^0-pdo^post2 == 0 /\ -ppbunlockinits^post2+ppbunlockinits^0 == 0 /\ ppblockinits^0-ppblockinits^post2 == 0 /\ -conditional^post2+conditional^0 == 0 /\ -iocreatedevice^post2+iocreatedevice^0 == 0 /\ i^0-i^post2 == 0 /\ -status^post2+status^0 == 0 /\ -dname^post2+dname^0 == 0), cost: 1 New rule: l0 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=1+num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ 2-conditional^0 <= 0), cost: 1 propagated equality pdolen^post2 = pdolen^0 propagated equality num^post2 = 1+num^0 propagated equality pdo^post2 = pdo^0 propagated equality ppbunlockinits^post2 = ppbunlockinits^0 propagated equality ppblockinits^post2 = ppblockinits^0 propagated equality conditional^post2 = conditional^0 propagated equality iocreatedevice^post2 = iocreatedevice^0 propagated equality i^post2 = i^0 propagated equality status^post2 = status^0 propagated equality dname^post2 = dname^0 Simplified Guard Original rule: l0 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=1+num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ 2-conditional^0 <= 0), cost: 1 New rule: l0 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=1+num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, 2-conditional^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=1+num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, 2-conditional^0 <= 0, cost: 1 New rule: l0 -> l2 : num^0'=1+num^0, 2-conditional^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : conditional^0'=conditional^post3, dname^0'=dname^post3, i^0'=i^post3, iocreatedevice^0'=iocreatedevice^post3, num^0'=num^post3, pdo^0'=pdo^post3, pdolen^0'=pdolen^post3, ppblockinits^0'=ppblockinits^post3, ppbunlockinits^0'=ppbunlockinits^post3, status^0'=status^post3, (-conditional^post3+conditional^0 == 0 /\ iocreatedevice^post3 == 0 /\ -dname^post3+dname^0 == 0 /\ pdo^0-pdo^post3 == 0 /\ -1+conditional^0 <= 0 /\ -1-i^0+i^post3 == 0 /\ -1+status^post3 == 0 /\ ppblockinits^0-ppblockinits^post3 == 0 /\ -num^post3+num^0 == 0 /\ pdolen^0-pdolen^post3 == 0 /\ ppbunlockinits^0-ppbunlockinits^post3 == 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=1+i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=1, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 propagated equality conditional^post3 = conditional^0 propagated equality iocreatedevice^post3 = 0 propagated equality dname^post3 = dname^0 propagated equality pdo^post3 = pdo^0 propagated equality i^post3 = 1+i^0 propagated equality status^post3 = 1 propagated equality ppblockinits^post3 = ppblockinits^0 propagated equality num^post3 = num^0 propagated equality pdolen^post3 = pdolen^0 propagated equality ppbunlockinits^post3 = ppbunlockinits^0 Simplified Guard Original rule: l3 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=1+i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=1, (0 == 0 /\ -1+conditional^0 <= 0), cost: 1 New rule: l3 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=1+i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=1, -1+conditional^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=1+i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=1, -1+conditional^0 <= 0, cost: 1 New rule: l3 -> l2 : i^0'=1+i^0, iocreatedevice^0'=0, status^0'=1, -1+conditional^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : conditional^0'=conditional^post4, dname^0'=dname^post4, i^0'=i^post4, iocreatedevice^0'=iocreatedevice^post4, num^0'=num^post4, pdo^0'=pdo^post4, pdolen^0'=pdolen^post4, ppblockinits^0'=ppblockinits^post4, ppbunlockinits^0'=ppbunlockinits^post4, status^0'=status^post4, (0 == 0 /\ num^0-num^post4 == 0 /\ pdo^post4 == 0 /\ 2-conditional^0 <= 0 /\ i^0-i^post4 == 0 /\ iocreatedevice^post4 == 0 /\ -ppbunlockinits^post4+ppbunlockinits^0 == 0 /\ -dname^post4+dname^0 == 0 /\ ppblockinits^0-ppblockinits^post4 == 0 /\ -status^post4+status^0 == 0 /\ pdolen^0-pdolen^post4 == 0), cost: 1 New rule: l3 -> l0 : conditional^0'=conditional^post4, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ 2-conditional^0 <= 0), cost: 1 propagated equality num^post4 = num^0 propagated equality pdo^post4 = 0 propagated equality i^post4 = i^0 propagated equality iocreatedevice^post4 = 0 propagated equality ppbunlockinits^post4 = ppbunlockinits^0 propagated equality dname^post4 = dname^0 propagated equality ppblockinits^post4 = ppblockinits^0 propagated equality status^post4 = status^0 propagated equality pdolen^post4 = pdolen^0 Simplified Guard Original rule: l3 -> l0 : conditional^0'=conditional^post4, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ 2-conditional^0 <= 0), cost: 1 New rule: l3 -> l0 : conditional^0'=conditional^post4, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, 2-conditional^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : conditional^0'=conditional^post4, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, 2-conditional^0 <= 0, cost: 1 New rule: l3 -> l0 : conditional^0'=conditional^post4, iocreatedevice^0'=0, pdo^0'=0, 2-conditional^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l4 : conditional^0'=conditional^post5, dname^0'=dname^post5, i^0'=i^post5, iocreatedevice^0'=iocreatedevice^post5, num^0'=num^post5, pdo^0'=pdo^post5, pdolen^0'=pdolen^post5, ppblockinits^0'=ppblockinits^post5, ppbunlockinits^0'=ppbunlockinits^post5, status^0'=status^post5, (i^0-i^post5 == 0 /\ conditional^0-conditional^post5 == 0 /\ num^post5 == 0 /\ status^0-status^post5 == 0 /\ pdolen^0-pdolen^post5 == 0 /\ pdo^0-pdo^post5 == 0 /\ -dname^post5+dname^0 == 0 /\ iocreatedevice^0-iocreatedevice^post5 == 0 /\ -ppblockinits^post5+ppblockinits^0 == 0 /\ -1+ppbunlockinits^post5 == 0), cost: 1 New rule: l1 -> l4 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=1, status^0'=status^0, 0 == 0, cost: 1 propagated equality i^post5 = i^0 propagated equality conditional^post5 = conditional^0 propagated equality num^post5 = 0 propagated equality status^post5 = status^0 propagated equality pdolen^post5 = pdolen^0 propagated equality pdo^post5 = pdo^0 propagated equality dname^post5 = dname^0 propagated equality iocreatedevice^post5 = iocreatedevice^0 propagated equality ppblockinits^post5 = ppblockinits^0 propagated equality ppbunlockinits^post5 = 1 Simplified Guard Original rule: l1 -> l4 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=1, status^0'=status^0, 0 == 0, cost: 1 New rule: l1 -> l4 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=1, status^0'=status^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=1, status^0'=status^0, T, cost: 1 New rule: l1 -> l4 : num^0'=0, ppbunlockinits^0'=1, T, cost: 1 Propagated Equalities Original rule: l5 -> l1 : conditional^0'=conditional^post6, dname^0'=dname^post6, i^0'=i^post6, iocreatedevice^0'=iocreatedevice^post6, num^0'=num^post6, pdo^0'=pdo^post6, pdolen^0'=pdolen^post6, ppblockinits^0'=ppblockinits^post6, ppbunlockinits^0'=ppbunlockinits^post6, status^0'=status^post6, (ppblockinits^0-ppblockinits^post6 == 0 /\ -pdolen^post6+pdolen^0 == 0 /\ -ppbunlockinits^post6+ppbunlockinits^0 == 0 /\ -conditional^post6+conditional^0 == 0 /\ i^0-i^post6 == 0 /\ -num^post6+num^0 == 0 /\ pdo^0-pdo^post6 == 0 /\ -dname^post6+dname^0 == 0 /\ status^0-status^post6 == 0 /\ iocreatedevice^0-iocreatedevice^post6 == 0 /\ dname^0 <= 0), cost: 1 New rule: l5 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ dname^0 <= 0), cost: 1 propagated equality ppblockinits^post6 = ppblockinits^0 propagated equality pdolen^post6 = pdolen^0 propagated equality ppbunlockinits^post6 = ppbunlockinits^0 propagated equality conditional^post6 = conditional^0 propagated equality i^post6 = i^0 propagated equality num^post6 = num^0 propagated equality pdo^post6 = pdo^0 propagated equality dname^post6 = dname^0 propagated equality status^post6 = status^0 propagated equality iocreatedevice^post6 = iocreatedevice^0 Simplified Guard Original rule: l5 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ dname^0 <= 0), cost: 1 New rule: l5 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, dname^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, dname^0 <= 0, cost: 1 New rule: l5 -> l1 : dname^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l3 : conditional^0'=conditional^post7, dname^0'=dname^post7, i^0'=i^post7, iocreatedevice^0'=iocreatedevice^post7, num^0'=num^post7, pdo^0'=pdo^post7, pdolen^0'=pdolen^post7, ppblockinits^0'=ppblockinits^post7, ppbunlockinits^0'=ppbunlockinits^post7, status^0'=status^post7, (0 == 0 /\ pdolen^0-pdolen^post7 == 0 /\ pdo^0-pdo^post7 == 0 /\ -1+iocreatedevice^post7 == 0 /\ -ppbunlockinits^post7+ppbunlockinits^0 == 0 /\ ppblockinits^0-ppblockinits^post7 == 0 /\ -dname^post7+dname^0 == 0 /\ -num^post7+num^0 == 0 /\ -status^post7+status^0 == 0 /\ i^0-i^post7 == 0 /\ 1-dname^0 <= 0), cost: 1 New rule: l5 -> l3 : conditional^0'=conditional^post7, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=1, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ 1-dname^0 <= 0), cost: 1 propagated equality pdolen^post7 = pdolen^0 propagated equality pdo^post7 = pdo^0 propagated equality iocreatedevice^post7 = 1 propagated equality ppbunlockinits^post7 = ppbunlockinits^0 propagated equality ppblockinits^post7 = ppblockinits^0 propagated equality dname^post7 = dname^0 propagated equality num^post7 = num^0 propagated equality status^post7 = status^0 propagated equality i^post7 = i^0 Simplified Guard Original rule: l5 -> l3 : conditional^0'=conditional^post7, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=1, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, (0 == 0 /\ 1-dname^0 <= 0), cost: 1 New rule: l5 -> l3 : conditional^0'=conditional^post7, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=1, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, 1-dname^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l3 : conditional^0'=conditional^post7, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=1, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=status^0, 1-dname^0 <= 0, cost: 1 New rule: l5 -> l3 : conditional^0'=conditional^post7, iocreatedevice^0'=1, 1-dname^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l1 : conditional^0'=conditional^post8, dname^0'=dname^post8, i^0'=i^post8, iocreatedevice^0'=iocreatedevice^post8, num^0'=num^post8, pdo^0'=pdo^post8, pdolen^0'=pdolen^post8, ppblockinits^0'=ppblockinits^post8, ppbunlockinits^0'=ppbunlockinits^post8, status^0'=status^post8, (pdolen^0-pdolen^post8 == 0 /\ status^post8 == 0 /\ -conditional^post8+conditional^0 == 0 /\ pdolen^0-i^0 <= 0 /\ pdo^0-pdo^post8 == 0 /\ -ppbunlockinits^post8+ppbunlockinits^0 == 0 /\ -dname^post8+dname^0 == 0 /\ ppblockinits^0-ppblockinits^post8 == 0 /\ -num^post8+num^0 == 0 /\ -iocreatedevice^post8+iocreatedevice^0 == 0 /\ i^0-i^post8 == 0), cost: 1 New rule: l2 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, (0 == 0 /\ pdolen^0-i^0 <= 0), cost: 1 propagated equality pdolen^post8 = pdolen^0 propagated equality status^post8 = 0 propagated equality conditional^post8 = conditional^0 propagated equality pdo^post8 = pdo^0 propagated equality ppbunlockinits^post8 = ppbunlockinits^0 propagated equality dname^post8 = dname^0 propagated equality ppblockinits^post8 = ppblockinits^0 propagated equality num^post8 = num^0 propagated equality iocreatedevice^post8 = iocreatedevice^0 propagated equality i^post8 = i^0 Simplified Guard Original rule: l2 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, (0 == 0 /\ pdolen^0-i^0 <= 0), cost: 1 New rule: l2 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, pdolen^0-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l1 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=ppblockinits^0, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, pdolen^0-i^0 <= 0, cost: 1 New rule: l2 -> l1 : status^0'=0, pdolen^0-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l5 : conditional^0'=conditional^post9, dname^0'=dname^post9, i^0'=i^post9, iocreatedevice^0'=iocreatedevice^post9, num^0'=num^post9, pdo^0'=pdo^post9, pdolen^0'=pdolen^post9, ppblockinits^0'=ppblockinits^post9, ppbunlockinits^0'=ppbunlockinits^post9, status^0'=status^post9, (0 == 0 /\ -iocreatedevice^post9+iocreatedevice^0 == 0 /\ -num^post9+num^0 == 0 /\ pdo^0-pdo^post9 == 0 /\ status^post9 == 0 /\ -conditional^post9+conditional^0 == 0 /\ 1-pdolen^0+i^0 <= 0 /\ pdolen^0-pdolen^post9 == 0 /\ ppbunlockinits^0-ppbunlockinits^post9 == 0 /\ i^0-i^post9 == 0 /\ -1+ppblockinits^post9 == 0), cost: 1 New rule: l2 -> l5 : conditional^0'=conditional^0, dname^0'=dname^post9, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=1, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, (0 == 0 /\ 1-pdolen^0+i^0 <= 0), cost: 1 propagated equality iocreatedevice^post9 = iocreatedevice^0 propagated equality num^post9 = num^0 propagated equality pdo^post9 = pdo^0 propagated equality status^post9 = 0 propagated equality conditional^post9 = conditional^0 propagated equality pdolen^post9 = pdolen^0 propagated equality ppbunlockinits^post9 = ppbunlockinits^0 propagated equality i^post9 = i^0 propagated equality ppblockinits^post9 = 1 Simplified Guard Original rule: l2 -> l5 : conditional^0'=conditional^0, dname^0'=dname^post9, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=1, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, (0 == 0 /\ 1-pdolen^0+i^0 <= 0), cost: 1 New rule: l2 -> l5 : conditional^0'=conditional^0, dname^0'=dname^post9, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=1, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, 1-pdolen^0+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l5 : conditional^0'=conditional^0, dname^0'=dname^post9, i^0'=i^0, iocreatedevice^0'=iocreatedevice^0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^0, ppblockinits^0'=1, ppbunlockinits^0'=ppbunlockinits^0, status^0'=0, 1-pdolen^0+i^0 <= 0, cost: 1 New rule: l2 -> l5 : dname^0'=dname^post9, ppblockinits^0'=1, status^0'=0, 1-pdolen^0+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l2 : conditional^0'=conditional^post10, dname^0'=dname^post10, i^0'=i^post10, iocreatedevice^0'=iocreatedevice^post10, num^0'=num^post10, pdo^0'=pdo^post10, pdolen^0'=pdolen^post10, ppblockinits^0'=ppblockinits^post10, ppbunlockinits^0'=ppbunlockinits^post10, status^0'=status^post10, (0 == 0 /\ ppbunlockinits^post10 == 0 /\ -conditional^post10+conditional^post11 == 0 /\ -conditional^post11+conditional^0 == 0 /\ -iocreatedevice^post11+iocreatedevice^0 == 0 /\ num^post11-num^post10 == 0 /\ -ppblockinits^post11+ppblockinits^0 == 0 /\ -ppbunlockinits^post11+ppbunlockinits^0 == 0 /\ status^post10 == 0 /\ pdo^0-pdo^post11 == 0 /\ -dname^post11+dname^0 == 0 /\ -1+ppblockinits^post10 == 0 /\ i^0-i^post11 == 0 /\ iocreatedevice^post10 == 0 /\ status^0-status^post11 == 0 /\ -num^post11+num^0 == 0 /\ -pdo^post10+pdo^post11 == 0 /\ -dname^post10+dname^post11 == 0 /\ pdolen^0-pdolen^post11 == 0), cost: 1 New rule: l7 -> l2 : conditional^0'=conditional^post11, dname^0'=dname^post11, i^0'=i^post10, iocreatedevice^0'=0, num^0'=num^post11, pdo^0'=pdo^post11, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, (0 == 0 /\ -conditional^post11+conditional^0 == 0 /\ -iocreatedevice^post11+iocreatedevice^0 == 0 /\ -ppblockinits^post11+ppblockinits^0 == 0 /\ -ppbunlockinits^post11+ppbunlockinits^0 == 0 /\ pdo^0-pdo^post11 == 0 /\ -dname^post11+dname^0 == 0 /\ i^0-i^post11 == 0 /\ status^0-status^post11 == 0 /\ -num^post11+num^0 == 0 /\ pdolen^0-pdolen^post11 == 0), cost: 1 propagated equality ppbunlockinits^post10 = 0 propagated equality conditional^post10 = conditional^post11 propagated equality num^post10 = num^post11 propagated equality status^post10 = 0 propagated equality ppblockinits^post10 = 1 propagated equality iocreatedevice^post10 = 0 propagated equality pdo^post10 = pdo^post11 propagated equality dname^post10 = dname^post11 Propagated Equalities Original rule: l7 -> l2 : conditional^0'=conditional^post11, dname^0'=dname^post11, i^0'=i^post10, iocreatedevice^0'=0, num^0'=num^post11, pdo^0'=pdo^post11, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, (0 == 0 /\ -conditional^post11+conditional^0 == 0 /\ -iocreatedevice^post11+iocreatedevice^0 == 0 /\ -ppblockinits^post11+ppblockinits^0 == 0 /\ -ppbunlockinits^post11+ppbunlockinits^0 == 0 /\ pdo^0-pdo^post11 == 0 /\ -dname^post11+dname^0 == 0 /\ i^0-i^post11 == 0 /\ status^0-status^post11 == 0 /\ -num^post11+num^0 == 0 /\ pdolen^0-pdolen^post11 == 0), cost: 1 New rule: l7 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^post10, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, 0 == 0, cost: 1 propagated equality conditional^post11 = conditional^0 propagated equality iocreatedevice^post11 = iocreatedevice^0 propagated equality ppblockinits^post11 = ppblockinits^0 propagated equality ppbunlockinits^post11 = ppbunlockinits^0 propagated equality pdo^post11 = pdo^0 propagated equality dname^post11 = dname^0 propagated equality i^post11 = i^0 propagated equality status^post11 = status^0 propagated equality num^post11 = num^0 propagated equality pdolen^post11 = pdolen^0 Simplified Guard Original rule: l7 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^post10, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, 0 == 0, cost: 1 New rule: l7 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^post10, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l2 : conditional^0'=conditional^0, dname^0'=dname^0, i^0'=i^post10, iocreatedevice^0'=0, num^0'=num^0, pdo^0'=pdo^0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, T, cost: 1 New rule: l7 -> l2 : i^0'=i^post10, iocreatedevice^0'=0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, T, cost: 1 Step with 21 Trace 21[T] Blocked [{}, {}] Step with 19 Trace 21[T], 19[(pdolen^0-i^0 <= 0)] Blocked [{}, {}, {}] Step with 16 Trace 21[T], 19[(pdolen^0-i^0 <= 0)], 16[T] Blocked [{}, {}, {}, {}] Backtrack Trace 21[T], 19[(pdolen^0-i^0 <= 0)] Blocked [{}, {}, {16[T]}] Backtrack Trace 21[T] Blocked [{}, {19[T]}] Step with 20 Trace 21[T], 20[(1-pdolen^0+i^0 <= 0)] Blocked [{}, {19[T]}, {}] Step with 17 Trace 21[T], 20[(1-pdolen^0+i^0 <= 0)], 17[(dname^0 <= 0)] Blocked [{}, {19[T]}, {}, {}] Step with 16 Trace 21[T], 20[(1-pdolen^0+i^0 <= 0)], 17[(dname^0 <= 0)], 16[T] Blocked [{}, {19[T]}, {}, {}, {}] Backtrack Trace 21[T], 20[(1-pdolen^0+i^0 <= 0)], 17[(dname^0 <= 0)] Blocked [{}, {19[T]}, {}, {16[T]}] Backtrack Trace 21[T], 20[(1-pdolen^0+i^0 <= 0)] Blocked [{}, {19[T]}, {17[T]}] Step with 18 Trace 21[T], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)] Blocked [{}, {19[T]}, {17[T]}, {}] Step with 14 Trace 21[T], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 14[(-1+conditional^0 <= 0)] Blocked [{}, {19[T]}, {17[T]}, {}, {}] Accelerate Start location: l7 Program variables: conditional^0 dname^0 i^0 iocreatedevice^0 num^0 pdo^0 pdolen^0 ppblockinits^0 ppbunlockinits^0 status^0 12: l0 -> l1 : -1+conditional^0 <= 0, cost: 1 13: l0 -> l2 : num^0'=1+num^0, 2-conditional^0 <= 0, cost: 1 16: l1 -> l4 : num^0'=0, ppbunlockinits^0'=1, T, cost: 1 19: l2 -> l1 : status^0'=0, pdolen^0-i^0 <= 0, cost: 1 20: l2 -> l5 : dname^0'=dname^post9, ppblockinits^0'=1, status^0'=0, 1-pdolen^0+i^0 <= 0, cost: 1 22: l2 -> l2 : conditional^0'=conditional^post71, dname^0'=dname^post91, i^0'=i^0+n, iocreatedevice^0'=0, ppblockinits^0'=1, status^0'=1, (1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0), cost: 1 14: l3 -> l2 : i^0'=1+i^0, iocreatedevice^0'=0, status^0'=1, -1+conditional^0 <= 0, cost: 1 15: l3 -> l0 : conditional^0'=conditional^post4, iocreatedevice^0'=0, pdo^0'=0, 2-conditional^0 <= 0, cost: 1 17: l5 -> l1 : dname^0 <= 0, cost: 1 18: l5 -> l3 : conditional^0'=conditional^post7, iocreatedevice^0'=1, 1-dname^0 <= 0, cost: 1 21: l7 -> l2 : i^0'=i^post10, iocreatedevice^0'=0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : conditional^0'=conditional^post71, dname^0'=dname^post91, i^0'=1+i^0, iocreatedevice^0'=0, ppblockinits^0'=1, status^0'=1, (-1+conditional^post71 <= 0 /\ 1-dname^post91 <= 0 /\ 1-pdolen^0+i^0 <= 0), cost: 1 New rule: l2 -> l2 : conditional^0'=conditional^post71, dname^0'=dname^post91, i^0'=i^0+n, iocreatedevice^0'=0, ppblockinits^0'=1, status^0'=1, (1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0), cost: 1 1-conditional^post71 >= 0 [0]: monotonic increase yields 1-conditional^post71 >= 0 -1+dname^post91 >= 0 [0]: monotonic increase yields -1+dname^post91 >= 0 -1+pdolen^0-i^0 >= 0 [0]: montonic decrease yields pdolen^0-i^0-n >= 0 -1+pdolen^0-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+pdolen^0-i^0 >= 0) Replacement map: {1-conditional^post71 >= 0 -> 1-conditional^post71 >= 0, -1+dname^post91 >= 0 -> -1+dname^post91 >= 0, -1+pdolen^0-i^0 >= 0 -> pdolen^0-i^0-n >= 0} Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)] Blocked [{}, {19[T]}, {22[T]}] Step with 19 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 19[(pdolen^0-i^0 <= 0)] Blocked [{}, {19[T]}, {22[T]}, {}] Step with 16 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 19[(pdolen^0-i^0 <= 0)], 16[T] Blocked [{}, {19[T]}, {22[T]}, {}, {}] Backtrack Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 19[(pdolen^0-i^0 <= 0)] Blocked [{}, {19[T]}, {22[T]}, {16[T]}] Backtrack Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}] Step with 20 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}] Step with 18 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {}] Step with 14 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 14[(-1+conditional^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {}, {}] Covered Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {14[T]}] Step with 15 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 15[(2-conditional^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {14[T]}, {}] Step with 12 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 15[(2-conditional^0 <= 0)], 12[(-1+conditional^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {14[T]}, {}, {}] Step with 16 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 15[(2-conditional^0 <= 0)], 12[(-1+conditional^0 <= 0)], 16[T] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {14[T]}, {}, {}, {}] Backtrack Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 15[(2-conditional^0 <= 0)], 12[(-1+conditional^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {14[T]}, {}, {16[T]}] Backtrack Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 15[(2-conditional^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {14[T]}, {12[T]}] Step with 13 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 20[(1-pdolen^0+i^0 <= 0)], 18[(1-dname^0 <= 0)], 15[(2-conditional^0 <= 0)], 13[(2-conditional^0 <= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {}, {14[T]}, {12[T]}, {}] Nonterm Start location: l7 Program variables: conditional^0 dname^0 i^0 iocreatedevice^0 num^0 pdo^0 pdolen^0 ppblockinits^0 ppbunlockinits^0 status^0 12: l0 -> l1 : -1+conditional^0 <= 0, cost: 1 13: l0 -> l2 : num^0'=1+num^0, 2-conditional^0 <= 0, cost: 1 16: l1 -> l4 : num^0'=0, ppbunlockinits^0'=1, T, cost: 1 19: l2 -> l1 : status^0'=0, pdolen^0-i^0 <= 0, cost: 1 20: l2 -> l5 : dname^0'=dname^post9, ppblockinits^0'=1, status^0'=0, 1-pdolen^0+i^0 <= 0, cost: 1 22: l2 -> l2 : conditional^0'=conditional^post71, dname^0'=dname^post91, i^0'=i^0+n, iocreatedevice^0'=0, ppblockinits^0'=1, status^0'=1, (1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0), cost: 1 23: l2 -> LoAT_sink : (-1+n2 >= 0 /\ -1+dname^post92 >= 0 /\ -1+pdolen^0-i^0 >= 0 /\ -2+conditional^post41 >= 0), cost: NONTERM 24: l2 -> l2 : conditional^0'=conditional^post41, dname^0'=dname^post92, iocreatedevice^0'=0, num^0'=n2+num^0, pdo^0'=0, ppblockinits^0'=1, status^0'=0, (-1+n2 >= 0 /\ -1+dname^post92 >= 0 /\ -1+pdolen^0-i^0 >= 0 /\ -2+conditional^post41 >= 0), cost: 1 14: l3 -> l2 : i^0'=1+i^0, iocreatedevice^0'=0, status^0'=1, -1+conditional^0 <= 0, cost: 1 15: l3 -> l0 : conditional^0'=conditional^post4, iocreatedevice^0'=0, pdo^0'=0, 2-conditional^0 <= 0, cost: 1 17: l5 -> l1 : dname^0 <= 0, cost: 1 18: l5 -> l3 : conditional^0'=conditional^post7, iocreatedevice^0'=1, 1-dname^0 <= 0, cost: 1 21: l7 -> l2 : i^0'=i^post10, iocreatedevice^0'=0, pdolen^0'=pdolen^post10, ppblockinits^0'=1, ppbunlockinits^0'=0, status^0'=0, T, cost: 1 Certificate of Non-Termination Original rule: l2 -> l2 : conditional^0'=conditional^post41, dname^0'=dname^post92, iocreatedevice^0'=0, num^0'=1+num^0, pdo^0'=0, ppblockinits^0'=1, status^0'=0, (1-pdolen^0+i^0 <= 0 /\ 1-dname^post92 <= 0 /\ 2-conditional^post41 <= 0), cost: 1 New rule: l2 -> LoAT_sink : (-1+n2 >= 0 /\ -1+dname^post92 >= 0 /\ -1+pdolen^0-i^0 >= 0 /\ -2+conditional^post41 >= 0), cost: NONTERM -1+dname^post92 >= 0 [0]: monotonic increase yields -1+dname^post92 >= 0 -1+pdolen^0-i^0 >= 0 [0]: monotonic increase yields -1+pdolen^0-i^0 >= 0 -2+conditional^post41 >= 0 [0]: monotonic increase yields -2+conditional^post41 >= 0 Replacement map: {-1+dname^post92 >= 0 -> -1+dname^post92 >= 0, -1+pdolen^0-i^0 >= 0 -> -1+pdolen^0-i^0 >= 0, -2+conditional^post41 >= 0 -> -2+conditional^post41 >= 0} Loop Acceleration Original rule: l2 -> l2 : conditional^0'=conditional^post41, dname^0'=dname^post92, iocreatedevice^0'=0, num^0'=1+num^0, pdo^0'=0, ppblockinits^0'=1, status^0'=0, (1-pdolen^0+i^0 <= 0 /\ 1-dname^post92 <= 0 /\ 2-conditional^post41 <= 0), cost: 1 New rule: l2 -> l2 : conditional^0'=conditional^post41, dname^0'=dname^post92, iocreatedevice^0'=0, num^0'=n2+num^0, pdo^0'=0, ppblockinits^0'=1, status^0'=0, (-1+n2 >= 0 /\ -1+dname^post92 >= 0 /\ -1+pdolen^0-i^0 >= 0 /\ -2+conditional^post41 >= 0), cost: 1 -1+dname^post92 >= 0 [0]: monotonic increase yields -1+dname^post92 >= 0 -1+pdolen^0-i^0 >= 0 [0]: monotonic increase yields -1+pdolen^0-i^0 >= 0 -2+conditional^post41 >= 0 [0]: monotonic increase yields -2+conditional^post41 >= 0 Replacement map: {-1+dname^post92 >= 0 -> -1+dname^post92 >= 0, -1+pdolen^0-i^0 >= 0 -> -1+pdolen^0-i^0 >= 0, -2+conditional^post41 >= 0 -> -2+conditional^post41 >= 0} Step with 23 Trace 21[T], 22[(1-conditional^post71 >= 0 /\ pdolen^0-i^0-n >= 0 /\ -1+dname^post91 >= 0 /\ -1+n >= 0)], 23[(-1+n2 >= 0 /\ -1+dname^post92 >= 0 /\ -1+pdolen^0-i^0 >= 0 /\ -2+conditional^post41 >= 0)] Blocked [{}, {19[T]}, {19[T], 22[T]}, {23[T]}] Refute Counterexample [ conditional^0=0 dname^0=0 i^0=0 iocreatedevice^0=0 num^0=0 pdo^0=0 pdolen^0=2 ppblockinits^0=1 ppbunlockinits^0=0 status^0=0 ] 21 [ conditional^0=0 dname^0=1 i^0=1 iocreatedevice^0=0 num^0=0 pdo^0=0 pdolen^0=2 ppblockinits^0=1 ppbunlockinits^0=0 status^0=1 ] 22 [ conditional^0=0 dname^0=0 i^0=i^0 iocreatedevice^0=iocreatedevice^0 num^0=0 pdo^0=0 pdolen^0=pdolen^0 ppblockinits^0=ppblockinits^0 ppbunlockinits^0=ppbunlockinits^0 status^0=status^0 ] 23 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b