Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / simulation / speed2.lus @ 2d37a1e1

History | View | Annotate | Download (1022 Bytes)

1
node COUNTER(init,incr:int;X,reset:bool) returns (C:int);
2
var PC: int;
3
let
4
  PC = init -> pre C;
5
  C = if reset then init
6
      else if X then (PC+incr)
7
      else PC;
8
tel
9

    
10

    
11
node speed(beacon,second:bool) returns (late,early:bool);
12
var
13
  diff,incr:int;
14
let
15
  incr = if (beacon and not second) then 1
16
         else if (second and not beacon) then 2
17
         else 0;
18
  diff = COUNTER(0,incr,(beacon or second),false);
19
  early = false -> if pre early then (diff > 0)
20
                   else (diff >= 10);
21
  late = false -> if pre late then (diff < 0)
22
                  else (diff <= -10);
23
tel
24
--subrange [0, 2] of int
25
node top(beacon,second:bool) returns (OK:bool);
26
--@ contract guarantees OK;
27
var late,early: bool;
28
let
29
  (late,early) = speed(beacon,second);
30

    
31
  OK = true -> not pre early or not late;
32

    
33
  --cannot go directly from early to late (valid)
34

    
35
  -- always was early and is not late; incorrect
36
--  --%PROPERTY true -> not late and pre early;
37

    
38
  -- if was early, will not next be late; correct
39
  --%PROPERTY OK; 
40
tel