[PPL-devel] Re: Widening operation in SICStus

[Roberto Bagnara]

V Panumong wrote:
> I've just tried a simple program on SICStus with ppl, but it failed.
> Is it something I've done wrongly?
> 
> The program is:
> test(CS, GS):-I='$VAR'(0), J='$VAR'(1),
>         ppl_new_Polyhedron_from_generators(nnc, [point(2*I+0*J),
>                                                  point(6*I+0*J),
>                                                  point(4*I+1*J)], PL1),
>         ppl_new_Polyhedron_from_generators(nnc, [point(2*I+0*J),
>                                                  point(10*I+0*J),
>                                                  point(6*I+0*J)], PL2),
>         ppl_Polyhedron_BHRZ03_widening_assign(PL1, PL2),
>         ppl_Polyhedron_get_constraints(PL1, CS),
>         ppl_Polyhedron_get_generators(PL1, GS).
> 
> The error returned is:
> ppl_sicstus: Polyhedron_widenings.cc:667: void 
> Parma_Polyhedra_Library::Polyhedron::BHRZ03_widening_assign(const 
> Parma_Polyhedra_Library::Polyhedron&, unsigned int*): Assertion 
> `x_copy.contains(y_copy)' failed.
> ./ps: line 1: 29556 Aborted
> 
> The program also fails if I change the predicate to 
> ppl_Polyhedron_H79_widening_assign.
> 
> I took this example program from "Automatic Discovery of Linear 
> Constraints Among Variables of a Program" by Cousot and Halwachs '78
> p.94

Dear Vaji,

an important requirement of widening predicates such as

   ppl_Polyhedron_BHRZ03_widening_assign/2

is that the first polyhedron must contain (or be equal to)
the second polyhedron.  So what you want to do is probably
the following:

test(CS, GS):-I='$VAR'(0), J='$VAR'(1),
         ppl_new_Polyhedron_from_generators(nnc, [point(2*I+0*J),
                                                  point(6*I+0*J),
                                                  point(4*I+1*J)], PL1),
         ppl_new_Polyhedron_from_generators(nnc, [point(2*I+0*J),
                                                  point(10*I+0*J),
                                                  point(6*I+0*J)], PL2),
         ppl_Polyhedron_poly_hull_assign(PL1, PL2),
         ppl_Polyhedron_BHRZ03_widening_assign(PL1, PL2),
         ppl_Polyhedron_get_constraints(PL1, CS),
         ppl_Polyhedron_get_generators(PL1, GS).

Notice that this is actually the _only_ interface invariant that
is only checked in versions of the library compiled with assertions
enabled.  Admittedly, this is a limitation and we would love to
find a cheap way to always do this test.

As things stand now, I think we should mitigate this problem as
much as possible by means of documentation.  The general library
documentation explains the containment prerequisite of extrapolation
and widening methods; the documentation of the C++ and of the C
interfaces do recall it;  the Prolog interface seems to say nothing
on the subject.

Pat, can you please update the Prolog interface documentation so
as to make it less likely that users stumble on this kind of problem?

Thank you Vaji: as you can see this kind of user feedback
is crucial for improving the library.
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