[PPL-devel] Widening when CP0 is not included in CP1

25 Sep 2005


      Hi,
In the documentation you always remark the precondition CP0<=CP1 
required by widening(CP1,CP0). What is the usual strategy when the 
condition is not met? I mean, imagine a list of consecutive abstract 
values (1D polyhedrons) like
    {1<x<2}, {2<x<3},{3<x<4}, ....,{n<x<n+1}
How can we ensure converge in these cases?
Thanks!
Mario Mendez