February 2007 - PPL-devel - BUGSENG Mailman

ppl ppl.spec.in
by Roberto Bagnara 22 Feb '07

22 Feb '07

CVSROOT: /cvs/ppl Module name: ppl Branch: ppl-0_9-branch Changes by: bagnara(a)cs.unipr.it 2007-02-22 11:50:16 Modified files: . : ppl.spec.in Log message: Dependencies for YAP fixed. Make sure the header files of GNU Prolog and YAP are found. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/ppl.spec.in.diff?cvsroot=ppl&…

1 0

ppl ppl.spec.in
by Roberto Bagnara 22 Feb '07

22 Feb '07

CVSROOT: /cvs/ppl Module name: ppl Branch: ppl-0_9-branch Changes by: bagnara(a)cs.unipr.it 2007-02-22 08:05:56 Modified files: . : ppl.spec.in Log message: Added missing dependencies. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/ppl.spec.in.diff?cvsroot=ppl&…

1 0

Re: [PPL-devel] PPL: Problem with Checked-Ints
by Roberto Bagnara 21 Feb '07

21 Feb '07

Didier Lime wrote: > I guess I should be using arbitrary length integers anyway! But for now, > I will take my chance with 64 bit checked integers (they should still be > more efficient even on 32 bit computers). They should be. > If I remember well, in the real application, I had this overflow in > remove_space_dimensions (in the conversion routine called by some > minimize function, if I remember my stack frames correctly). Maybe due > to the same emptiness test. Both the emptiness test and remove_space_dimensions() (may) call the conversion routine; so, yes, it is the same phenomenon. >> 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. > > Good idea but, in Romeo, I actually need those non-strict inequalities > so this is not an option. Do you mean that you need those _strict_ inequalities? If so, this may be one application of strict inequalities we do not know. Can you give us some intuition or point us to a paper that explains the role played by strict inequalities in the verification of Time Petri Nets? > Thanks again for your answer and more generally, I must say I do > appreciate programming with this library. From my point of view, you > have really done a great piece of work! Glad to be useful. Thanks! Roberto (on behalf of the entire development team) -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 2

[Fwd: Re: PPL: Problem with Checked-Ints]
by Roberto Bagnara 20 Feb '07

20 Feb '07

-------- Original Message -------- Subject: Re: [PPL-devel] PPL: Problem with Checked-Ints Date: Tue, 20 Feb 2007 11:00:41 +0100 From: Didier Lime <Didier.Lime(a)irccyn.ec-nantes.fr> To: Roberto Bagnara <bagnara(a)cs.unipr.it> References: <9F1730A5-0443-4D9A-B958-C33EC329191C(a)irccyn.ec-nantes.fr> <45DA0CEF.8040107(a)cs.unipr.it> Dear Roberto, First, thanks your for quick and thorough answer! > 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). OK. I had not anticipated this kind of operations, especially since in my particular application, coefficients are supposed to always decrease. I guess I should be using arbitrary length integers anyway! But for now, I will take my chance with 64 bit checked integers (they should still be more efficient even on 32 bit computers). >> 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. Indeed! 46342 does not sound like big when dealing with 32 bit integers (though I now understand it actually is!) > 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; OK. I actually got lazy when typing my sample code (and PPL seemed OK when browsing the source code of the library). > 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. If I remember well, in the real application, I had this overflow in remove_space_dimensions (in the conversion routine called by some minimize function, if I remember my stack frames correctly). Maybe due to the same emptiness test. > 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. Good idea but, in Romeo, I actually need those non-strict inequalities so this is not an option. > Finally, the new paper > BagnaraHZ06TR (BibTeX enty below the signature) can give you > other indications about how to best use the PPL. Thanks again for your answer and more generally, I must say I do appreciate programming with this library. From my point of view, you have really done a great piece of work! Best wishes, Didier -- Dr. Didier Lime Maître de Conférences IRCCyN / École Centrale de Nantes Nantes, France http://www.irccyn.ec-nantes.fr/~lime -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

PPL: Problem with Checked-Ints
by Didier Lime 19 Feb '07

19 Feb '07

Dear PPL developer, 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. 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. 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 Also it runs fine with checked ints and B being below or equal to 46341. I hope it is not just a misuse from me... Please ask if you need some more information. Best wishes, Didier -- Dr. Didier Lime Maître de Conférences IRCCyN / École Centrale de Nantes Nantes, France http://www.irccyn.ec-nantes.fr/~lime

2 1

ppl/src fpu-c99.inlines.hh fpu-ia32.inlines.hh ...
by Abramo Bagnara 19 Feb '07

19 Feb '07

CVSROOT: /cvs/ppl Module name: ppl Branch: altnum Changes by: abagnara(a)cs.unipr.it 2007-02-19 17:23:46 Modified files: src : fpu-c99.inlines.hh fpu-ia32.inlines.hh fpu-none.inlines.hh fpu-sparc.inlines.hh Log message: Add support for SSE. Removed unused function. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/fpu-c99.inlines.hh.diff?c… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/fpu-ia32.inlines.hh.diff?… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/fpu-none.inlines.hh.diff?… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/fpu-sparc.inlines.hh.diff…

1 0

ppl/Watchdog Makefile.am configure.ac doc/.cvs ...
by Roberto Bagnara 18 Feb '07

18 Feb '07

1 0

ppl/Watchdog/doc
by Roberto Bagnara 18 Feb '07

18 Feb '07

CVSROOT: /cvs/ppl Module name: ppl Changes by: bagnara(a)cs.unipr.it 2007-02-18 18:44:00 ppl/Watchdog/doc Update of /cvs/ppl/ppl/Watchdog/doc In directory spartacus.cs.unipr.it:/tmp/cvs-serv30611/doc Log Message: Directory /cvs/ppl/ppl/Watchdog/doc added to the repository

1 0

ppl ppl.spec.in
by Roberto Bagnara 18 Feb '07

18 Feb '07

CVSROOT: /cvs/ppl Module name: ppl Branch: ppl-0_9-branch Changes by: bagnara(a)cs.unipr.it 2007-02-18 13:16:22 Modified files: . : ppl.spec.in Log message: %doc tags corrected for the Prolog interfaces. Tabs used consistently instead of spaces. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/ppl.spec.in.diff?cvsroot=ppl&…

1 0

ppl ppl-0.9-docfiles.patch
by Roberto Bagnara 18 Feb '07

18 Feb '07

CVSROOT: /cvs/ppl Module name: ppl Branch: ppl-0_9-branch Changes by: bagnara(a)cs.unipr.it 2007-02-18 12:07:17 Modified files: . : ppl-0.9-docfiles.patch Log message: Revised. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/ppl-0.9-docfiles.patch.diff?c…

1 0