Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / _6countern.lus @ 2d37a1e1

History | View | Annotate | Download (194 Bytes)

1
node top (init:int) returns (OK:bool);
2
--@ contract guarantees OK;
3
var time:int;
4
let
5
  time = 0 -> if pre time = 5 then 0 
6
              else pre time + 1;
7
  OK = time <0;
8
  --%PROPERTY OK;
9
tel