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