WORST_CASE(?,O(n^1))
* Step 1: UnsatRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
3. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E = 40 && C = 100 && A = 0 && B = 0] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
5. lbl91(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 && 39 >= E && E >= 1 && 40 >= E && C = 100 && A = 0 && B = 0] (?,1)
6. lbl91(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 && 39 >= E && E >= 1 && 40 >= E && C = 100 && A = 0 && B = 0] (?,1)
7. lbl111(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E >= 40 && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
8. lbl111(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 2 && 41 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{3,4,5,6},1->{7,8,9,10},2->{7,8,9,10},3->{},4->{3,4,5,6},5->{7,8,9,10},6->{7,8,9,10},7->{},8->{3,4,5
,6},9->{7,8,9,10},10->{7,8,9,10},11->{0,1,2}]
+ Applied Processor:
UnsatRules
+ Details:
The following transitions have unsatisfiable constraints and are removed: [5,6]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
3. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E = 40 && C = 100 && A = 0 && B = 0] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
7. lbl111(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E >= 40 && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
8. lbl111(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 2 && 41 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{3,4},1->{7,8,9,10},2->{7,8,9,10},3->{},4->{3,4},7->{},8->{3,4},9->{7,8,9,10},10->{7,8,9,10},11->{0,1
,2}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, 100, .= 100) (< 0,0,D>, D, .= 0) (< 0,0,E>, 1, .= 1) (< 0,0,F>, F, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, 100, .= 100) (< 1,0,D>, D, .= 0) (< 1,0,E>, 2, .= 2) (< 1,0,F>, F, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, 100, .= 100) (< 2,0,D>, D, .= 0) (< 2,0,E>, 2, .= 2) (< 2,0,F>, F, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, F, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, 40, .= 40) (< 4,0,F>, F, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, 40, .= 40) (< 8,0,F>, F, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, 41, .= 41) (< 9,0,F>, F, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, 41, .= 41) (<10,0,F>, F, .= 0)
(<11,0,A>, B, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, D, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, F, .= 0) (<11,0,F>, F, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
3. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E = 40 && C = 100 && A = 0 && B = 0] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
7. lbl111(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E >= 40 && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
8. lbl111(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 2 && 41 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{3,4},1->{7,8,9,10},2->{7,8,9,10},3->{},4->{3,4},7->{},8->{3,4},9->{7,8,9,10},10->{7,8,9,10},11->{0,1
,2}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, 100) (< 3,0,D>, D) (< 3,0,E>, 40) (< 3,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, 100) (< 7,0,D>, D) (< 7,0,E>, 41) (< 7,0,F>, F)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 100) (< 8,0,D>, D) (< 8,0,E>, 40) (< 8,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
* Step 4: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
3. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E = 40 && C = 100 && A = 0 && B = 0] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
7. lbl111(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E >= 40 && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
8. lbl111(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 2 && 41 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{3,4},1->{7,8,9,10},2->{7,8,9,10},3->{},4->{3,4},7->{},8->{3,4},9->{7,8,9,10},10->{7,8,9,10},11->{0,1
,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, 100) (< 3,0,D>, D) (< 3,0,E>, 40) (< 3,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, 100) (< 7,0,D>, D) (< 7,0,E>, 41) (< 7,0,F>, F)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 100) (< 8,0,D>, D) (< 8,0,E>, 40) (< 8,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,3)
,(1,7)
,(1,8)
,(1,10)
,(2,7)
,(2,8)
,(2,9)
,(9,8)
,(9,10)
,(10,8)
,(10,9)]
* Step 5: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
3. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E = 40 && C = 100 && A = 0 && B = 0] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
7. lbl111(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E >= 40 && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
8. lbl111(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 2 && 41 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{4},1->{9},2->{10},3->{},4->{3,4},7->{},8->{3,4},9->{7,9},10->{7,10},11->{0,1,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, 100) (< 3,0,D>, D) (< 3,0,E>, 40) (< 3,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, 100) (< 7,0,D>, D) (< 7,0,E>, 41) (< 7,0,F>, F)
(< 8,0,A>, B) (< 8,0,B>, B) (< 8,0,C>, 100) (< 8,0,D>, D) (< 8,0,E>, 40) (< 8,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [8]
* Step 6: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
3. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E = 40 && C = 100 && A = 0 && B = 0] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
7. lbl111(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [E >= 40 && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{4},1->{9},2->{10},3->{},4->{3,4},7->{},9->{7,9},10->{7,10},11->{0,1,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 3,0,A>, B) (< 3,0,B>, B) (< 3,0,C>, 100) (< 3,0,D>, D) (< 3,0,E>, 40) (< 3,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 7,0,A>, B) (< 7,0,B>, B) (< 7,0,C>, 100) (< 7,0,D>, D) (< 7,0,E>, 41) (< 7,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3,7]
* Step 7: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{4},1->{9},2->{10},4->{4},9->{9},10->{10},11->{0,1,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = 43 + -1*x5
p(lbl91) = 42
p(start) = 42
p(start0) = 42
The following rules are strictly oriented:
[B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] ==>
lbl111(A,B,C,D,E,F) = 43 + -1*E
> 41 + -1*E
= lbl111(A,B,C,D,2 + E,F)
The following rules are weakly oriented:
[A = 0 && B = 0 && C = D && E = F] ==>
start(A,B,C,D,E,F) = 42
>= 42
= lbl91(A,B,100,D,1,F)
[0 >= 1 + B && A = B && C = D && E = F] ==>
start(A,B,C,D,E,F) = 42
>= 41
= lbl111(A,B,100,D,2,F)
[B >= 1 && A = B && C = D && E = F] ==>
start(A,B,C,D,E,F) = 42
>= 41
= lbl111(A,B,100,D,2,F)
[39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] ==>
lbl91(A,B,C,D,E,F) = 42
>= 42
= lbl91(A,B,C,D,1 + E,F)
[0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] ==>
lbl111(A,B,C,D,E,F) = 43 + -1*E
>= 41 + -1*E
= lbl111(A,B,C,D,2 + E,F)
True ==>
start0(A,B,C,D,E,F) = 42
>= 42
= start(B,B,D,D,F,F)
* Step 8: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (?,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (?,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (?,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (42,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{4},1->{9},2->{10},4->{4},9->{9},10->{10},11->{0,1,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 9: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (1,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (1,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (1,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (?,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (42,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{4},1->{9},2->{10},4->{4},9->{9},10->{10},11->{0,1,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = 19 + -99*x1 + -1*x5
p(lbl91) = -83 + -99*x1 + x3
p(start) = 18 + -99*x1
p(start0) = 18 + -99*x2
The following rules are strictly oriented:
[A = 0 && B = 0 && C = D && E = F] ==>
start(A,B,C,D,E,F) = 18 + -99*A
> 17 + -99*A
= lbl91(A,B,100,D,1,F)
[0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] ==>
lbl111(A,B,C,D,E,F) = 19 + -99*A + -1*E
> 17 + -99*A + -1*E
= lbl111(A,B,C,D,2 + E,F)
The following rules are weakly oriented:
[0 >= 1 + B && A = B && C = D && E = F] ==>
start(A,B,C,D,E,F) = 18 + -99*A
>= 17 + -99*A
= lbl111(A,B,100,D,2,F)
[B >= 1 && A = B && C = D && E = F] ==>
start(A,B,C,D,E,F) = 18 + -99*A
>= 17 + -99*A
= lbl111(A,B,100,D,2,F)
[39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] ==>
lbl91(A,B,C,D,E,F) = -83 + -99*A + C
>= -83 + -99*A + C
= lbl91(A,B,C,D,1 + E,F)
[B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] ==>
lbl111(A,B,C,D,E,F) = 19 + -99*A + -1*E
>= 17 + -99*A + -1*E
= lbl111(A,B,C,D,2 + E,F)
True ==>
start0(A,B,C,D,E,F) = 18 + -99*B
>= 18 + -99*B
= start(B,B,D,D,F,F)
* Step 10: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (1,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (1,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (1,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (?,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (18 + 99*B,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (42,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{4},1->{9},2->{10},4->{4},9->{9},10->{10},11->{0,1,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(lbl111) = 39
p(lbl91) = 41 + -1*x5
p(start) = 40
p(start0) = 40
The following rules are strictly oriented:
[0 >= 1 + B && A = B && C = D && E = F] ==>
start(A,B,C,D,E,F) = 40
> 39
= lbl111(A,B,100,D,2,F)
[B >= 1 && A = B && C = D && E = F] ==>
start(A,B,C,D,E,F) = 40
> 39
= lbl111(A,B,100,D,2,F)
[39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] ==>
lbl91(A,B,C,D,E,F) = 41 + -1*E
> 40 + -1*E
= lbl91(A,B,C,D,1 + E,F)
The following rules are weakly oriented:
[A = 0 && B = 0 && C = D && E = F] ==>
start(A,B,C,D,E,F) = 40
>= 40
= lbl91(A,B,100,D,1,F)
[0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] ==>
lbl111(A,B,C,D,E,F) = 39
>= 39
= lbl111(A,B,C,D,2 + E,F)
[B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] ==>
lbl111(A,B,C,D,E,F) = 39
>= 39
= lbl111(A,B,C,D,2 + E,F)
True ==>
start0(A,B,C,D,E,F) = 40
>= 40
= start(B,B,D,D,F,F)
* Step 11: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. start(A,B,C,D,E,F) -> lbl91(A,B,100,D,1,F) [A = 0 && B = 0 && C = D && E = F] (1,1)
1. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [0 >= 1 + B && A = B && C = D && E = F] (1,1)
2. start(A,B,C,D,E,F) -> lbl111(A,B,100,D,2,F) [B >= 1 && A = B && C = D && E = F] (1,1)
4. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,D,1 + E,F) [39 >= E && E >= 1 && 40 >= E && A = 0 && C = 100 && B = 0] (40,1)
9. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [0 >= 1 + B && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (18 + 99*B,1)
10. lbl111(A,B,C,D,E,F) -> lbl111(A,B,C,D,2 + E,F) [B >= 1 && 39 >= E && E >= 2 && 41 >= E && C = 100 && A = B] (42,1)
11. start0(A,B,C,D,E,F) -> start(B,B,D,D,F,F) True (1,1)
Signature:
{(lbl111,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
Flow Graph:
[0->{4},1->{9},2->{10},4->{4},9->{9},10->{10},11->{0,1,2}]
Sizebounds:
(< 0,0,A>, B) (< 0,0,B>, B) (< 0,0,C>, 100) (< 0,0,D>, D) (< 0,0,E>, 1) (< 0,0,F>, F)
(< 1,0,A>, B) (< 1,0,B>, B) (< 1,0,C>, 100) (< 1,0,D>, D) (< 1,0,E>, 2) (< 1,0,F>, F)
(< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, 100) (< 2,0,D>, D) (< 2,0,E>, 2) (< 2,0,F>, F)
(< 4,0,A>, B) (< 4,0,B>, B) (< 4,0,C>, 100) (< 4,0,D>, D) (< 4,0,E>, 40) (< 4,0,F>, F)
(< 9,0,A>, B) (< 9,0,B>, B) (< 9,0,C>, 100) (< 9,0,D>, D) (< 9,0,E>, 41) (< 9,0,F>, F)
(<10,0,A>, B) (<10,0,B>, B) (<10,0,C>, 100) (<10,0,D>, D) (<10,0,E>, 41) (<10,0,F>, F)
(<11,0,A>, B) (<11,0,B>, B) (<11,0,C>, D) (<11,0,D>, D) (<11,0,E>, F) (<11,0,F>, F)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))