Project

General

Profile

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

View differences:

regression_tests/lustre_files/success/kind_fmcad08/misc/durationThm_1_e1_350.lus
7 7
let
8 8
 age_of_p = 0 -> if pre(p) then pre(age_of_p) +1+ 1 else 0;
9 9
tel
10
--@ ensures OK;
11 10
node top (ik, im: int; p, q, r : bool) returns (OK: bool);
11
--@ contract guarantees OK;
12 12
var k,m : int;
13 13
    env : bool;
14 14
let

Also available in: Unified diff