Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / speed2.lus @ 22fe1c93

History | View | Annotate | Download (994 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
var late,early: bool;
27
let
28
  (late,early) = speed(beacon,second);
29

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

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

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

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