Bug #56 ยป two_counters.lus
1 |
-- a simple boolean ant int counter
|
---|---|
2 |
|
3 |
|
4 |
node greycounter (x:bool) returns (out:bool); |
5 |
var a,b:bool; |
6 |
let
|
7 |
a = false -> not pre(b); |
8 |
b = false -> pre(a); |
9 |
out = a and b; |
10 |
tel
|
11 |
|
12 |
node intloopcounter (x:bool) returns (out:bool); |
13 |
var time: int; |
14 |
let
|
15 |
time = 0 -> if pre(time) = 3 then 0 |
16 |
else pre time + 1; |
17 |
out = (time = 2); |
18 |
tel
|
19 |
|
20 |
|
21 |
|
22 |
node two_counters (x:bool) returns (OK:bool); |
23 |
var b,d:bool; |
24 |
let
|
25 |
b = greycounter(x); |
26 |
d = intloopcounter(x); |
27 |
OK = b = d; |
28 |
--%PROPERTY OK=true;
|
29 |
tel
|