[PPL-devel] PPL's Int64_Box's CC76_widening

[Enea Zaffanella]

On 09/02/2012 07:05 PM, Zhoulai wrote:
> Hello,
>
> By PPL's Int64_Box.CC76_widening_assign , I get [1,1] \widen [1,2] =
> [1,2] whereas [1,+inf] is expected in this case.
>
> Here is my Java test code (below createIntBox (a,b) is a help function
> that creates an interval of dimension 1 between integers 'a' and 'b')
>
>      Int64_Box b=createIntBox(1, 1);
>      Int64_Box b2=createIntBox(1, 2);
>      out.println(b+",      " + b2);
>
>      b2.CC76_widening_assign(b, new By_Reference<Integer>(0));
>      out.println(b+",      " + b2);
>
> I get:
>
> A in 1,      A in [1, 2]
> A in 1,      A in [1, 2]
>
> I probably misunderstand something, but applying the original definition
> of widening as defined in CC76, we have the following:
>
> [1,1] \widening [1,2] = [1, +inf]
>
> which is different from PPL's result above.
>
>
> Strangely, if I change 'b2' to [1,3] ,i.e.
>     Int64_Box b2=createIntBox(1, 3),
>
> I will get the expected results, i.e
> [1,1] \widening [1,3] = [1, +inf]
>
>
> So It becomes a bit confusing. Maybe PPL has another implementation of
> CC76's widening?  Can you clarify a bit?
>
> Thanks.
>
> Zell.


 From the users' manual:
=============================================
Widening and Extrapolation Operators on Boxes

The library provides a widening operator for boxes. Given two sequences 
of intervals defining two $n$-dimensional boxes, the CC76-widening 
applies, for each corresponding interval and bound, the interval 
constraint widening defined in [CC76]. For extra precision, this 
incorporates the widening with thresholds as defined in [BCCetal02] with 
$\{-2, -1, 0, 1, 2\}$ as the set of default threshold values.
=============================================

The behavior you observe is due to the fact that the upper bound 2 is 
below one of the default threshold values, while 3 is not.

Enea.