Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / machine_types / kind_fmcad / two_counters.lus @ 2d37a1e1

History | View | Annotate | Download (540 Bytes)

1 8af9a0b9 ploc
-- a simple boolean ant int counter
2
3
node greycounter (x:bool) returns (out:bool);
4
var a,b:bool;
5
let
6
  a = false -> not pre(b);
7
  b = false -> pre(a);
8
  out = a and b;
9
tel
10
11
node intloopcounter (x:bool) returns (out:bool);
12
var time: int;
13
let
14
--! /machine_types/: (time, "uint8");
15
  time = 0 -> if pre(time) = 3 then 0
16
            else pre time + 1;
17
  out = (time = 2);
18
tel
19
20
21
node top (x:bool) returns (OK:bool);
22 2d37a1e1 ploc
--@ contract guarantees OK;
23 8af9a0b9 ploc
var b,d:bool;
24
let
25
  b = greycounter(x);
26
  d = intloopcounter(x);
27
  OK = b = d;
28
  --%PROPERTY OK;
29
tel