Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / automata / with_properties / counters.lus @ 02d89bbb

History | View | Annotate | Download (1.02 KB)

1
-- a simple boolean ant int counter
2

    
3
node greycounter (x:bool) 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:bool) 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
node auto (x:bool) returns -- (out:bool);
20
 (_state: int);
21
let
22
  automaton four_states
23
  state One : 
24
  let 
25
 --   out = false;
26
    _state = 1;
27
  tel until true restart Two
28
  state Two : 
29
  let 
30
 --   out = false;
31
    _state = 2;
32
  tel until true restart Three
33
  state Three : 
34
  let 
35
--    out = true;
36
   _state = 3;
37
  tel until true restart Four
38
  state Four :
39
  let 
40
 --   out = false;
41
    _state = 4;
42
  tel until true restart One
43
tel
44

    
45

    
46

    
47
--@ ensures OK;
48
node top (x:bool) returns (OK:bool);
49
var a,b,d:bool;
50
    s:int;
51
    OK1,OK2,OK3: bool;
52
    
53
let
54
  b = greycounter(x);
55
  d = intloopcounter(x);
56
  s = auto(x);
57
  a = s= 3;
58
  OK1 = b = d;
59
  OK2 = b = a;
60
  OK3 = a = d;
61
  OK = OK3;
62
  --%PROPERTY OK;
63
tel