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