Module: ppl/ppl
Branch: master
Commit: 8391990970df4c26d8bccc9ad41d68beaea99f50
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8391990970df…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Mon Oct 28 09:19:59 2013 +0100
Updated.
---
NEWS | 4 +++-
1 files changed, 3 insertions(+), 1 deletions(-)
diff --git a/NEWS b/NEWS
index 2b035af..3fc1d9b 100644
--- a/NEWS
+++ b/NEWS
@@ -9,12 +9,14 @@ Parma Polyhedra Library NEWS -- history of user-visible changes
===============================================================
--------------------------------------------------------------------------
-NEWS for version 1.1 (released date to be decided)
+NEWS for version 1.1 (released on October 28, 2013)
--------------------------------------------------------------------------
New and Changed Features
========================
+o Added a new operator on polyhedra: the positive time elapse.
+
o In the Java language interface:
- The constraint/generator/... system classes now extend the ArrayList
Module: ppl/ppl
Branch: master
Commit: 346cfc0d619893a05f79da7d53e454f556da5c6b
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=346cfc0d6198…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Mon Oct 28 09:04:37 2013 +0100
Label updated.
---
doc/definitions.dox | 2 +-
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/doc/definitions.dox b/doc/definitions.dox
index eae3ce5..6565e52 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -1586,7 +1586,7 @@ Note that the above set might not be an NNC polyhedron.
\subsection Positive_Time_Elapse_Operator Positive Time-Elapse Operator
The <EM>positive time-elapse</EM> operator has been defined in
-\ref BFM11 "[BFM11,BFM12]".
+\ref BFM11 "[BFM11,BFM13]".
The operator provided by the library works on NNC
polyhedra. For any two NNC polyhedra \f$\cP, \cQ \in \Pset_n\f$, the
positive time-elapse between \f$\cP\f$ and \f$\cQ\f$, denoted \f$ \cP
Module: ppl/ppl
Branch: master
Commit: 81b01e9b60766bec50569a1ef68dc22d70de0a65
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=81b01e9b6076…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Mon Oct 28 09:03:22 2013 +0100
BenerecettiFM13 has been published.
---
doc/definitions.dox | 45 ++++++++++++++++++++++++---------------------
doc/ppl.bib | 26 ++++++++++++++++++++++++--
2 files changed, 48 insertions(+), 23 deletions(-)
diff --git a/doc/definitions.dox b/doc/definitions.dox
index b5c6007..eae3ce5 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -3070,6 +3070,30 @@ R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, and E. Z
</DD>
+<DT>[BFM11]</DT>
+<DD>
+\anchor BFM11
+M. Benerecetti, M. Faella, and S. Minopoli.
+ Towards efficient exact synthesis for linear hybrid systems.
+ In <em>Proceedings of 2nd International Symposium on Games,
+ Automata, Logics and Formal Verification (GandALF 2011)</em>, volume 54 of <em>
+ Electronic Proceedings in Theoretical Computer Science</em>, pages 263-277,
+ Minori, Amalfi Coast, Italy, 2011.
+
+</DD>
+
+
+<DT>[BFM13]</DT>
+<DD>
+\anchor BFM13
+M. Benerecetti, M. Faella, and S. Minopoli.
+ Automatic synthesis of switching controllers for linear hybrid
+ systems: Safety control.
+ <em>Theoretical Computer Science</em>, 493:116-138, 2013.
+
+</DD>
+
+
<DT>[BFT00]</DT>
<DD>
\anchor BFT00
@@ -3542,27 +3566,6 @@ R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill.
</DD>
-<DT>[BFM11]</DT>
-<DD>
-\anchor BFM11
-M. Benerecetti, M. Faella, and S. Minopoli.
- Towards efficient exact synthesis for Linear Hybrid Systems.
- In <em>Proceedings of the 2nd International Symposium on Games,
- Automata, Logics and Formal Verification (GandALF 2011)</em>,
- volume 54 of <em>Electronic Proceedings in Theoretical Computer Science</em>,
- pages 263-277.
-</DD>
-
-
-<DT>[BFM12]</DT>
-<DD>
-\anchor BFM12
-M. Benerecetti, M. Faella, and S. Minopoli.
- Automatic synthesis of switching controllers for Linear Hybrid Systems: safety control.
- <em>Theoretical Computer Science</em>, Elsevier. To appear.
-</DD>
-
-
<DT>[CC76]</DT>
<DD>
\anchor CC76
diff --git a/doc/ppl.bib b/doc/ppl.bib
index 02d4d18..cbb16bb 100644
--- a/doc/ppl.bib
+++ b/doc/ppl.bib
@@ -1249,12 +1249,34 @@ Summarizing:
top of the tool PHAVer."
}
-@Article{BenerecettiFM12,
+@Article{BenerecettiFM13,
Author = "M. Benerecetti and M. Faella and S. Minopoli",
Title = "Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Safety Control",
Journal = "Theoretical Computer Science",
+ Volume = 493,
+ Pages = "116--138",
Publisher = "Elsevier",
- Notes = "To appear"
+ Year = 2013,
+ Abstract = "In this paper we study the problem of automatically
+ generating switching controllers for the class of Linear
+ Hybrid Automata, with respect to safety
+ objectives. While the same problem has been already
+ considered in the literature, no sound and complete
+ solution has been provided so far. We identify and solve
+ inaccuracies contained in previous characterizations of
+ the problem, providing a sound and complete symbolic
+ fixpoint procedure to compute the set of states from
+ which a controller can keep the system in a given set of
+ desired states. While the overall procedure may not
+ terminate, we prove the termination of each iteration,
+ thus paving the way to an effective implementation. The
+ techniques needed to effectively and efficiently
+ implement the proposed solution procedure, based on
+ polyhedral abstractions of the state space, are
+ thoroughly illustrated and discussed. Finally, some
+ supporting and promising experimental results, based on
+ the implementation of the proposed techniques on top of
+ the tool PHAVer, are presented."
}
@InProceedings{BessonJT99,
Module: ppl/ppl
Branch: master
Commit: 24bf4c88063cbf59eac24068dcc2601e6e42981d
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=24bf4c88063c…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Mon Oct 28 08:52:27 2013 +0100
Updated.
---
demos/ppl_lcdd/ppl_lcdd.1 | 4 ++--
demos/ppl_lpsol/ppl_lpsol.1 | 4 ++--
demos/ppl_pips/ppl_pips.1 | 4 ++--
doc/ppl-config.1 | 4 ++--
4 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/demos/ppl_lcdd/ppl_lcdd.1 b/demos/ppl_lcdd/ppl_lcdd.1
index 7a8bf46..ff895ef 100644
--- a/demos/ppl_lcdd/ppl_lcdd.1
+++ b/demos/ppl_lcdd/ppl_lcdd.1
@@ -1,5 +1,5 @@
-.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.4.
-.TH PPL_LCDD "1" "June 2012" "ppl_lcdd 1.0" "User Commands"
+.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.11.
+.TH PPL_LCDD "1" "October 2013" "ppl_lcdd 1.1" "User Commands"
.SH NAME
ppl_lcdd \- a PPL-based program for vertex/facet enumeration of convex polyhedra
.SH SYNOPSIS
diff --git a/demos/ppl_lpsol/ppl_lpsol.1 b/demos/ppl_lpsol/ppl_lpsol.1
index 8b0044f..039821d 100644
--- a/demos/ppl_lpsol/ppl_lpsol.1
+++ b/demos/ppl_lpsol/ppl_lpsol.1
@@ -1,5 +1,5 @@
-.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.4.
-.TH PPL_LPSOL "1" "June 2012" "ppl_lpsol 1.0" "User Commands"
+.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.11.
+.TH PPL_LPSOL "1" "October 2013" "ppl_lpsol 1.1" "User Commands"
.SH NAME
ppl_lpsol \- a PPL-based mixed integer programming problem solver
.SH SYNOPSIS
diff --git a/demos/ppl_pips/ppl_pips.1 b/demos/ppl_pips/ppl_pips.1
index da2b2ea..c15f2d2 100644
--- a/demos/ppl_pips/ppl_pips.1
+++ b/demos/ppl_pips/ppl_pips.1
@@ -1,5 +1,5 @@
-.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.4.
-.TH PPL_PIPS "1" "June 2012" "ppl_pips 1.0" "User Commands"
+.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.11.
+.TH PPL_PIPS "1" "October 2013" "ppl_pips 1.1" "User Commands"
.SH NAME
ppl_pips \- a PPL-based parametric integer programming problem solver
.SH SYNOPSIS
diff --git a/doc/ppl-config.1 b/doc/ppl-config.1
index d03caac..92d7d49 100644
--- a/doc/ppl-config.1
+++ b/doc/ppl-config.1
@@ -1,5 +1,5 @@
-.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.4.
-.TH PPL-CONFIG "1" "June 2012" "ppl-config 1.0" "User Commands"
+.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.11.
+.TH PPL-CONFIG "1" "October 2013" "ppl-config 1.1" "User Commands"
.SH NAME
ppl-config \- obtain information about an installation of the Parma Polyhedra Library
.SH SYNOPSIS
Module: ppl/ppl
Branch: master
Commit: c0c660fe771942d58dd8834eccb04346dec9be3a
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c0c660fe7719…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Mon Oct 28 08:05:05 2013 +0100
Version number bumped.
---
configure.ac | 2 +-
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/configure.ac b/configure.ac
index 25ffd0c..39ade54 100644
--- a/configure.ac
+++ b/configure.ac
@@ -24,7 +24,7 @@
# Process this file with Autoconf to produce a configure script.
# Every other copy of the package version number gets its value from here.
-AC_INIT([the Parma Polyhedra Library], [1.1pre13], [ppl-devel(a)cs.unipr.it], [ppl])
+AC_INIT([the Parma Polyhedra Library], [1.1pre14], [ppl-devel(a)cs.unipr.it], [ppl])
# Minimum Autoconf version required.
AC_PREREQ(2.61)