From bcde99fbe99174a094f38fdda70ad69d65a423f4 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 30 Apr 2014 17:19:08 +0200 Subject: Fist commit (WIP) --- tests/sources/0602_rate_limiter.c | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 tests/sources/0602_rate_limiter.c (limited to 'tests/sources/0602_rate_limiter.c') 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); -- cgit v1.2.3