[PPL-devel] Widening Operator

[Roberto Bagnara]

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

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it