Didier Lime wrote:

I am currently using the PPL to do some formal verification on Time Petri Nets. You might be interested in knowing that the next release of Romeo (http://romeo.rts-software.org/) should rely on it for all its "hybrid" computations.

Dear Didier, this is good news! Please let us know when the release is out.

Anyway, I have a strange "positive overflow" with the code below. The complete error message reads: $ ./test_ppl terminate called after throwing an instance of 'std::overflow_error' what(): Positive overflow. Abort trap

Info that should be useful: - I run this code on an Apple MacBook Pro with an Intel Core 2 Duo processor - I compiled the PPL seamlessly with options --enabled- optimization=speed and --enable-coefficients=checked-int32 - g++ --version reads: i686-apple-darwin8-g++-4.0.1 (GCC) 4.0.1 (Apple Computer, Inc. build 5367)

My sample code : #include <iostream> using namespace std;

#include <ppl.hh> using namespace PPL; using namespace PPL::IO_Operators;

int main() { NNC_Polyhedron P(2); Variable A(0); Variable B(1);

P.add_constraint(B == 46342); P.add_constraint(A >= 0); P.add_constraint(A <= 1);

Linear_Expression expr = B - A; P.affine_image(B, expr);

cout << P << endl;

return 0; }

I compile it with g++ -o test_ppl test_ppl.cc -lppl -lgmp and get the above exception when executing it.

I have checked. The overflow is genuine: the statement `cout << P << endl;' checks whether `P' is empty in order to print `false' in case it is. To do so, it calls a conversion routine that, at some stage, multiplies 46342 by 46341, and this gives an overflow on 32-bit integers (46342*46341 = 2147534622 > 2147483647).

Now, if I compile the PPL with --enable-coefficients=native-int32, it just runs fine and gives the intended result: A + B = 46342, -A >= -1

With native integers the PPL is, in practice, just a generator of random behavior. In this particular case, perhaps the right thing happens by chance. Notice though that the right result is A + B = 46342, A >= 0, -A >= -1

Also it runs fine with checked ints and B being below or equal to 46341.

No wonder (46341*46340 = 2147441940 < 2147483647).

I hope it is not just a misuse from me... Please ask if you need some more information.

I think your surprise is due to the PPL internal computations: your problem does no seem to have big enough coefficients to justify an overflow with 32-bit integers, but in fact it has. A few further annotations: I had to change two `using' directives in your program so as to read using namespace Parma_Polyhedra_Library; using namespace Parma_Polyhedra_Library::IO_Operators; If you change the output statement to cout << P.constraints() << endl; the conversion routine is not called and you will see the right result being printed. Note also that C_Polyhedron objects are significantly more efficient than NNC_Polyhedron objects: so, if you don't need to work with non-closed polyhedra (i.e., don't need strict inequalities) you may consider to use the former for efficiency. Finally, the new paper BagnaraHZ06TR (BibTeX enty below the signature) can give you other indications about how to best use the PPL. Please do not hesitate to come back to us: your feedback is highly appreciated. All the best, 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 @TechReport{BagnaraHZ06TR, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems", Number = 457, Type = "Quaderno", Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy", Year = 2006, Note = "Available at \url{http://www.cs.unipr.it/Publications/}. Also published as {\tt arXiv:cs.MS/0612085}, available from \url{http://arxiv.org/}.", Abstract = "Since its inception as a student project in 2001, initially just for the handling (as the name implies) of convex polyhedra, the \emph{Parma Polyhedra Library} has been continuously improved and extended by joining scrupulous research on the theoretical foundations of (possibly non-convex) numerical abstractions to a total adherence to the best available practices in software development. Even though it is still not fully mature and functionally complete, the Parma Polyhedra Library already offers a combination of functionality, reliability, usability and performance that is not matched by similar, freely available libraries. In this paper, we present the main features of the current version of the library, emphasizing those that distinguish it from other similar libraries and those that are important for applications in the field of analysis and verification of hardware and software systems.", URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06TR.pdf" }