Project

General

Profile

Bug #56 ยป two_counters.lus

Hamza Bourbouh, 10/06/2017 12:22 AM

 
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
    (1-1/1)