Project

General

Profile

Revision 65f71d05 test/src/kind_fmcad08/misc/durationThm_2_e3_329_e4_1.lus

View differences:

test/src/kind_fmcad08/misc/durationThm_2_e3_329_e4_1.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;
10 11
node top (k0: int; p, q, r, t : bool) returns (OK: bool);
11 12
var k: int;
12 13
    env : bool;

Also available in: Unified diff