Project

General

Profile

Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/simulation/cd_e7_8.lus

View differences:

regression_tests/lustre_files/success/kind_fmcad08/simulation/cd_e7_8.lus
23 23
  cpt = 0 -> if acceptable then 0 else pre(cpt)+1;
24 24
  ok = true -> (pre cpt<=7);
25 25
tel
26
--@ ensures OK;
27 26
node top(diff:int) returns (OK: bool);
27
--@ contract guarantees OK;
28 28
var speed: int; 
29 29
    plus,minus,realistic: bool;
30 30
let

Also available in: Unified diff