
Hi,
I'm doing a first pass at integrating PPL with the Action Language Verifier under Dr. Tevfik Bultan at UC Santa Barbara. I've run into what appears to be a problem in the most recent 0.4.2 release. Please let me know as soon as possible if I'm doing something wrong or if it's a genuine problem. I'd like to have an integration I can show next week.
The problem is that minimized_constraints is crashing when it gets down into strongly_minimize_constraints:
if (topologically_closed || !strict_inequals_saturate_all_rays) { assert(cs_rows < cs.num_rows()); ...
The condition topologically_closed is true, but cs_rows == cs.num_rows().
Here is the testcase which reproduces the condition: ----------------------------------------- #include "ppl.hh" using namespace Parma_Polyhedra_Library;
int main() { Variable x2(0), x3(1), x5(2); NNC_Polyhedron poly(3, Polyhedron::UNIVERSE);
poly.add_constraint(x5 > x2); poly.add_constraint(x3 >= x2); poly.add_constraint(x2 + 1 > x3);
poly.minimized_constraints(); return 0; } ------------------------------------------
Thanks, Ken Mixter

Dear Ken,
it seems you have found a genuine bug in the PPL. We are investigating and we hope to be back to you with a workaround soon. All the best
Roberto
kmixter@longshot.com wrote:
Hi,
I'm doing a first pass at integrating PPL with the Action Language Verifier under Dr. Tevfik Bultan at UC Santa Barbara. I've run into what appears to be a problem in the most recent 0.4.2 release. Please let me know as soon as possible if I'm doing something wrong or if it's a genuine problem. I'd like to have an integration I can show next week.
The problem is that minimized_constraints is crashing when it gets down into strongly_minimize_constraints:
if (topologically_closed || !strict_inequals_saturate_all_rays) { assert(cs_rows < cs.num_rows()); ...
The condition topologically_closed is true, but cs_rows == cs.num_rows().
Here is the testcase which reproduces the condition:
#include "ppl.hh" using namespace Parma_Polyhedra_Library;
int main() { Variable x2(0), x3(1), x5(2); NNC_Polyhedron poly(3, Polyhedron::UNIVERSE);
poly.add_constraint(x5 > x2); poly.add_constraint(x3 >= x2); poly.add_constraint(x2 + 1 > x3);
poly.minimized_constraints(); return 0; }
Thanks, Ken Mixter

kmixter@longshot.com wrote:
I'm doing a first pass at integrating PPL with the Action Language Verifier under Dr. Tevfik Bultan at UC Santa Barbara. I've run into what appears to be a problem in the most recent 0.4.2 release. Please let me know as soon as possible if I'm doing something wrong or if it's a genuine problem. I'd like to have an integration I can show next week.
The problem is that minimized_constraints is crashing when it gets down into strongly_minimize_constraints:
if (topologically_closed || !strict_inequals_saturate_all_rays) { assert(cs_rows < cs.num_rows()); ...
The condition topologically_closed is true, but cs_rows == cs.num_rows().
Here is the testcase which reproduces the condition:
Dear Ken,
we have solved the bug you have reported. The quickest way to let you have a workaround is, we believe, providing you with a snapshot of what will become PPL version 0.5. You can find it in our snapshots' area, accessible by FTP at
ftp://ftp.cs.unipr.it/pub/ppl/snapshots/
and by HTTP at
http://www.cs.unipr.it/ppl/Download/ftp/snapshots/
Of course, this operation is a bit rushed and not without risks since the snapshot did not undergo thorough testing and because version 0.5 brings some changes that are not backward compatible (_most_ of which are listed in the NEWS file). However, we will give you the maximum of assistance we can. Please do not hesitate to post the questions you may have to ppl-devel@cs.unipr.it (you have just been given full write permission to that mailing list) for the quickest response time. Thanks a lot for helping us improve PPL. Cheers
Roberto

Hello Roberto,
we have solved the bug you have reported. The quickest way to let you have a workaround is, we believe, providing you with a snapshot of what will become PPL version 0.5. You can find it in our snapshots' area, accessible by FTP at
ftp://ftp.cs.unipr.it/pub/ppl/snapshots/
and by HTTP at
http://www.cs.unipr.it/ppl/Download/ftp/snapshots/
Of course, this operation is a bit rushed and not without risks since the snapshot did not undergo thorough testing and because version 0.5 brings some changes that are not backward compatible (_most_ of which are listed in the NEWS file). However, we will give you the maximum of assistance we can. Please do not hesitate to post the questions you may have to ppl-devel@cs.unipr.it (you have just been given full write permission to that mailing list) for the quickest response time. Thanks a lot for helping us improve PPL.
Thank you for the quick response! I integrated the new version 0.5pre8 which drastically improves what I can demo.
-Ken

kmixter@longshot.com wrote:
Thank you for the quick response! I integrated the new version 0.5pre8 which drastically improves what I can demo.
Hi Ken,
that is great news! When will we be able to play with your system? We have some ongoing work that could greatly benefit from experimentation with another application, and the Action Language Verifier is a very promising candidate for that purpose. Cheers
Roberto

Dear Ken,
the PPL snapshot we gave you some time ago contained a couple of bugs that have now been fixed. Up-to-date snapshots are now online at the usual place, that is
ftp://ftp.cs.unipr.it/pub/ppl/snapshots/
and, if you prefer HTTP,
http://www.cs.unipr.it/ppl/Download/ftp/snapshots/
Merry Christmas and Happy New Year to you and to all the people on ppl-devel@cs.unipr.it. Ciao
Roberto
participants (2)
-
kmixter@longshot.com
-
Roberto Bagnara