Project

General

Profile

Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/misc/traffic_e7_46.lus

View differences:

regression_tests/lustre_files/success/kind_fmcad08/misc/traffic_e7_46.lus
11 11
     else if Delta > 0 and Prev < 10 then Prev+Delta
12 12
     else Prev;
13 13
tel
14
--@ ensures OK;
15 14
node top( Delta : int ) returns ( OK : bool );
15
--@ contract guarantees OK;
16 16
var Total : int;
17 17
let
18 18
  Total = Store( Delta );

Also available in: Unified diff