1 files changed, 26 insertions, 0 deletions
diff --git a/tests/sources/0602_rate_limiter.c b/tests/sources/0602_rate_limiter.c
new file mode 100644
index 0000000..a36da77
--- /dev/null
+++ b/tests/sources/0602_rate_limiter.c
@@ -0,0 +1,26 @@
+// Example from Miné HOSC 2006
+
+// Rate limiter: at each loop iteration, a new input is fetched (X) and
+// a new output (Y) is computed; Y tries to follow X but is limited to
+// change no more that a given slope (D) in absolute value
+
+// To prove that the assertion holds, this version needs the polyhedra
+// domain and an unrolling factor of at least 6
+
+int X;  // input
+int Y;  // output
+int S;  // last output
+int D;  // maximum slope;
+
+Y = 0;
+while (rand(0,1)==1) {
+  X = rand(-128,128);
+  D = rand(0,16);
+  S = Y;
+  int R = X - S; // current slope
+  Y = X;
+  if (R <= -D)     Y = S - D; // slope too small
+  else if (R >= D) Y = S + D; // slope too large
+}
+
+assert(Y >= -128 && Y <= 128);