[PPL-devel] Widening Operator

[Enrico Oliosi]

> Dear Enrico,
>
> I assume you are working with PPL 0.5, and that by "[our] operator"
> you mean the BHRZ03 widening.  If so, notice that the widening proposed
> in the PhD thesis of Nicholas Halbwachs (which is a refinement of the
> one proposed by Patrick Cousot and Halbwachs himself in their POPL'78
> paper) is already present in the version of the library you have,
> where it is called H79.  So implementation of the Cousot & Halbwachs
> widening and extrapolation operators are provided by methods
>
>  void H79_widening_assign(const Polyhedron& y, unsigned* tp = 0);
>  void limited_H79_extrapolation_assign(const Polyhedron& y,
> 					const ConSys& cs,
> 					unsigned* tp = 0);
>  void bounded_H79_extrapolation_assign(const Polyhedron& y,
> 					const ConSys& cs,
> 					unsigned* tp = 0);
>
[...]
> Please, do not hesitate to come back to us if I have misunderstood
> your question.

Dear all,
yes I use PPL 0.5. I used exactly H79 widening operator, I have, i.e., 
two polyhedra:

ph1 :
-A - 2*B >= -6,
B >= 0,
A - 2*B >= 2.

ph2:
-A - 2*B >= -10,
B >= 0,
A - 2*B >= 2.

if I call the function ph1.H79_widening_assign(ph2) the result is
-A - 2*B >= -6,
B >= 0,
A - 2*B >= 2

which is the first one (ph1).
In the Cousot & Halbwachs's article the same example gives a different result:
B >= 0,
A - 2*B >= 2

Maybe I wrong something when I invoke these functions.

All the best,

     Enrico.