blob: a36da77839a9944460da080862c4caa4c359dad2 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
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);
|
