Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / two_counters_e7_222.lus @ b745c1a8

History | View | Annotate | Download (473 Bytes)

1

    
2
node greycounter (x:bool) returns (out:bool);
3
var a,b:bool;
4
let
5
  a = false -> not pre(b);
6
  b = false -> pre(a);
7
  out = a or b;
8
tel
9
node intloopcounter (x:bool) returns (out:bool);
10
var time: int;
11
let
12
  time = 0 -> if pre(time) = 3 then 0
13
            else pre time + 1;
14
  out = (time = 2);
15
tel
16
node top (x:bool) returns (OK:bool);
17
--@ contract guarantee OK;
18
var b,d:bool;
19
let
20
  b = greycounter(x);
21
  d = intloopcounter(x);
22
  OK = b = d;
23
  --%MAIN;
24
  --%PROPERTY  OK;
25
tel