WORST_CASE(?,O(n^1))
* Step 1: TrivialSCCs WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C) -> f3(-1*A,B,C) True (?,1)
1. f3(A,B,C) -> f7(0,D,C) [A = 0] (?,1)
2. f4(A,B,C) -> f7(0,D,C) [A = 0] (?,1)
3. f6(A,B,C) -> f4(A,B,1) [A >= 1] (1,1)
4. f3(A,B,C) -> f4(-1 + -1*A,B,1) [0 >= 1 + A && 0 >= C] (?,1)
5. f3(A,B,C) -> f4(-1 + -1*A,B,1) [0 >= 1 + A && C >= 2] (?,1)
6. f3(A,B,C) -> f4(-1 + -1*A,B,1) [A >= 1 && 0 >= C] (?,1)
7. f3(A,B,C) -> f4(-1 + -1*A,B,1) [A >= 1 && C >= 2] (?,1)
8. f4(A,B,C) -> f3(1 + -1*A,B,0) [0 >= 1 + A && C = 1] (?,1)
9. f4(A,B,C) -> f3(1 + -1*A,B,0) [A >= 1 && C = 1] (?,1)
10. f5(A,B,C) -> f3(1 + -1*A,B,0) [0 >= 1 + A && C = 1] (?,1)
11. f5(A,B,C) -> f3(1 + -1*A,B,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,3);(f3,3);(f4,3);(f5,3);(f6,3);(f7,3)}
Flow Graph:
[0->{1,4,5,6,7},1->{},2->{},3->{2,8,9},4->{2,8,9},5->{2,8,9},6->{2,8,9},7->{2,8,9},8->{1,4,5,6,7},9->{1,4
,5,6,7},10->{1,4,5,6,7},11->{1,4,5,6,7}]
+ Applied Processor:
TrivialSCCs
+ Details:
All trivial SCCs of the transition graph admit timebound 1.
* Step 2: RestrictVarsProcessor WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,B,C) -> f3(-1*A,B,C) True (1,1)
1. f3(A,B,C) -> f7(0,D,C) [A = 0] (?,1)
2. f4(A,B,C) -> f7(0,D,C) [A = 0] (?,1)
3. f6(A,B,C) -> f4(A,B,1) [A >= 1] (1,1)
4. f3(A,B,C) -> f4(-1 + -1*A,B,1) [0 >= 1 + A && 0 >= C] (?,1)
5. f3(A,B,C) -> f4(-1 + -1*A,B,1) [0 >= 1 + A && C >= 2] (?,1)
6. f3(A,B,C) -> f4(-1 + -1*A,B,1) [A >= 1 && 0 >= C] (?,1)
7. f3(A,B,C) -> f4(-1 + -1*A,B,1) [A >= 1 && C >= 2] (?,1)
8. f4(A,B,C) -> f3(1 + -1*A,B,0) [0 >= 1 + A && C = 1] (?,1)
9. f4(A,B,C) -> f3(1 + -1*A,B,0) [A >= 1 && C = 1] (?,1)
10. f5(A,B,C) -> f3(1 + -1*A,B,0) [0 >= 1 + A && C = 1] (1,1)
11. f5(A,B,C) -> f3(1 + -1*A,B,0) [A >= 1 && C = 1] (1,1)
Signature:
{(f0,3);(f3,3);(f4,3);(f5,3);(f6,3);(f7,3)}
Flow Graph:
[0->{1,4,5,6,7},1->{},2->{},3->{2,8,9},4->{2,8,9},5->{2,8,9},6->{2,8,9},7->{2,8,9},8->{1,4,5,6,7},9->{1,4
,5,6,7},10->{1,4,5,6,7},11->{1,4,5,6,7}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [B] .
* Step 3: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. f0(A,C) -> f3(-1*A,C) True (?,1)
1. f3(A,C) -> f7(0,C) [A = 0] (?,1)
2. f4(A,C) -> f7(0,C) [A = 0] (?,1)
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
5. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && C >= 2] (?,1)
6. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && 0 >= C] (?,1)
7. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && C >= 2] (?,1)
8. f4(A,C) -> f3(1 + -1*A,0) [0 >= 1 + A && C = 1] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
10. f5(A,C) -> f3(1 + -1*A,0) [0 >= 1 + A && C = 1] (?,1)
11. f5(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[0->{1,4,5,6,7},1->{},2->{},3->{2,8,9},4->{2,8,9},5->{2,8,9},6->{2,8,9},7->{2,8,9},8->{1,4,5,6,7},9->{1,4
,5,6,7},10->{1,4,5,6,7},11->{1,4,5,6,7}]
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [0,10,11]
* Step 4: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. f3(A,C) -> f7(0,C) [A = 0] (?,1)
2. f4(A,C) -> f7(0,C) [A = 0] (?,1)
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
5. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && C >= 2] (?,1)
6. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && 0 >= C] (?,1)
7. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && C >= 2] (?,1)
8. f4(A,C) -> f3(1 + -1*A,0) [0 >= 1 + A && C = 1] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[1->{},2->{},3->{2,8,9},4->{2,8,9},5->{2,8,9},6->{2,8,9},7->{2,8,9},8->{1,4,5,6,7},9->{1,4,5,6,7}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<1,0,A>, 0, .= 0) (<1,0,C>, C, .= 0)
(<2,0,A>, 0, .= 0) (<2,0,C>, C, .= 0)
(<3,0,A>, A, .= 0) (<3,0,C>, 1, .= 1)
(<4,0,A>, 1 + A, .+ 1) (<4,0,C>, 1, .= 1)
(<5,0,A>, 1 + A, .+ 1) (<5,0,C>, 1, .= 1)
(<6,0,A>, 1 + A, .+ 1) (<6,0,C>, 1, .= 1)
(<7,0,A>, 1 + A, .+ 1) (<7,0,C>, 1, .= 1)
(<8,0,A>, 1 + A, .+ 1) (<8,0,C>, 0, .= 0)
(<9,0,A>, 1 + A, .+ 1) (<9,0,C>, 0, .= 0)
* Step 5: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. f3(A,C) -> f7(0,C) [A = 0] (?,1)
2. f4(A,C) -> f7(0,C) [A = 0] (?,1)
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
5. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && C >= 2] (?,1)
6. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && 0 >= C] (?,1)
7. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && C >= 2] (?,1)
8. f4(A,C) -> f3(1 + -1*A,0) [0 >= 1 + A && C = 1] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[1->{},2->{},3->{2,8,9},4->{2,8,9},5->{2,8,9},6->{2,8,9},7->{2,8,9},8->{1,4,5,6,7},9->{1,4,5,6,7}]
Sizebounds:
(<1,0,A>, ?) (<1,0,C>, ?)
(<2,0,A>, ?) (<2,0,C>, ?)
(<3,0,A>, ?) (<3,0,C>, ?)
(<4,0,A>, ?) (<4,0,C>, ?)
(<5,0,A>, ?) (<5,0,C>, ?)
(<6,0,A>, ?) (<6,0,C>, ?)
(<7,0,A>, ?) (<7,0,C>, ?)
(<8,0,A>, ?) (<8,0,C>, ?)
(<9,0,A>, ?) (<9,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<1,0,A>, 0) (<1,0,C>, 0)
(<2,0,A>, 0) (<2,0,C>, 1)
(<3,0,A>, A) (<3,0,C>, 1)
(<4,0,A>, 0) (<4,0,C>, 1)
(<5,0,A>, 0) (<5,0,C>, 1)
(<6,0,A>, ?) (<6,0,C>, 1)
(<7,0,A>, ?) (<7,0,C>, 1)
(<8,0,A>, 2) (<8,0,C>, 0)
(<9,0,A>, ?) (<9,0,C>, 0)
* Step 6: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. f3(A,C) -> f7(0,C) [A = 0] (?,1)
2. f4(A,C) -> f7(0,C) [A = 0] (?,1)
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
5. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && C >= 2] (?,1)
6. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && 0 >= C] (?,1)
7. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && C >= 2] (?,1)
8. f4(A,C) -> f3(1 + -1*A,0) [0 >= 1 + A && C = 1] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[1->{},2->{},3->{2,8,9},4->{2,8,9},5->{2,8,9},6->{2,8,9},7->{2,8,9},8->{1,4,5,6,7},9->{1,4,5,6,7}]
Sizebounds:
(<1,0,A>, 0) (<1,0,C>, 0)
(<2,0,A>, 0) (<2,0,C>, 1)
(<3,0,A>, A) (<3,0,C>, 1)
(<4,0,A>, 0) (<4,0,C>, 1)
(<5,0,A>, 0) (<5,0,C>, 1)
(<6,0,A>, ?) (<6,0,C>, 1)
(<7,0,A>, ?) (<7,0,C>, 1)
(<8,0,A>, 2) (<8,0,C>, 0)
(<9,0,A>, ?) (<9,0,C>, 0)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(3,2)
,(3,8)
,(4,8)
,(5,8)
,(6,2)
,(6,9)
,(7,2)
,(7,9)
,(8,1)
,(8,4)
,(8,5)
,(8,7)
,(9,5)
,(9,6)
,(9,7)]
* Step 7: UnreachableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. f3(A,C) -> f7(0,C) [A = 0] (?,1)
2. f4(A,C) -> f7(0,C) [A = 0] (?,1)
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
5. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && C >= 2] (?,1)
6. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && 0 >= C] (?,1)
7. f3(A,C) -> f4(-1 + -1*A,1) [A >= 1 && C >= 2] (?,1)
8. f4(A,C) -> f3(1 + -1*A,0) [0 >= 1 + A && C = 1] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[1->{},2->{},3->{9},4->{2,9},5->{2,9},6->{8},7->{8},8->{6},9->{1,4}]
Sizebounds:
(<1,0,A>, 0) (<1,0,C>, 0)
(<2,0,A>, 0) (<2,0,C>, 1)
(<3,0,A>, A) (<3,0,C>, 1)
(<4,0,A>, 0) (<4,0,C>, 1)
(<5,0,A>, 0) (<5,0,C>, 1)
(<6,0,A>, ?) (<6,0,C>, 1)
(<7,0,A>, ?) (<7,0,C>, 1)
(<8,0,A>, 2) (<8,0,C>, 0)
(<9,0,A>, ?) (<9,0,C>, 0)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [5,6,7,8]
* Step 8: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
1. f3(A,C) -> f7(0,C) [A = 0] (?,1)
2. f4(A,C) -> f7(0,C) [A = 0] (?,1)
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[1->{},2->{},3->{9},4->{2,9},9->{1,4}]
Sizebounds:
(<1,0,A>, 0) (<1,0,C>, 0)
(<2,0,A>, 0) (<2,0,C>, 1)
(<3,0,A>, A) (<3,0,C>, 1)
(<4,0,A>, 0) (<4,0,C>, 1)
(<9,0,A>, ?) (<9,0,C>, 0)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [1,2]
* Step 9: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (?,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[3->{9},4->{9},9->{4}]
Sizebounds:
(<3,0,A>, A) (<3,0,C>, 1)
(<4,0,A>, 0) (<4,0,C>, 1)
(<9,0,A>, ?) (<9,0,C>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f3) = -1 + -1*x1
p(f4) = x1
p(f6) = x1
The following rules are strictly oriented:
[A >= 1 && C = 1] ==>
f4(A,C) = A
> -2 + A
= f3(1 + -1*A,0)
The following rules are weakly oriented:
[A >= 1] ==>
f6(A,C) = A
>= A
= f4(A,1)
[0 >= 1 + A && 0 >= C] ==>
f3(A,C) = -1 + -1*A
>= -1 + -1*A
= f4(-1 + -1*A,1)
* Step 10: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (?,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (A,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[3->{9},4->{9},9->{4}]
Sizebounds:
(<3,0,A>, A) (<3,0,C>, 1)
(<4,0,A>, 0) (<4,0,C>, 1)
(<9,0,A>, ?) (<9,0,C>, 0)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 11: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
3. f6(A,C) -> f4(A,1) [A >= 1] (1,1)
4. f3(A,C) -> f4(-1 + -1*A,1) [0 >= 1 + A && 0 >= C] (A,1)
9. f4(A,C) -> f3(1 + -1*A,0) [A >= 1 && C = 1] (A,1)
Signature:
{(f0,2);(f3,2);(f4,2);(f5,2);(f6,2);(f7,2)}
Flow Graph:
[3->{9},4->{9},9->{4}]
Sizebounds:
(<3,0,A>, A) (<3,0,C>, 1)
(<4,0,A>, 0) (<4,0,C>, 1)
(<9,0,A>, ?) (<9,0,C>, 0)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))