Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / examples / two_counters / two_counters.lus @ 9b0432bc

History | View | Annotate | Download (453 Bytes)

1
-- a simple boolean ant int counter
2

    
3
node greycounter (x:int) returns (out:bool);
4
var a,b:bool;
5
let
6
  a = false -> not pre(b);
7
  b = false -> pre(a);
8
  out = a and b;
9
tel
10

    
11
node intloopcounter (x:int) returns (out:bool);
12
var time: int;
13
let
14
  time = 0 -> if pre(time) = 3 then 0
15
            else pre time + 1;
16
  out = (time = 2);
17
tel
18

    
19

    
20
node top (x:int) returns (OK:bool);
21
var b,d:bool;
22
let
23
  b = greycounter(x);
24
  d = intloopcounter(x);
25
  OK = b = d;
26
tel