[PPL-devel] [GIT] ppl/ppl(floating_point): Modified test03 and test04.
Roberto Amadini
r.amadini at virgilio.it
Thu Oct 1 17:32:55 CEST 2009
Module: ppl/ppl
Branch: floating_point
Commit: f18c42ee75a560eb6221c759de4297b7db58bb7a
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f18c42ee75a560eb6221c759de4297b7db58bb7a
Author: Roberto Amadini <r.amadini at virgilio.it>
Date: Thu Oct 1 16:40:19 2009 +0200
Modified test03 and test04.
---
tests/Floating_Point_Expression/Makefile.am | 14 ++--
tests/Floating_Point_Expression/digitalfilters1.cc | 87 ++++++++++++++++++--
2 files changed, 85 insertions(+), 16 deletions(-)
diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am
index 27acb8a..b6d2a0c 100644
--- a/tests/Floating_Point_Expression/Makefile.am
+++ b/tests/Floating_Point_Expression/Makefile.am
@@ -136,19 +136,19 @@ digitalfilters1_SOURCES = digitalfilters1.cc
#bdshape2_SOURCE = bdshape2.cc
-polyhedron2_SOURCES = polyhedron2.cc
+#polyhedron2_SOURCES = polyhedron2.cc
-polyhedron1_SOURCES = polyhedron1.cc
+#polyhedron1_SOURCES = polyhedron1.cc
-bdshape1_SOURCES = bdshape1.cc
+#bdshape1_SOURCES = bdshape1.cc
-floatingpointexpr1_SOURCES = floatingpointexpr1.cc
+#floatingpointexpr1_SOURCES = floatingpointexpr1.cc
-linearform1_SOURCES = linearform1.cc
+#linearform1_SOURCES = linearform1.cc
-octagonalshape1_SOURCES = octagonalshape1.cc
+#octagonalshape1_SOURCES = octagonalshape1.cc
-octagonalshape2_SOURCES = octagonalshape2.cc
+#octagonalshape2_SOURCES = octagonalshape2.cc
#
diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc
index a0a5a40..63da991 100644
--- a/tests/Floating_Point_Expression/digitalfilters1.cc
+++ b/tests/Floating_Point_Expression/digitalfilters1.cc
@@ -112,7 +112,7 @@ test02() {
return true;
}
-// tests rate limiter using octagons abstract domain and
+// tests rate limiter using octagons abstract domain.
bool
test03() {
Variable X(0); //input
@@ -146,7 +146,6 @@ test03() {
//if (R <= -D) Y = S - D;
FP_Octagonal_Shape oc_then(oc);
- FP_Interval_Abstract_Store as_then(abstract_store);
oc_then.refine_with_linear_form_inequality(FP_Linear_Form(R),
-FP_Linear_Form(D));
oc_then.affine_image(Y, FP_Linear_Form(S - D));
@@ -154,12 +153,11 @@ test03() {
oc.refine_with_linear_form_inequality(-FP_Linear_Form(D),
FP_Linear_Form(R));
oc.upper_bound_assign(oc_then);
- abstract_store.upper_bound_assign(as_then);
- print_constraints(Box<FP_Interval>(oc) ,"*** if (R <= -D) Y = S - D; ***");
+ print_constraints(Box<FP_Interval>(oc) ,
+ "*** if (R <= -D) Y = S - D; ***");
//if (R >= D) Y = S + D;
oc_then = oc;
- as_then = abstract_store;
oc_then.refine_with_linear_form_inequality(FP_Linear_Form(D),
FP_Linear_Form(R));
oc_then.affine_image(Y, FP_Linear_Form(S + D));
@@ -168,8 +166,8 @@ test03() {
FP_Linear_Form(D));
oc.upper_bound_assign(oc_then);
- abstract_store.upper_bound_assign(as_then);
- print_constraints(Box<FP_Interval>(oc) ,"*** if (R >= D) Y = S + D; ***");
+ print_constraints(Box<FP_Interval>(oc) ,
+ "*** if (R >= D) Y = S + D; ***");
}
oc.refine_fp_interval_abstract_store(abstract_store);
@@ -178,17 +176,88 @@ test03() {
return tmp.is_bounded();
}
+// tests rate limiter using polyhedra abstract domain.
bool
test04() {
+ Variable X(0); //input
+ Variable D(1); //input
+ Variable Y(2); //output
+ Variable S(3); //last output
+ Variable R(4); //actual rate
+ FP_Interval_Abstract_Store abstract_store(5);
+ NNC_Polyhedron ph(abstract_store);
+ FP_Interval tmp(0);
+ abstract_store.set_interval(X, tmp);
+ abstract_store.set_interval(D, tmp);
+ abstract_store.set_interval(Y, tmp);
+ abstract_store.set_interval(S, tmp);
+ abstract_store.set_interval(R, tmp);
+ NNC_Polyhedron ph_begin;
- return true;
+ // Y = 0;
+ ph.affine_image(Y, FP_Linear_Form(tmp), abstract_store);
+
+ for(unsigned int n = 0; ph_begin != ph; ++n) {
+
+ nout << "*** n = " << n << " ***" << endl;
+ ph_begin = ph;
+
+ //X = [-128, 128]; D = [0, 16]; S = Y; R = X - S; Y = X;
+ tmp.lower() = -128;
+ tmp.upper() = 128;
+ ph.affine_image(X, FP_Linear_Form(tmp), abstract_store);
+ tmp.lower() = 0;
+ tmp.upper() = 16;
+ ph.affine_image(D, FP_Linear_Form(tmp), abstract_store);
+ ph.affine_image(S, FP_Linear_Form(Y), abstract_store);
+ ph.affine_image(R, FP_Linear_Form(X - S), abstract_store);
+ ph.affine_image(Y, FP_Linear_Form(X), abstract_store);
+
+ //if (R <= -D) Y = S - D;
+ NNC_Polyhedron ph_then(ph);
+ FP_Interval_Abstract_Store as_then(abstract_store);
+ ph_then.refine_with_linear_form_inequality(FP_Linear_Form(R),
+ -FP_Linear_Form(D),
+ abstract_store);
+ ph_then.affine_image(Y, FP_Linear_Form(S - D), abstract_store);
+
+ ph.refine_with_linear_form_inequality(-FP_Linear_Form(D),
+ FP_Linear_Form(R),
+ abstract_store);
+ ph.upper_bound_assign(ph_then);
+ abstract_store.upper_bound_assign(as_then);
+ print_constraints(Box<FP_Interval>(ph) ,
+ "*** if (R <= -D) Y = S - D; ***");
+
+ //if (R >= D) Y = S + D;
+ ph_then = ph;
+ as_then = abstract_store;
+ ph_then.refine_with_linear_form_inequality(FP_Linear_Form(D),
+ FP_Linear_Form(R),
+ abstract_store);
+ ph_then.affine_image(Y, FP_Linear_Form(S + D), abstract_store);
+
+ ph.refine_with_linear_form_inequality(FP_Linear_Form(R),
+ FP_Linear_Form(D),
+ abstract_store);
+
+ ph.upper_bound_assign(ph_then);
+ abstract_store.upper_bound_assign(as_then);
+ print_constraints(Box<FP_Interval>(ph) ,
+ "*** if (R >= D) Y = S + D; ***");
+ }
+
+ ph.refine_fp_interval_abstract_store(abstract_store);
+ tmp = abstract_store.get_interval(Y);
+ nout << "*** Y in " << tmp << " ***" << endl;
+ return tmp.is_bounded();
}
} // namespace
BEGIN_MAIN
- DO_TEST(test01);
+ //DO_TEST(test01);
//DO_TEST(test02);
DO_TEST(test03);
//DO_TEST(test04);
More information about the PPL-devel
mailing list