WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalterminatestart(A,B,C) -> evalterminateentryin(A,B,C) True (1,1)
1. evalterminateentryin(A,B,C) -> evalterminatebb1in(B,A,C) True (?,1)
2. evalterminatebb1in(A,B,C) -> evalterminatebbin(A,B,C) [100 >= B && A >= C] (?,1)
3. evalterminatebb1in(A,B,C) -> evalterminatereturnin(A,B,C) [B >= 101] (?,1)
4. evalterminatebb1in(A,B,C) -> evalterminatereturnin(A,B,C) [C >= 1 + A] (?,1)
5. evalterminatebbin(A,B,C) -> evalterminatebb1in(-1 + A,C,1 + B) True (?,1)
6. evalterminatereturnin(A,B,C) -> evalterminatestop(A,B,C) True (?,1)
Signature:
{(evalterminatebb1in,3)
;(evalterminatebbin,3)
;(evalterminateentryin,3)
;(evalterminatereturnin,3)
;(evalterminatestart,3)
;(evalterminatestop,3)}
Flow Graph:
[0->{1},1->{2,3,4},2->{5},3->{6},4->{6},5->{2,3,4},6->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, A, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>, C, .= 0)
(<1,0,A>, B, .= 0) (<1,0,B>, A, .= 0) (<1,0,C>, C, .= 0)
(<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, C, .= 0)
(<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0) (<4,0,C>, C, .= 0)
(<5,0,A>, 1 + A, .+ 1) (<5,0,B>, C, .= 0) (<5,0,C>, 1 + B, .+ 1)
(<6,0,A>, A, .= 0) (<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalterminatestart(A,B,C) -> evalterminateentryin(A,B,C) True (1,1)
1. evalterminateentryin(A,B,C) -> evalterminatebb1in(B,A,C) True (?,1)
2. evalterminatebb1in(A,B,C) -> evalterminatebbin(A,B,C) [100 >= B && A >= C] (?,1)
3. evalterminatebb1in(A,B,C) -> evalterminatereturnin(A,B,C) [B >= 101] (?,1)
4. evalterminatebb1in(A,B,C) -> evalterminatereturnin(A,B,C) [C >= 1 + A] (?,1)
5. evalterminatebbin(A,B,C) -> evalterminatebb1in(-1 + A,C,1 + B) True (?,1)
6. evalterminatereturnin(A,B,C) -> evalterminatestop(A,B,C) True (?,1)
Signature:
{(evalterminatebb1in,3)
;(evalterminatebbin,3)
;(evalterminateentryin,3)
;(evalterminatereturnin,3)
;(evalterminatestart,3)
;(evalterminatestop,3)}
Flow Graph:
[0->{1},1->{2,3,4},2->{5},3->{6},4->{6},5->{2,3,4},6->{}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?)
(<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?)
(<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?)
(<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?)
(<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?)
(<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?)
(<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C)
(<1,0,A>, B) (<1,0,B>, A) (<1,0,C>, C)
(<2,0,A>, ?) (<2,0,B>, 100) (<2,0,C>, 100 + C)
(<3,0,A>, ?) (<3,0,B>, 100 + A + C) (<3,0,C>, 100 + C)
(<4,0,A>, ?) (<4,0,B>, 100 + A + C) (<4,0,C>, 100 + C)
(<5,0,A>, ?) (<5,0,B>, 100 + C) (<5,0,C>, 100)
(<6,0,A>, ?) (<6,0,B>, 100 + A + C) (<6,0,C>, 100 + C)
* Step 3: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalterminatestart(A,B,C) -> evalterminateentryin(A,B,C) True (1,1)
1. evalterminateentryin(A,B,C) -> evalterminatebb1in(B,A,C) True (?,1)
2. evalterminatebb1in(A,B,C) -> evalterminatebbin(A,B,C) [100 >= B && A >= C] (?,1)
3. evalterminatebb1in(A,B,C) -> evalterminatereturnin(A,B,C) [B >= 101] (?,1)
4. evalterminatebb1in(A,B,C) -> evalterminatereturnin(A,B,C) [C >= 1 + A] (?,1)
5. evalterminatebbin(A,B,C) -> evalterminatebb1in(-1 + A,C,1 + B) True (?,1)
6. evalterminatereturnin(A,B,C) -> evalterminatestop(A,B,C) True (?,1)
Signature:
{(evalterminatebb1in,3)
;(evalterminatebbin,3)
;(evalterminateentryin,3)
;(evalterminatereturnin,3)
;(evalterminatestart,3)
;(evalterminatestop,3)}
Flow Graph:
[0->{1},1->{2,3,4},2->{5},3->{6},4->{6},5->{2,3,4},6->{}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C)
(<1,0,A>, B) (<1,0,B>, A) (<1,0,C>, C)
(<2,0,A>, ?) (<2,0,B>, 100) (<2,0,C>, 100 + C)
(<3,0,A>, ?) (<3,0,B>, 100 + A + C) (<3,0,C>, 100 + C)
(<4,0,A>, ?) (<4,0,B>, 100 + A + C) (<4,0,C>, 100 + C)
(<5,0,A>, ?) (<5,0,B>, 100 + C) (<5,0,C>, 100)
(<6,0,A>, ?) (<6,0,B>, 100 + A + C) (<6,0,C>, 100 + C)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3,4,6]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalterminatestart(A,B,C) -> evalterminateentryin(A,B,C) True (1,1)
1. evalterminateentryin(A,B,C) -> evalterminatebb1in(B,A,C) True (?,1)
2. evalterminatebb1in(A,B,C) -> evalterminatebbin(A,B,C) [100 >= B && A >= C] (?,1)
5. evalterminatebbin(A,B,C) -> evalterminatebb1in(-1 + A,C,1 + B) True (?,1)
Signature:
{(evalterminatebb1in,3)
;(evalterminatebbin,3)
;(evalterminateentryin,3)
;(evalterminatereturnin,3)
;(evalterminatestart,3)
;(evalterminatestop,3)}
Flow Graph:
[0->{1},1->{2},2->{5},5->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C)
(<1,0,A>, B) (<1,0,B>, A) (<1,0,C>, C)
(<2,0,A>, ?) (<2,0,B>, 100) (<2,0,C>, 100 + C)
(<5,0,A>, ?) (<5,0,B>, 100 + C) (<5,0,C>, 100)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalterminatebb1in) = 101 + x1 + -1*x2 + -1*x3
p(evalterminatebbin) = 100 + x1 + -1*x2 + -1*x3
p(evalterminateentryin) = 101 + -1*x1 + x2 + -1*x3
p(evalterminatestart) = 101 + -1*x1 + x2 + -1*x3
The following rules are strictly oriented:
[100 >= B && A >= C] ==>
evalterminatebb1in(A,B,C) = 101 + A + -1*B + -1*C
> 100 + A + -1*B + -1*C
= evalterminatebbin(A,B,C)
The following rules are weakly oriented:
True ==>
evalterminatestart(A,B,C) = 101 + -1*A + B + -1*C
>= 101 + -1*A + B + -1*C
= evalterminateentryin(A,B,C)
True ==>
evalterminateentryin(A,B,C) = 101 + -1*A + B + -1*C
>= 101 + -1*A + B + -1*C
= evalterminatebb1in(B,A,C)
True ==>
evalterminatebbin(A,B,C) = 100 + A + -1*B + -1*C
>= 99 + A + -1*B + -1*C
= evalterminatebb1in(-1 + A,C,1 + B)
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalterminatestart(A,B,C) -> evalterminateentryin(A,B,C) True (1,1)
1. evalterminateentryin(A,B,C) -> evalterminatebb1in(B,A,C) True (?,1)
2. evalterminatebb1in(A,B,C) -> evalterminatebbin(A,B,C) [100 >= B && A >= C] (101 + A + B + C,1)
5. evalterminatebbin(A,B,C) -> evalterminatebb1in(-1 + A,C,1 + B) True (?,1)
Signature:
{(evalterminatebb1in,3)
;(evalterminatebbin,3)
;(evalterminateentryin,3)
;(evalterminatereturnin,3)
;(evalterminatestart,3)
;(evalterminatestop,3)}
Flow Graph:
[0->{1},1->{2},2->{5},5->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C)
(<1,0,A>, B) (<1,0,B>, A) (<1,0,C>, C)
(<2,0,A>, ?) (<2,0,B>, 100) (<2,0,C>, 100 + C)
(<5,0,A>, ?) (<5,0,B>, 100 + C) (<5,0,C>, 100)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 6: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalterminatestart(A,B,C) -> evalterminateentryin(A,B,C) True (1,1)
1. evalterminateentryin(A,B,C) -> evalterminatebb1in(B,A,C) True (1,1)
2. evalterminatebb1in(A,B,C) -> evalterminatebbin(A,B,C) [100 >= B && A >= C] (101 + A + B + C,1)
5. evalterminatebbin(A,B,C) -> evalterminatebb1in(-1 + A,C,1 + B) True (101 + A + B + C,1)
Signature:
{(evalterminatebb1in,3)
;(evalterminatebbin,3)
;(evalterminateentryin,3)
;(evalterminatereturnin,3)
;(evalterminatestart,3)
;(evalterminatestop,3)}
Flow Graph:
[0->{1},1->{2},2->{5},5->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C)
(<1,0,A>, B) (<1,0,B>, A) (<1,0,C>, C)
(<2,0,A>, ?) (<2,0,B>, 100) (<2,0,C>, 100 + C)
(<5,0,A>, ?) (<5,0,B>, 100 + C) (<5,0,C>, 100)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))