lustrec/optim/oversampling/oversampling0_denot.h @ 6a93d814
| 1 |
#include "streams_acsl.h"
|
|---|---|
| 2 |
|
| 3 |
/*
|
| 4 |
node f(x:int) returns (cpt, y:int )
|
| 5 |
let
|
| 6 |
y = x + 1;
|
| 7 |
cpt = (0 fby cpt) + 1;
|
| 8 |
tel
|
| 9 |
*/
|
| 10 |
|
| 11 |
/*@ predicate denot_f (stream<integer> x, stream<integer> cpt, stream<integer> y) =
|
| 12 |
(cpt = ite (_arrow, lift0 (0), pre(cpt)))
|
| 13 |
&& (y = iplus (x, lift0 (1)));
|
| 14 |
*/
|
| 15 |
|