January 2013 - PPL-devel - BUGSENG Mailman

Re: [PPL-devel] ppl-1.0 tests fail to build on s390/s390x
by Roberto Bagnara 06 Feb '13

06 Feb '13

Hi Matthias. I just hit the wrong button on the administrative interface of the ppl-devel mailing list. So the message has gone forever before I could read it. Please resend it to the list and accept my apologies. Kind regards, Roberto P.S. This is the failure, right? https://buildd.debian.org/fetch.cgi?pkg=ppl&arch=s390x&ver=1.0-1&stamp=1359… -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com

2 5

Technical questions on how to extend a polyhedron
by giuseppe lipari 31 Jan '13

31 Jan '13

Dear all, we are using the PPL (C++ version) to model a parametric real-time scheduling problem. At some point in our methodology, we obtain a region of space constrained by a C_Polyhedron that describes a subset of valid solutions for our problem. Our problem has also this nice property: if X=(x_1, ..., x_n) is a vector contained in the C_Polyhedron, then any Y = (y_1, ...., y_n) with forall i 0<= y_i <= x_i, is also a valid solution. Therefore we would like to extend the C_Polyhedron to include all vectors 0<= Y <= X. So, our questions are: 1) Is there any simple way of doing it in PPL? In 2D we thought of the following simple strategy: add points (0,0) (x1,0) (0, x2) to the set of generators of the polyhedron, then minimize it. 2) Is this strategy correct? 3) How can we extend it to N dimension? Thanks in advance for your kind response Giuseppe Lipari Laboratoire Spécification et Vérification, Ecole Normale Supérieure de Cachan

3 3

[GIT] ppl/ppl(master): Added missing line.
by Abramo Bagnara 30 Jan '13

30 Jan '13

Module: ppl/ppl Branch: master Commit: 3822e9ecd0783a5743dd48cda86ae17ba702c468 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3822e9ecd078… Author: Abramo Bagnara <abramo.bagnara(a)bugseng.com> Date: Wed Jan 30 09:20:06 2013 +0100 Added missing line. --- src/Float_defs.hh | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/src/Float_defs.hh b/src/Float_defs.hh index 3e455d2..090e70e 100644 --- a/src/Float_defs.hh +++ b/src/Float_defs.hh @@ -267,6 +267,7 @@ struct float_ieee754_quad { static const int EXPONENT_MIN = -EXPONENT_MAX + 1; static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); + static const Floating_Point_Format floating_point_format = IEEE754_QUAD; int inf_sign() const; bool is_nan() const; int zero_sign() const;

1 0

Extracting the source files
by Albert Cluster 24 Jan '13

24 Jan '13

Hi PPL Mailing List, I know it's not particularly a development issue, but I'm trying to download ppl sources to compile a cross-compilation tool chain but What ever the source I download from the ftp server, i'm not able to extract the source. It says that the file is corrupted. Do you have any idea on how I could solve that issue ? Have a nice day, and thank you for that software. Best regards, Albert.

2 5

[GIT] ppl/ppl(master): Obsolete link updated.
by Roberto Bagnara 21 Jan '13

21 Jan '13

Module: ppl/ppl Branch: master Commit: 09a5a4484a0361d77a716b579a9411aae5baa432 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=09a5a4484a03… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Jan 21 21:09:16 2013 +0100 Obsolete link updated. --- doc/ppl_citations.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index f9f388f..4c2f23d 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -530,7 +530,7 @@ Summarizing: Institution = "Departament de Llenguatges i Sistemes Inform{\`a}tics, Universitat Polit{\`e}cnica de Catalunya, Barcelona, Spain", Year = 2005, - Note = "Available at \url{http://www.lsi.upc.es/dept/techreps/techreps.html}" + Note = "Available at \url{http://www.lsi.upc.edu/dept/techreps/techreps.html}" } @Incollection{BandaG09,

1 0

[GIT] ppl/ppl(polyops): Merge branch 'master' into polyops
by Roberto Bagnara 17 Jan '13

17 Jan '13

Module: ppl/ppl Branch: polyops Commit: 3e14a54f0b6c8a5b72d00b26919b1a74b9e8e2c8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3e14a54f0b6c… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Thu Jan 17 09:16:09 2013 +0100 Merge branch 'master' into polyops ---

1 0

[GIT] ppl/ppl(polyops): Comments fixed.
by Roberto Bagnara 17 Jan '13

17 Jan '13

Module: ppl/ppl Branch: polyops Commit: fba4b31ebf3179be4fa020f5278d67728b192c8e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fba4b31ebf31… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Thu Jan 17 08:59:34 2013 +0100 Comments fixed. (Thanks to Marco Faella.) --- src/Generator_defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Generator_defs.hh b/src/Generator_defs.hh index 5471ee2..5bb204c 100644 --- a/src/Generator_defs.hh +++ b/src/Generator_defs.hh @@ -625,14 +625,14 @@ private: //! Marks the epsilon dimension as a standard dimension. /*! - The row topology is changed to <CODE>NOT_NECESSARILY_CLOSED</CODE>, and + The row topology is changed to <CODE>NECESSARILY_CLOSED</CODE>, and the number of space dimensions is increased by 1. */ void mark_as_necessarily_closed(); //! Marks the last dimension as the epsilon dimension. /*! - The row topology is changed to <CODE>NECESSARILY_CLOSED</CODE>, and + The row topology is changed to <CODE>NOT_NECESSARILY_CLOSED</CODE>, and the number of space dimensions is decreased by 1. */ void mark_as_not_necessarily_closed();

1 0

[GIT] ppl/ppl(master): Comments fixed.
by Roberto Bagnara 17 Jan '13

17 Jan '13

Module: ppl/ppl Branch: master Commit: fba4b31ebf3179be4fa020f5278d67728b192c8e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fba4b31ebf31… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Thu Jan 17 08:59:34 2013 +0100 Comments fixed. (Thanks to Marco Faella.) --- src/Generator_defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Generator_defs.hh b/src/Generator_defs.hh index 5471ee2..5bb204c 100644 --- a/src/Generator_defs.hh +++ b/src/Generator_defs.hh @@ -625,14 +625,14 @@ private: //! Marks the epsilon dimension as a standard dimension. /*! - The row topology is changed to <CODE>NOT_NECESSARILY_CLOSED</CODE>, and + The row topology is changed to <CODE>NECESSARILY_CLOSED</CODE>, and the number of space dimensions is increased by 1. */ void mark_as_necessarily_closed(); //! Marks the last dimension as the epsilon dimension. /*! - The row topology is changed to <CODE>NECESSARILY_CLOSED</CODE>, and + The row topology is changed to <CODE>NOT_NECESSARILY_CLOSED</CODE>, and the number of space dimensions is decreased by 1. */ void mark_as_not_necessarily_closed();

1 0

[GIT] ppl/ppl(polyops): Merge branch 'polyops' of ssh://git.cs.unipr.it/ppl /ppl into polyops
by Marco Faella 15 Jan '13

15 Jan '13

Module: ppl/ppl Branch: polyops Commit: 6790e3270667e4d85821bad8b879ead72498cabf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6790e3270667… Author: Marco Faella <marfaella(a)gmail.com> Date: Tue Jan 15 14:35:01 2013 +0100 Merge branch 'polyops' of ssh://git.cs.unipr.it/ppl/ppl into polyops ---

1 0

[GIT] ppl/ppl(polyops): first draft of positive_time_elapse added
by Marco Faella 15 Jan '13

15 Jan '13

Module: ppl/ppl Branch: polyops Commit: a357bc4aefebd03e72ed131a086f966cf7cb65f5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a357bc4aefeb… Author: Marco Faella <marfaella(a)gmail.com> Date: Tue Jan 15 14:34:06 2013 +0100 first draft of positive_time_elapse added --- src/NNC_Polyhedron.cc | 5 ++ src/NNC_Polyhedron_defs.hh | 9 +++ src/Polyhedron_defs.hh | 2 + src/Polyhedron_nonpublic.cc | 166 ++++++++++++++++++++++++++++++++++++++++++- 4 files changed, 181 insertions(+), 1 deletions(-) diff --git a/src/NNC_Polyhedron.cc b/src/NNC_Polyhedron.cc index 65fb421..7db5270 100644 --- a/src/NNC_Polyhedron.cc +++ b/src/NNC_Polyhedron.cc @@ -86,3 +86,8 @@ PPL::NNC_Polyhedron::poly_hull_assign_if_exact(const NNC_Polyhedron& y) { #endif #undef USE_BHZ09 } + +void +PPL::NNC_Polyhedron::positive_time_elapse_assign(const Polyhedron& y) { + Polyhedron::positive_time_elapse_assign(y); +} diff --git a/src/NNC_Polyhedron_defs.hh b/src/NNC_Polyhedron_defs.hh index 67c7850..3eefffd 100644 --- a/src/NNC_Polyhedron_defs.hh +++ b/src/NNC_Polyhedron_defs.hh @@ -249,6 +249,15 @@ public: //! Same as poly_hull_assign_if_exact(y). bool upper_bound_assign_if_exact(const NNC_Polyhedron& y); + + /*! \brief + Assigns to \p *this the result of computing the + "positive time-elapse" between \p *this and \p y. + + \exception std::invalid_argument + Thrown if \p *this and \p y are dimension-incompatible. + */ + void positive_time_elapse_assign(const Polyhedron& y); }; #include "NNC_Polyhedron_inlines.hh" diff --git a/src/Polyhedron_defs.hh b/src/Polyhedron_defs.hh index c967f42..0f36dc3 100644 --- a/src/Polyhedron_defs.hh +++ b/src/Polyhedron_defs.hh @@ -2830,6 +2830,8 @@ protected: static bool add_to_system_and_check_independence(Linear_System1& eq_sys, const Row2& eq); + + void positive_time_elapse_assign(const Polyhedron& y); }; #include "Ph_Status_inlines.hh" diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index 06f0977..984bcc7 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -228,7 +228,7 @@ PPL::Polyhedron::Polyhedron(const Topology topol, const Generator_System& gs) // Even though `gs_copy' has pending generators, since the // constraints of the polyhedron are not up-to-date, the // polyhedron cannot have pending generators. By integrating the - // pending part of `gen_sys' we may loose sortedness. + // pending part of `gen_sys' we may lose sortedness. gen_sys.set_sorted(false); gen_sys.unset_pending_rows(); } @@ -2212,6 +2212,170 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* vars_p, } void +PPL::Polyhedron::positive_time_elapse_assign(const Polyhedron& y) { + // Private method: the caller must ensure the following. + PPL_ASSERT(!is_necessarily_closed()); + + Polyhedron& x = *this; + // Dimension-compatibility checks. + if (x.space_dim != y.space_dim) + throw_dimension_incompatible("positive_time_elapse_assign(y)", "y", y); + + // Dealing with the zero-dimensional case. + if (x.space_dim == 0) { + if (y.marked_empty()) + x.set_empty(); + return; + } + + // If either one of `x' or `y' is empty, the result is empty too. + if (x.marked_empty() || y.marked_empty() + || (x.has_pending_constraints() && !x.process_pending_constraints()) + || (!x.generators_are_up_to_date() && !x.update_generators()) + || (y.has_pending_constraints() && !y.process_pending_constraints()) + || (!y.generators_are_up_to_date() && !y.update_generators())) { + x.set_empty(); + return; + } + + // At this point both generator systems are up-to-date, + // possibly containing pending generators. + + // The new system of generators that will replace the one of x. + Generator_System new_gs(x.gen_sys); + dimension_type num_rows = new_gs.num_rows(); + + // We are going to do all sorts of funny things with new_gs, so we better + // mark it unsorted. + // Notice: "Sorted" is an attribute of Linear_System, encapsulated by Generator_System; + // hence, the following is equivalent to new_gs.set_sorted(false). + new_gs.sys.set_sorted(false); + + // DEBUG + // std::cout << std::endl << "new_gs 1 (" << new_gs.num_rows() << "): "; + // new_gs.ascii_dump(std::cout); + + // Remove all points from new_gs and put them in 'x_points_gs' for later use. + // Notice that we do not remove the corresponding closure points. + Generator_System x_points_gs; + for (dimension_type i = num_rows; i-- > 0;) { + Generator &g = new_gs.sys.rows[i]; + if (g.is_point()) { + x_points_gs.insert(g); + num_rows--; + swap(g, new_gs.sys.rows[num_rows]); + } + } + new_gs.sys.rows.resize(num_rows); + + // When there are no pending rows, the pending row index points at + // the smallest non-valid row, i.e., it is equal to the number of rows. + // Hence, each time the system is manually resized, the pending row index + // must be updated. + new_gs.unset_pending_rows(); + PPL_ASSERT(new_gs.sys.OK()); + + // We use a pointer in order to avoid copying the generator + // system when it is not necessary, i.e., when y is an NNC. + const Generator_System *gs = &y.gen_sys; + Generator_System y_gs; + + // If y is closed, promote its generator system to not necessarily closed. + if (y.is_necessarily_closed()) { + y_gs = y.gen_sys; + y_gs.convert_into_non_necessarily_closed(); + y_gs.add_corresponding_closure_points(); + gs = &y_gs; + } + + PPL_ASSERT(gs->OK()); + //gs->ascii_dump(std::cout); + //IO_Operators::operator<<(std::cout, *gs); + + const dimension_type gs_num_rows = gs->num_rows(); + + // For each generator g of y... + for (dimension_type i = gs_num_rows; i-- > 0; ) { + const Generator &g = gs->sys.rows[i]; + + switch (g.type()) { + case Generator::POINT: + // In principle, points should be added to new_gs as rays. + // However, for each point there is a corresponding closure point in "gs". + // Hence, we leave this operation to closure points. + + // Insert into new_gs the sum of g and each point of x. + // For each original point gx of x... + for (dimension_type j = x_points_gs.sys.num_rows(); j-- > 0; ) { + const Generator &gx = x_points_gs.sys.rows[j]; + PPL_ASSERT(gx.is_point()); + // ...insert the point obtained as the sum of g and gx. + Generator new_g = g; // make a copy + Coefficient new_divisor = g.expr.inhomogeneous_term() * gx.expr.inhomogeneous_term(); + + new_g.expr.linear_combine(gx.expr, gx.expr.inhomogeneous_term(), g.expr.inhomogeneous_term()); + new_g.expr.set_inhomogeneous_term(new_divisor); + if (new_g.is_not_necessarily_closed()) { + new_g.set_epsilon_coefficient(g.epsilon_coefficient()); + } + new_g.expr.normalize(); + + // DEBUG + // std::cout << std::endl << "g:"; + // IO_Operators::operator<<(std::cout, g.expr); + // std::cout << std::endl << "gx:"; + // IO_Operators::operator<<(std::cout, gx.expr); + // std::cout << std::endl << "new_g:"; + // IO_Operators::operator<<(std::cout, new_g.expr); + + PPL_ASSERT(new_g.OK()); + + new_gs.insert(new_g); + } + break; + case Generator::CLOSURE_POINT: + // If g is not the origin, insert g into new_gs, as a ray. + if (!g.expr.all_homogeneous_terms_are_zero()) { + // Turn a copy of g into a ray. + Generator g_as_a_ray = g; + g_as_a_ray.expr.set_inhomogeneous_term(0); + g_as_a_ray.expr.normalize(); + PPL_ASSERT(g_as_a_ray.OK()); + // Insert the ray. + new_gs.insert(g_as_a_ray); + } + break; + case Generator::RAY: + case Generator::LINE: + // Insert g into new_gs. + new_gs.insert(g); + break; + } + } + new_gs.add_corresponding_closure_points(); + // Notice: add_corresponding_closure_points adds them as pending. + new_gs.unset_pending_rows(); + + //Polyhedron new_x(...,new_gs); + //swap(x,new_x); + + PPL_ASSERT(new_gs.sys.OK()); + + // Stealing the rows from `new_gs'. + using std::swap; + swap(gen_sys, new_gs); + + gen_sys.set_sorted(false); + clear_generators_minimized(); + // Generators are now up-to-date. + set_generators_up_to_date(); + // Constraints are not up-to-date. + clear_constraints_up_to_date(); + + PPL_ASSERT_HEAVY(x.OK(true) && y.OK(true)); +} + +void PPL::Polyhedron::throw_invalid_argument(const char* method, const char* reason) const { std::ostringstream s;

1 0