[PPL-devel] [GIT] ppl/ppl(floating_point): Started to test analysis on digital filters.

[Roberto Amadini]

Module: ppl/ppl
Branch: floating_point
Commit: dc276e0c0a15896719a929593f63414b32703952
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dc276e0c0a15896719a929593f63414b32703952

Author: Roberto Amadini <r.amadini at virgilio.it>
Date:   Mon Sep 28 20:03:16 2009 +0200

Started to test analysis on digital filters.
Temporarily modified tests/Floating_Point_Expression/Makefile.am

---

 tests/Floating_Point_Expression/Makefile.am        |    9 +-
 tests/Floating_Point_Expression/digitalfilters1.cc |  113 ++++++++++++++++++++
 tests/Floating_Point_Expression/octagonalshape2.cc |    1 -
 3 files changed, 119 insertions(+), 4 deletions(-)

diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am
index d2f12e8..fd77e8a 100644
--- a/tests/Floating_Point_Expression/Makefile.am
+++ b/tests/Floating_Point_Expression/Makefile.am
@@ -50,7 +50,8 @@ $(top_builddir)/tests/libppl_tests.a \
 $(top_builddir)/src/libppl.la \
 @extra_libraries@
 
-ORIGINAL_TESTS = polyhedron2
+ORIGINAL_TESTS = \
+digitalfilters1
 
 #bdshape1 \
 #floatingpointexpr1 \
@@ -58,7 +59,7 @@ ORIGINAL_TESTS = polyhedron2
 #octagonalshape1 \
 #octagonalshape2 \
 #polyhedron1 \
-polyhedron2
+#polyhedron2
 
 
 
@@ -131,7 +132,9 @@ print_INSTANCES:
 # Sources for the tests
 #
 
-polyhedron2_SOURCES = polyhedron2.cc
+digitalfilters1_SOURCES = digitalfilters1.cc
+
+#polyhedron2_SOURCES = polyhedron2.cc
 
 #polyhedron1_SOURCES = polyhedron1.cc
 
diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc
new file mode 100644
index 0000000..2df3586
--- /dev/null
+++ b/tests/Floating_Point_Expression/digitalfilters1.cc
@@ -0,0 +1,113 @@
+/* Test Rate Limiter on differents abstract domains.
+   Copyright (C) 2001-2009 Roberto Bagnara <bagnara at cs.unipr.it>
+
+This file is part of the Parma Polyhedra Library (PPL).
+
+The PPL is free software; you can redistribute it and/or modify it
+under the terms of the GNU General Public License as published by the
+Free Software Foundation; either version 3 of the License, or (at your
+option) any later version.
+
+The PPL is distributed in the hope that it will be useful, but WITHOUT
+ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program; if not, write to the Free Software Foundation,
+Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
+
+For the most up-to-date information see the Parma Polyhedra Library
+site: http://www.cs.unipr.it/ppl/ . */
+
+#include "ppl_test.hh"
+
+namespace {
+
+/*
+This file tests a rate limiter that, given random input flows of floating
+point values X and D, bounded respectively by [-128, 128] and [0, 16],
+computes an output flow Y that tries to follow X while having a change rate
+limited by D. The pseudo-code of such rate limiter is the following:
+
+input X, D;
+output Y;
+R = (-inf, +inf);
+S = (-inf, +inf);
+for (n = 0; n < N; ++n) {
+  S = Y;
+  R = X - S;
+  Y = X;
+  if (R <= -D)
+    Y = S - D;
+  if (R >= D)
+    Y = S + D;
+}
+*/
+
+// tests rate limiter using intervals abstract domain.
+bool
+test01() {
+  Variable X(0); //input
+  Variable D(1); //input
+  Variable Y(2); //output
+  Variable S(3);
+  Variable R(4);
+  FP_Interval_Abstract_Store abstract_store(5);
+  FP_Interval tmp(-128);
+  tmp.join_assign(128);
+  abstract_store.set_interval(X, tmp);
+  abstract_store.set_interval(Y, tmp);
+  tmp.lower() = 0;
+  tmp.upper() = 16;
+  abstract_store.set_interval(D, tmp);
+
+  //if (R <= -D) Y = S - D;
+  FP_Interval_Abstract_Store as_then(abstract_store);
+  as_then.refine_with_constraint(R <= -D);
+  as_then.set_interval(Y, abstract_store.get_interval(S)
+                        - abstract_store.get_interval(D));
+  abstract_store.refine_with_constraint(R > -D);
+  abstract_store.upper_bound_assign(as_then);
+
+  //if (R >= D)  Y = S + D;
+  as_then = abstract_store;
+  as_then.refine_with_constraint(R >= D);
+  as_then.set_interval(Y, abstract_store.get_interval(S)
+                        + abstract_store.get_interval(D));
+  abstract_store.refine_with_constraint(R > D);
+  abstract_store.upper_bound_assign(as_then);
+
+  nout << "Y in " << abstract_store.get_interval(Y) << endl;
+  return true;
+}
+
+// tests rate limiter using bounded differences abstract domain.
+bool
+test02() {
+
+  return true;
+}
+
+// tests rate limiter using octagons abstract domain.
+bool
+test03() {
+
+  return true;
+}
+
+// tests rate limiter using polyhedra abstract domain.
+bool
+test04() {
+
+  return true;
+}
+
+} // namespace
+
+BEGIN_MAIN
+  DO_TEST(test01);
+  //DO_TEST(test02);
+  //DO_TEST(test03);
+  //DO_TEST(test04);
+END_MAIN
diff --git a/tests/Floating_Point_Expression/octagonalshape2.cc b/tests/Floating_Point_Expression/octagonalshape2.cc
index 5a869ec..8c8ac96 100644
--- a/tests/Floating_Point_Expression/octagonalshape2.cc
+++ b/tests/Floating_Point_Expression/octagonalshape2.cc
@@ -29,7 +29,6 @@ namespace {
 bool
 test01() {
   Variable A(0);
-  Variable B(1);
   FP_Octagonal_Shape oc1(0);
   bool ok1 = false;
   FP_Linear_Form l1(A);