Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / _6counters_e8_371_e3_224.lus @ 22fe1c93

History | View | Annotate | Download (539 Bytes)

1 22fe1c93 ploc
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) and 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
var a,b:bool;
21
let
22
  OK = a=b;
23
  a = int6I(x);
24
  b = bool6(x);
25
  --%PROPERTY OK;
26
tel