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
-- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
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 -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
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 -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
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 -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it
participants (2)
-
kmixter@longshot.com -
Roberto Bagnara