WORST_CASE(?,O(n^2))
* Step 1: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. eratos0(A,B) -> eratos(-1 + A,B) True (?,1)
1. eratos1(A,B) -> filter(B,-1 + A) True (?,1)
2. eratos(A,B) -> c2(eratos0(A,C),eratos1(A,C)) [A >= 1] (?,1)
3. outfilter(A,B) -> outfilter(A,-1 + B) [B >= 1] (?,1)
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[0->{2},1->{4},2->{0,1},3->{3},4->{4},5->{2}]
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [3]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. eratos0(A,B) -> eratos(-1 + A,B) True (?,1)
1. eratos1(A,B) -> filter(B,-1 + A) True (?,1)
2. eratos(A,B) -> c2(eratos0(A,C),eratos1(A,C)) [A >= 1] (?,1)
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[0->{2},1->{4},2->{0,1},4->{4},5->{2}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, 1 + A, .+ 1) (<0,0,B>, B, .= 0)
(<1,0,A>, B, .= 0) (<1,0,B>, 1 + A, .+ 1)
(<2,0,A>, A, .= 0) (<2,0,B>, ?, .?)
(<2,1,A>, A, .= 0) (<2,1,B>, ?, .?)
(<4,0,A>, A, .= 0) (<4,0,B>, 1 + B, .+ 1)
(<5,0,A>, A, .= 0) (<5,0,B>, B, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. eratos0(A,B) -> eratos(-1 + A,B) True (?,1)
1. eratos1(A,B) -> filter(B,-1 + A) True (?,1)
2. eratos(A,B) -> c2(eratos0(A,C),eratos1(A,C)) [A >= 1] (?,1)
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[0->{2},1->{4},2->{0,1},4->{4},5->{2}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, ?) (<1,0,B>, ?)
(<2,0,A>, ?) (<2,0,B>, ?)
(<2,1,A>, ?) (<2,1,B>, ?)
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, ?) (<5,0,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, ?) (<1,0,B>, ?)
(<2,0,A>, ?) (<2,0,B>, ?)
(<2,1,A>, ?) (<2,1,B>, ?)
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
* Step 4: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. eratos0(A,B) -> eratos(-1 + A,B) True (?,1)
1. eratos1(A,B) -> filter(B,-1 + A) True (?,1)
2. eratos(A,B) -> c2(eratos0(A,C),eratos1(A,C)) [A >= 1] (?,1)
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[0->{2},1->{4},2->{0,1},4->{4},5->{2}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, ?) (<1,0,B>, ?)
(<2,0,A>, ?) (<2,0,B>, ?)
(<2,1,A>, ?) (<2,1,B>, ?)
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
+ Applied Processor:
ChainProcessor False [0,1,2,4,5]
+ Details:
We chained rule 2 to obtain the rules [6] .
* Step 5: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. eratos0(A,B) -> eratos(-1 + A,B) True (?,1)
1. eratos1(A,B) -> filter(B,-1 + A) True (?,1)
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
6. eratos(A,B) -> c2(eratos(-1 + A,C),eratos1(A,C)) [A >= 1] (?,2)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[0->{6},1->{4},4->{4},5->{6},6->{1,6}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, ?) (<1,0,B>, ?)
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<6,0,A>, ?) (<6,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [0]
* Step 6: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. eratos1(A,B) -> filter(B,-1 + A) True (?,1)
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
6. eratos(A,B) -> c2(eratos(-1 + A,C),eratos1(A,C)) [A >= 1] (?,2)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[1->{4},4->{4},5->{6},6->{1,6}]
Sizebounds:
(<1,0,A>, ?) (<1,0,B>, ?)
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<6,0,A>, ?) (<6,0,B>, ?)
+ Applied Processor:
ChainProcessor False [1,4,5,6]
+ Details:
We chained rule 6 to obtain the rules [7] .
* Step 7: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. eratos1(A,B) -> filter(B,-1 + A) True (?,1)
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
7. eratos(A,B) -> c2(eratos(-1 + A,C),filter(C,-2 + A)) [A >= 1] (?,3)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[1->{4},4->{4},5->{7},7->{4,7}]
Sizebounds:
(<1,0,A>, ?) (<1,0,B>, ?)
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<7,0,A>, ?) (<7,0,B>, ?)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [1]
* Step 8: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
7. eratos(A,B) -> c2(eratos(-1 + A,C),filter(C,-2 + A)) [A >= 1] (?,3)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[4->{4},5->{7},7->{4,7}]
Sizebounds:
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<7,0,A>, ?) (<7,0,B>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<4,0,A>, A, .= 0) (<4,0,B>, 1 + B, .+ 1)
(<5,0,A>, A, .= 0) (<5,0,B>, B, .= 0)
(<7,0,A>, 1 + A, .+ 1) (<7,0,B>, ?, .?)
(<7,1,A>, ?, .?) (<7,1,B>, 2 + A, .+ 2)
* Step 9: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
7. eratos(A,B) -> c2(eratos(-1 + A,C),filter(C,-2 + A)) [A >= 1] (?,3)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[4->{4},5->{7},7->{4,7}]
Sizebounds:
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, ?) (<5,0,B>, ?)
(<7,0,A>, ?) (<7,0,B>, ?)
(<7,1,A>, ?) (<7,1,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<7,0,A>, ?) (<7,0,B>, ?)
(<7,1,A>, ?) (<7,1,B>, ?)
* Step 10: LocationConstraintsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
7. eratos(A,B) -> c2(eratos(-1 + A,C),filter(C,-2 + A)) [A >= 1] (?,3)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[4->{4},5->{7},7->{4,7}]
Sizebounds:
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<7,0,A>, ?) (<7,0,B>, ?)
(<7,1,A>, ?) (<7,1,B>, ?)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 4 : True 5 : True 7 : True .
* Step 11: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (?,1)
5. start(A,B) -> eratos(A,B) True (1,1)
7. eratos(A,B) -> c2(eratos(-1 + A,C),filter(C,-2 + A)) [A >= 1] (?,3)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[4->{4},5->{7},7->{4,7}]
Sizebounds:
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<7,0,A>, ?) (<7,0,B>, ?)
(<7,1,A>, ?) (<7,1,B>, ?)
+ Applied Processor:
LoopRecurrenceProcessor [7]
+ Details:
Applying the recurrence pattern linear * f to the expression A yields the solution A + A^2 .
* Step 12: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (A + A^2,1)
5. start(A,B) -> eratos(A,B) True (1,1)
7. eratos(A,B) -> c2(eratos(-1 + A,C),filter(C,-2 + A)) [A >= 1] (A + A^2,3)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[4->{4},5->{7},7->{4,7}]
Sizebounds:
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<7,0,A>, ?) (<7,0,B>, ?)
(<7,1,A>, ?) (<7,1,B>, ?)
+ Applied Processor:
LoopRecurrenceProcessor [4]
+ Details:
Applying the recurrence pattern linear * f to the expression B yields the solution B .
* Step 13: UnsatPaths WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. filter(A,B) -> filter(A,-1 + B) [B >= 1] (A + A^2,1)
5. start(A,B) -> eratos(A,B) True (1,1)
7. eratos(A,B) -> c2(eratos(-1 + A,C),filter(C,-2 + A)) [A >= 1] (A + A^2,3)
Signature:
{(eratos,2);(eratos0,2);(eratos1,2);(filter,2);(outfilter,2);(start,2)}
Flow Graph:
[4->{4},5->{7},7->{4,7}]
Sizebounds:
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, A) (<5,0,B>, B)
(<7,0,A>, ?) (<7,0,B>, ?)
(<7,1,A>, ?) (<7,1,B>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))