Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (700 Bytes)

1 b8dc00eb bourbouh
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
2
-- property is that it should never reach 6 or 7
3
4
node bool6 (x:bool) returns (out:bool);
5
var a,b,c: bool;
6
let
7
  a = false -> not pre(a);
8
  b = false -> (not pre(c) and not pre(b) and pre(a)) or
9
           (pre(b) and not pre(a));
10
  c = false -> (pre(c) and not pre(a)) or (pre(b) and pre(a));
11
  out = a and c;
12
tel
13
14
-- this resets to 1, not 0
15
node int6I (x:bool) returns (out:bool);
16
var time:int;
17
let
18
  time = 0 -> if pre time = 5 then 1
19
              else pre time + 1;
20
  out = time = 5;
21
tel
22
23
24
25
node top (x:bool) returns (OK:bool);
26 bd3f748f ploc
--@ contract guarantee OK;
27 b8dc00eb bourbouh
var a,b:bool;
28
let
29
  OK = a=b;
30
  a = int6I(x);
31
  b = bool6(x);
32
  --%PROPERTY OK;
33
tel