- PPL-devel - BUGSENG Mailman

ppl/src Row.defs.hh Row.cc Matrix.cc minimize. ...
by Enea Zaffanella 20 Jan '03

20 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-20 09:22:50 Modified files: src : Row.defs.hh Row.cc Matrix.cc minimize.cc simplify.cc Log message: Strong normalization of Row objects now enforce the first non-zero coefficient to be positive. When creating a matrix having n copies of the same row, the matrix is now declared to be sorted (since sortedness by itself does not implies that it has no duplicates); this also includes the case of empty matrices. Some improvements in methods Matrix::gauss() and Matrix::back_substitute(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Row.defs.hh.diff?cvsroot=… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Row.cc.diff?cvsroot=ppl&r… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Matrix.cc.diff?cvsroot=pp… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/minimize.cc.diff?cvsroot=… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/simplify.cc.diff?cvsroot=…

1 0

ppl/src Constraint.cc Constraint.inlines.hh Ge ...
by Enea Zaffanella 18 Jan '03

18 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-18 16:59:09 Modified files: src : Constraint.cc Constraint.inlines.hh Generator.cc Matrix.cc minimize.cc simplify.cc Polyhedron.cc Log message: Implemented changes required to make the library compile cleanly and pass `make check' when the flag EXTRA_NORMALIZATION is set to 1 (the default being still 0). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Constraint.cc.diff?cvsroo… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Constraint.inlines.hh.dif… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Generator.cc.diff?cvsroot… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Matrix.cc.diff?cvsroot=pp… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/minimize.cc.diff?cvsroot=… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/simplify.cc.diff?cvsroot=… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron.cc.diff?cvsroo…

1 0

ppl/tests Makefile.am
by Roberto Bagnara 18 Jan '03

18 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2003-01-18 12:53:16 Modified files: tests : Makefile.am Log message: The `libppl_tests.a' library should not be built until the `make check' command is run. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Makefile.am.diff?cvsroo…

1 0

ppl/src Polyhedron.cc
by Enea Zaffanella 18 Jan '03

18 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-18 11:58:12 Modified files: src : Polyhedron.cc Log message: Corrected a bug in poly_hull_assign_and_minimize(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron.cc.diff?cvsroo…

1 0

The Action Language Verifier and the Parma Polyhedra Library
by Roberto Bagnara 15 Jan '03

15 Jan '03

Dear Ken, we have started studying your code in order to understand your needs and to improve the PPL. To start with, we have modified parmiface.c so as to use the `Polyhedron::check_universe()' method (this results in cleaner code that is also more efficient). kmixter(a)longshot.com wrote: > You may also want to download the latest version 0.2 for full > documentation and examples. We did that, in order to have more examples to test with and we ran across a bug. We have modifies ALV's main program so as to catch standard exceptions and print them. With this modification, here is what happens: $ ~/composite/composite/obj-linux/action -r statechart.al Module main Local variables main.Office.0 of type 1 main.Occupants.0 of type 1 main.Light.0 of type 1 main.turn_off of type 1 main.turn_on of type 1 main.exit of type 1 main.enter of type 1 main.count of type 4 Formal variables items size 4 items size 4 **************** domain variables type 0 main.0.Office.0 main.0.Occupants.0 main.0.Light.0 main.0.turn_off main.0.turn_on main.0.exit main.0.enter type 1 main.0.count Exception caught: PPL::NNC_Polyhedron::inters_assign_and_min(y): this->space_dimension() == 2, y->space_dimension() == 1. Capacity : 10003 Total references : 0 Hits : 0 ( nan %) Misses : 0 ( nan %) Collisions : 0 ( nan %) Stats The important bit is Exception caught: PPL::NNC_Polyhedron::inters_assign_and_min(y): this->space_dimension() == 2, y->space_dimension() == 1. This says that NNC_Polyhedron::intersection_assign_and_minimize() has been called over two polyhedra of different dimensions. The only call to this method is in parmiface.c in the function Polyhedron *DomainIntersection(Polyhedron *d1, Polyhedron *d2, int). Do you know what might go wrong? Meanwhile, please find attached the patch file for the changes mentioned above (without the change to `main()' you would see an abort instead of the description of the caught exception). Notice that this patch assumes you have already applied the path we sent you a few days ago. 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 diff -rcp2 composite.1/parser/main.c composite/parser/main.c *** composite.1/parser/main.c Tue Jan 7 15:38:48 2003 --- composite/parser/main.c Tue Jan 7 16:39:37 2003 *************** *** 6,9 **** --- 6,10 ---- #include <stdlib.h> #include <iostream.h> + #include <stdexcept> #include <bool.h> *************** temporal operator \n\ *** 99,103 **** char *startHeap; ! int main(int argc,char **argv) { char *fileName; --- 100,104 ---- char *startHeap; ! int main(int argc,char **argv) try { char *fileName; *************** int main(int argc,char **argv) { *** 338,346 **** } ! ! ! ! ! ! ! --- 339,345 ---- } ! catch (const exception& e) { ! cerr << "Exception caught:\n" ! << e.what() ! << endl; ! } diff -rcp2 composite.1/util/parmiface.c composite/util/parmiface.c *** composite.1/util/parmiface.c Tue Jan 7 15:38:48 2003 --- composite/util/parmiface.c Tue Jan 7 15:43:17 2003 *************** int DomainIsEmpty(Polyhedron *p) *** 144,149 **** int PolyhedronIsUniverse(Polyhedron *p) { ! const PPL::ConSys *cs = &p->_data->constraints(); ! return cs->begin() == cs->end(); } --- 144,148 ---- int PolyhedronIsUniverse(Polyhedron *p) { ! return p->_data->check_universe(); } *************** Polyhedron *DomainDifference(Polyhedron *** 307,315 **** for (p2 = d2; p2 != NULL; p2 = p2->next) { - const PPL::ConSys *cs = &p2->_data->constraints(); - PPL::ConSys::const_iterator i = cs->begin(); Polyhedron *result = NULL; ! if (cs->begin() == cs->end()) { /* Universe polyhedrons have no constraints, so they need to be special-cased, meaning this should result in empty polyhedron. */ --- 306,312 ---- for (p2 = d2; p2 != NULL; p2 = p2->next) { Polyhedron *result = NULL; ! if (p2->_data->check_universe()) { /* Universe polyhedrons have no constraints, so they need to be special-cased, meaning this should result in empty polyhedron. */ *************** Polyhedron *DomainDifference(Polyhedron *** 317,320 **** --- 314,320 ---- } + const PPL::ConSys *cs = &p2->_data->constraints(); + PPL::ConSys::const_iterator i; + for (p1 = remainder; p1 != NULL; p1 = p1->next) { for (i = cs->begin(); i != cs->end(); ++i) {

2 1

ppl ./README doc/devref-browse.doxyconf-latex. ...
by Enea Zaffanella 15 Jan '03

15 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-15 14:57:47 Modified files: . : README doc : devref-browse.doxyconf-latex.in devref-print.doxyconf-latex.in devref.doxyconf-html.in Removed files: src : Init.inlines.hh Log message: No longer using file Init.inlines.hh. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/README.diff?cvsroot=ppl&r1=1.… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/doc/devref-browse.doxyconf-la… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/doc/devref-print.doxyconf-lat… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/doc/devref.doxyconf-html.in.d… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Init.inlines.hh.diff?cvsr…

1 0

ppl/src Polyhedron.cc
by Enea Zaffanella 15 Jan '03

15 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-15 14:54:00 Modified files: src : Polyhedron.cc Log message: After applying each of the techniques of the BHRZ03 widening, check whether we have obtained a polyhedron strictly smaller than that one obtainable using the H79 widening. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron.cc.diff?cvsroo…

1 0

ppl/src Init.defs.hh Init.cc Makefile.am
by Enea Zaffanella 15 Jan '03

15 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-15 14:51:08 Modified files: src : Init.defs.hh Init.cc Makefile.am Log message: Initialization and finalization of the library are no longer inlined. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Init.defs.hh.diff?cvsroot… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Init.cc.diff?cvsroot=ppl&… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Makefile.am.diff?cvsroot=…

1 0

ppl/src Polyhedron.cc
by Enea Zaffanella 13 Jan '03

13 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-13 23:22:46 Modified files: src : Polyhedron.cc Log message: Many improvements in the code and comments of method averaging_constraints(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron.cc.diff?cvsroo…

1 0

ppl/src Polyhedron.inlines.hh
by Enea Zaffanella 12 Jan '03

12 Jan '03

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2003-01-12 23:42:40 Modified files: src : Polyhedron.inlines.hh Log message: Try to avoid minimization in method check_empty(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Polyhedron.inlines.hh.dif…

1 0