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