Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (565 Bytes)

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