[PPL-devel] [GIT] ppl/ppl(floating_point): Added a preliminary version of test05. Edited previous tests.

[Roberto Amadini]

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

Author: Roberto Amadini <r.amadini at virgilio.it>
Date:   Tue Sep 29 13:02:52 2009 +0200

Added a preliminary version of test05. Edited previous tests.

---

 tests/Floating_Point_Expression/digitalfilters1.cc |   82 +++++++++++++++++++-
 1 files changed, 80 insertions(+), 2 deletions(-)

diff --git a/tests/Floating_Point_Expression/digitalfilters1.cc b/tests/Floating_Point_Expression/digitalfilters1.cc
index 9061076..92af68a 100644
--- a/tests/Floating_Point_Expression/digitalfilters1.cc
+++ b/tests/Floating_Point_Expression/digitalfilters1.cc
@@ -116,6 +116,7 @@ test03() {
   oc.affine_image(R, FP_Linear_Form(X - S));
   oc.affine_image(Y, FP_Linear_Form(X));
 
+
   //if (R <= -D) Y = S - D;
   FP_Linear_Form lr(R);
   FP_Octagonal_Shape oc_then(oc);
@@ -136,7 +137,7 @@ test03() {
   tmp = abstract_store.get_interval(Y);
   nout << "Y in " << tmp << endl;
 
-  return tmp.is_bounded();
+  return (tmp.lower() == -136);
 }
 
 // tests rate limiter using polyhedra abstract domain.
@@ -195,6 +196,82 @@ test04() {
 
   tmp = abstract_store.get_interval(Y);
   nout << "Y in " << tmp << endl;
+  return (tmp.lower() == -128);
+}
+
+// tests rate limiter using octagons abstract domain and
+// FP_Linear_Form_Abstract_Store.
+bool
+test05() {
+  Variable X(0); //input
+  Variable D(1); //input
+  Variable Y(2); //output
+  Variable S(3); //last output
+  Variable R(4); //actual rate
+  Var_FP_Expression x(0);
+  Var_FP_Expression d(1);
+  Var_FP_Expression y(2);
+  Var_FP_Expression s(3);
+  Var_FP_Expression r(4);
+  FP_Linear_Form lx(X);
+  FP_Linear_Form ld(D);
+  FP_Linear_Form ly(Y);
+  FP_Linear_Form ls;
+  FP_Linear_Form lr;
+  FP_Interval_Abstract_Store abstract_store(5);
+  FP_Linear_Form_Abstract_Store lf_abstract_store;
+  FP_Interval tmp(-128);
+  tmp.join_assign(128);
+  abstract_store.set_interval(X, tmp);
+  tmp.lower() = 0;
+  tmp.upper() = 16;
+  abstract_store.set_interval(D, tmp);
+  FP_Octagonal_Shape oc(abstract_store);
+
+  nout << "*** n = 0 ***" << endl;
+
+  //S = Y; R = X - S; Y = X;
+  oc.affine_image(S, ly);
+  //assign_linear_form
+  Var_FP_Expression* px = new Var_FP_Expression(0);
+  Var_FP_Expression* ps = new Var_FP_Expression(3);
+  Dif_FP_Expression x_dif_s(px, ps);
+  x_dif_s.linearize(abstract_store, lf_abstract_store, lr);
+  oc.affine_image(R, lr);
+  //assign_linear_form
+  oc.affine_image(Y, lx);
+  //assign_linear_form
+
+  //if (R <= -D) Y = S - D;
+  FP_Octagonal_Shape oc_then(oc);
+  oc_then.refine_with_linear_form_inequality(lr, -ld);
+  Var_FP_Expression* ps1 = new Var_FP_Expression(3);
+  Var_FP_Expression* pd  = new Var_FP_Expression(2);
+  Dif_FP_Expression s1_dif_d(ps1, pd);
+  s1_dif_d.linearize(abstract_store, lf_abstract_store, ly);
+  oc_then.affine_image(Y, ly);
+  //assign_linear_form
+  oc.refine_with_linear_form_inequality(-ld, lr);
+  oc.upper_bound_assign(oc_then);
+  oc.refine_fp_interval_abstract_store(abstract_store);
+  //lub on FP_Interval_abstract_store
+
+  //if (R >= D)  Y = S + D;
+  oc_then = oc;
+  oc_then.refine_with_linear_form_inequality(ld, lr);
+  Var_FP_Expression* ps2 = new Var_FP_Expression(3);
+  Var_FP_Expression* pd1  = new Var_FP_Expression(2);
+  Sum_FP_Expression s2_sum_d1(ps2, pd1);
+  s2_sum_d1.linearize(abstract_store, lf_abstract_store, ly);
+  oc_then.affine_image(Y, ly);
+  //assign_linear_form
+  oc.refine_with_linear_form_inequality(lr, ld);
+  oc.upper_bound_assign(oc_then);
+  oc.refine_fp_interval_abstract_store(abstract_store);
+  //lub on FP_Interval_abstract_store
+
+  tmp = abstract_store.get_interval(Y);
+  nout << "Y in " << tmp << endl;
   return tmp.is_bounded();
 }
 
@@ -202,7 +279,8 @@ test04() {
 
 BEGIN_MAIN
   DO_TEST(test01);
-  //DO_TEST(test02);
+  DO_TEST(test02);
   DO_TEST(test03);
   DO_TEST(test04);
+  DO_TEST(test05);
 END_MAIN