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.