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