Enrico Oliosi wrote:
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.
Dear Enrico,
you are calling H79_widening_assign() with the arguments reversed. If you look at the documentation, in fact, you will see that an invocation of the form
x.H79_widening_assign(y)
is valid only if y is contained in x. In your example, you have that ph2 is not contained in ph1, but the other way around. So what you want is
ph2.H79_widening_assign(ph1)
and the result, in ph2, will be what you expect. Actually, applying the widening by Cousot and Halbwachs to polyhedra that do not satisfy the required inclusion property is a very common mistake (but don't tell this anyone!).
In order to detect this kind of mistakes, let me suggest you to configure the PPL with the `--enable-assertions' while you are still debugging your application. Your program will be (much) slower, but you will detect bugs in your code (or perhaps in the PPL itself) more quickly. Later, when you will require more speed you can reconfigure the library without the `--enable-assertions' option and recompile. I hope this helps: let us know how it goes. Cheers,
Roberto