WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1)
3. evalwcet2bb5in(A,B) -> evalwcet2returnin(A,B) [A >= 5] (?,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (?,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
9. evalwcet2returnin(A,B) -> evalwcet2stop(A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{4,5,6},8->{2,3},9->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, A, .= 0) (<0,0,B>, B, .= 0)
(<1,0,A>, A, .= 0) (<1,0,B>, B, .= 0)
(<2,0,A>, A, .= 0) (<2,0,B>, 0, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0)
(<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0)
(<5,0,A>, A, .= 0) (<5,0,B>, B, .= 0)
(<6,0,A>, A, .= 0) (<6,0,B>, B, .= 0)
(<7,0,A>, A, .= 0) (<7,0,B>, 1 + B, .+ 1)
(<8,0,A>, 1 + A, .+ 1) (<8,0,B>, B, .= 0)
(<9,0,A>, A, .= 0) (<9,0,B>, B, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1)
3. evalwcet2bb5in(A,B) -> evalwcet2returnin(A,B) [A >= 5] (?,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (?,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
9. evalwcet2returnin(A,B) -> evalwcet2stop(A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{4,5,6},8->{2,3},9->{}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?)
(<1,0,A>, ?) (<1,0,B>, ?)
(<2,0,A>, ?) (<2,0,B>, ?)
(<3,0,A>, ?) (<3,0,B>, ?)
(<4,0,A>, ?) (<4,0,B>, ?)
(<5,0,A>, ?) (<5,0,B>, ?)
(<6,0,A>, ?) (<6,0,B>, ?)
(<7,0,A>, ?) (<7,0,B>, ?)
(<8,0,A>, ?) (<8,0,B>, ?)
(<9,0,A>, ?) (<9,0,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<3,0,A>, ?) (<3,0,B>, 9 + B)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
(<9,0,A>, ?) (<9,0,B>, 9 + B)
* Step 3: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1)
3. evalwcet2bb5in(A,B) -> evalwcet2returnin(A,B) [A >= 5] (?,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (?,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
9. evalwcet2returnin(A,B) -> evalwcet2stop(A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{4,5,6},8->{2,3},9->{}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<3,0,A>, ?) (<3,0,B>, 9 + B)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
(<9,0,A>, ?) (<9,0,B>, 9 + B)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(2,6)]
* Step 4: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1)
3. evalwcet2bb5in(A,B) -> evalwcet2returnin(A,B) [A >= 5] (?,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (?,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
9. evalwcet2returnin(A,B) -> evalwcet2stop(A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5},3->{9},4->{7},5->{8},6->{8},7->{4,5,6},8->{2,3},9->{}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<3,0,A>, ?) (<3,0,B>, 9 + B)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
(<9,0,A>, ?) (<9,0,B>, 9 + B)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3,9]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (?,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalwcet2bb1in) = 3 + -1*x1
p(evalwcet2bb2in) = 3 + -1*x1
p(evalwcet2bb4in) = 2 + -1*x1
p(evalwcet2bb5in) = 3 + -1*x1
p(evalwcet2entryin) = 3 + -1*x1
p(evalwcet2start) = 3 + -1*x1
The following rules are strictly oriented:
[2 >= A] ==>
evalwcet2bb2in(A,B) = 3 + -1*A
> 2 + -1*A
= evalwcet2bb4in(A,B)
The following rules are weakly oriented:
True ==>
evalwcet2start(A,B) = 3 + -1*A
>= 3 + -1*A
= evalwcet2entryin(A,B)
True ==>
evalwcet2entryin(A,B) = 3 + -1*A
>= 3 + -1*A
= evalwcet2bb5in(A,B)
[4 >= A] ==>
evalwcet2bb5in(A,B) = 3 + -1*A
>= 3 + -1*A
= evalwcet2bb2in(A,0)
[A >= 3 && 9 >= B] ==>
evalwcet2bb2in(A,B) = 3 + -1*A
>= 3 + -1*A
= evalwcet2bb1in(A,B)
[B >= 10] ==>
evalwcet2bb2in(A,B) = 3 + -1*A
>= 2 + -1*A
= evalwcet2bb4in(A,B)
True ==>
evalwcet2bb1in(A,B) = 3 + -1*A
>= 3 + -1*A
= evalwcet2bb2in(A,1 + B)
True ==>
evalwcet2bb4in(A,B) = 2 + -1*A
>= 2 + -1*A
= evalwcet2bb5in(1 + A,B)
* Step 6: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (3 + A,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 7: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (1,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (3 + A,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalwcet2bb1in) = 4 + -1*x1
p(evalwcet2bb2in) = 4 + -1*x1
p(evalwcet2bb4in) = 4 + -1*x1
p(evalwcet2bb5in) = 5 + -1*x1
p(evalwcet2entryin) = 5 + -1*x1
p(evalwcet2start) = 5 + -1*x1
The following rules are strictly oriented:
[4 >= A] ==>
evalwcet2bb5in(A,B) = 5 + -1*A
> 4 + -1*A
= evalwcet2bb2in(A,0)
The following rules are weakly oriented:
True ==>
evalwcet2start(A,B) = 5 + -1*A
>= 5 + -1*A
= evalwcet2entryin(A,B)
True ==>
evalwcet2entryin(A,B) = 5 + -1*A
>= 5 + -1*A
= evalwcet2bb5in(A,B)
[A >= 3 && 9 >= B] ==>
evalwcet2bb2in(A,B) = 4 + -1*A
>= 4 + -1*A
= evalwcet2bb1in(A,B)
[2 >= A] ==>
evalwcet2bb2in(A,B) = 4 + -1*A
>= 4 + -1*A
= evalwcet2bb4in(A,B)
[B >= 10] ==>
evalwcet2bb2in(A,B) = 4 + -1*A
>= 4 + -1*A
= evalwcet2bb4in(A,B)
True ==>
evalwcet2bb1in(A,B) = 4 + -1*A
>= 4 + -1*A
= evalwcet2bb2in(A,1 + B)
True ==>
evalwcet2bb4in(A,B) = 4 + -1*A
>= 4 + -1*A
= evalwcet2bb5in(1 + A,B)
* Step 8: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (1,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (5 + A,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (3 + A,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [5,7,4,6], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalwcet2bb1in) = 1
p(evalwcet2bb2in) = 1
p(evalwcet2bb4in) = 0
The following rules are strictly oriented:
[2 >= A] ==>
evalwcet2bb2in(A,B) = 1
> 0
= evalwcet2bb4in(A,B)
[B >= 10] ==>
evalwcet2bb2in(A,B) = 1
> 0
= evalwcet2bb4in(A,B)
The following rules are weakly oriented:
[A >= 3 && 9 >= B] ==>
evalwcet2bb2in(A,B) = 1
>= 1
= evalwcet2bb1in(A,B)
True ==>
evalwcet2bb1in(A,B) = 1
>= 1
= evalwcet2bb2in(A,1 + B)
We use the following global sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
* Step 9: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (1,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (5 + A,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (3 + A,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (5 + A,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 10: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (1,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (5 + A,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (3 + A,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (5 + A,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (8 + 2*A,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [8,5,7,4,6], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalwcet2bb1in) = 9 + -1*x2
p(evalwcet2bb2in) = 10 + -1*x2
p(evalwcet2bb4in) = 10 + -1*x2
p(evalwcet2bb5in) = 10 + -1*x2
The following rules are strictly oriented:
[A >= 3 && 9 >= B] ==>
evalwcet2bb2in(A,B) = 10 + -1*B
> 9 + -1*B
= evalwcet2bb1in(A,B)
The following rules are weakly oriented:
[2 >= A] ==>
evalwcet2bb2in(A,B) = 10 + -1*B
>= 10 + -1*B
= evalwcet2bb4in(A,B)
[B >= 10] ==>
evalwcet2bb2in(A,B) = 10 + -1*B
>= 10 + -1*B
= evalwcet2bb4in(A,B)
True ==>
evalwcet2bb1in(A,B) = 9 + -1*B
>= 9 + -1*B
= evalwcet2bb2in(A,1 + B)
True ==>
evalwcet2bb4in(A,B) = 10 + -1*B
>= 10 + -1*B
= evalwcet2bb5in(1 + A,B)
We use the following global sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
* Step 11: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (1,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (5 + A,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (50 + 10*A,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (3 + A,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (5 + A,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (8 + 2*A,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 12: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1)
1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (1,1)
2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (5 + A,1)
4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (50 + 10*A,1)
5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (3 + A,1)
6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (5 + A,1)
7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (50 + 10*A,1)
8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (8 + 2*A,1)
Signature:
{(evalwcet2bb1in,2)
;(evalwcet2bb2in,2)
;(evalwcet2bb4in,2)
;(evalwcet2bb5in,2)
;(evalwcet2entryin,2)
;(evalwcet2returnin,2)
;(evalwcet2start,2)
;(evalwcet2stop,2)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{7},5->{8},6->{8},7->{4,5,6},8->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, B)
(<2,0,A>, 4) (<2,0,B>, 0)
(<4,0,A>, ?) (<4,0,B>, 9)
(<5,0,A>, 2) (<5,0,B>, 9)
(<6,0,A>, ?) (<6,0,B>, 9)
(<7,0,A>, ?) (<7,0,B>, 9)
(<8,0,A>, ?) (<8,0,B>, 9)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))