Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (449 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 and 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+ 1;
14
  out = (time = 2);
15
tel
16
node top (x:bool) returns (OK:bool);
17
var b,d:bool;
18
let
19
  b = greycounter(x);
20
  d = intloopcounter(x);
21
  OK = b = d;
22
  --%MAIN;
23
  --%PROPERTY  OK;
24
tel