WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1)
1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1)
2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1)
3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1)
4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1)
5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1)
6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1)
7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1)
8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1)
Signature:
{(evalrandom1dbb1in,2)
;(evalrandom1dbb5in,2)
;(evalrandom1dentryin,2)
;(evalrandom1dreturnin,2)
;(evalrandom1dstart,2)
;(evalrandom1dstop,2)}
Flow Graph:
[0->{1,2},1->{3,4},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}]
+ 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>, 1, .= 1)
(<2,0,A>, A, .= 0) (<2,0,B>, B, .= 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>, 1 + B, .+ 1)
(<6,0,A>, A, .= 0) (<6,0,B>, 1 + B, .+ 1)
(<7,0,A>, A, .= 0) (<7,0,B>, 1 + B, .+ 1)
(<8,0,A>, A, .= 0) (<8,0,B>, B, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1)
1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1)
2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1)
3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1)
4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1)
5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1)
6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1)
7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1)
8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1)
Signature:
{(evalrandom1dbb1in,2)
;(evalrandom1dbb5in,2)
;(evalrandom1dentryin,2)
;(evalrandom1dreturnin,2)
;(evalrandom1dstart,2)
;(evalrandom1dstop,2)}
Flow Graph:
[0->{1,2},1->{3,4},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}]
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>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, 1)
(<2,0,A>, A) (<2,0,B>, B)
(<3,0,A>, A) (<3,0,B>, A)
(<4,0,A>, A) (<4,0,B>, 1 + A)
(<5,0,A>, A) (<5,0,B>, A)
(<6,0,A>, A) (<6,0,B>, A)
(<7,0,A>, A) (<7,0,B>, A)
(<8,0,A>, A) (<8,0,B>, 1 + A + B)
* Step 3: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1)
1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1)
2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1)
3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1)
4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1)
5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1)
6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1)
7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1)
8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1)
Signature:
{(evalrandom1dbb1in,2)
;(evalrandom1dbb5in,2)
;(evalrandom1dentryin,2)
;(evalrandom1dreturnin,2)
;(evalrandom1dstart,2)
;(evalrandom1dstop,2)}
Flow Graph:
[0->{1,2},1->{3,4},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, 1)
(<2,0,A>, A) (<2,0,B>, B)
(<3,0,A>, A) (<3,0,B>, A)
(<4,0,A>, A) (<4,0,B>, 1 + A)
(<5,0,A>, A) (<5,0,B>, A)
(<6,0,A>, A) (<6,0,B>, A)
(<7,0,A>, A) (<7,0,B>, A)
(<8,0,A>, A) (<8,0,B>, 1 + A + B)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(1,4)]
* Step 4: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1)
1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1)
2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1)
3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1)
4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1)
5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1)
6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1)
7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1)
8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1)
Signature:
{(evalrandom1dbb1in,2)
;(evalrandom1dbb5in,2)
;(evalrandom1dentryin,2)
;(evalrandom1dreturnin,2)
;(evalrandom1dstart,2)
;(evalrandom1dstop,2)}
Flow Graph:
[0->{1,2},1->{3},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, 1)
(<2,0,A>, A) (<2,0,B>, B)
(<3,0,A>, A) (<3,0,B>, A)
(<4,0,A>, A) (<4,0,B>, 1 + A)
(<5,0,A>, A) (<5,0,B>, A)
(<6,0,A>, A) (<6,0,B>, A)
(<7,0,A>, A) (<7,0,B>, A)
(<8,0,A>, A) (<8,0,B>, 1 + A + B)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [2,4,8]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1)
1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1)
3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1)
5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1)
6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1)
7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1)
Signature:
{(evalrandom1dbb1in,2)
;(evalrandom1dbb5in,2)
;(evalrandom1dentryin,2)
;(evalrandom1dreturnin,2)
;(evalrandom1dstart,2)
;(evalrandom1dstop,2)}
Flow Graph:
[0->{1},1->{3},3->{5,6,7},5->{3},6->{3},7->{3}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, 1)
(<3,0,A>, A) (<3,0,B>, A)
(<5,0,A>, A) (<5,0,B>, A)
(<6,0,A>, A) (<6,0,B>, A)
(<7,0,A>, A) (<7,0,B>, A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalrandom1dbb1in) = x1 + -1*x2
p(evalrandom1dbb5in) = 1 + x1 + -1*x2
p(evalrandom1dentryin) = x1
p(evalrandom1dstart) = x1
The following rules are strictly oriented:
[A >= B] ==>
evalrandom1dbb5in(A,B) = 1 + A + -1*B
> A + -1*B
= evalrandom1dbb1in(A,B)
The following rules are weakly oriented:
True ==>
evalrandom1dstart(A,B) = A
>= A
= evalrandom1dentryin(A,B)
[A >= 1] ==>
evalrandom1dentryin(A,B) = A
>= A
= evalrandom1dbb5in(A,1)
[0 >= 1 + C] ==>
evalrandom1dbb1in(A,B) = A + -1*B
>= A + -1*B
= evalrandom1dbb5in(A,1 + B)
[C >= 1] ==>
evalrandom1dbb1in(A,B) = A + -1*B
>= A + -1*B
= evalrandom1dbb5in(A,1 + B)
True ==>
evalrandom1dbb1in(A,B) = A + -1*B
>= A + -1*B
= evalrandom1dbb5in(A,1 + B)
* Step 6: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1)
1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1)
3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (A,1)
5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1)
6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1)
7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1)
Signature:
{(evalrandom1dbb1in,2)
;(evalrandom1dbb5in,2)
;(evalrandom1dentryin,2)
;(evalrandom1dreturnin,2)
;(evalrandom1dstart,2)
;(evalrandom1dstop,2)}
Flow Graph:
[0->{1},1->{3},3->{5,6,7},5->{3},6->{3},7->{3}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, 1)
(<3,0,A>, A) (<3,0,B>, A)
(<5,0,A>, A) (<5,0,B>, A)
(<6,0,A>, A) (<6,0,B>, A)
(<7,0,A>, A) (<7,0,B>, A)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 7: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1)
1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (1,1)
3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (A,1)
5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (A,1)
6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (A,1)
7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (A,1)
Signature:
{(evalrandom1dbb1in,2)
;(evalrandom1dbb5in,2)
;(evalrandom1dentryin,2)
;(evalrandom1dreturnin,2)
;(evalrandom1dstart,2)
;(evalrandom1dstop,2)}
Flow Graph:
[0->{1},1->{3},3->{5,6,7},5->{3},6->{3},7->{3}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B)
(<1,0,A>, A) (<1,0,B>, 1)
(<3,0,A>, A) (<3,0,B>, A)
(<5,0,A>, A) (<5,0,B>, A)
(<6,0,A>, A) (<6,0,B>, A)
(<7,0,A>, A) (<7,0,B>, A)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))