Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / ex8.lus @ 22fe1c93

History | View | Annotate | Download (872 Bytes)

1 22fe1c93 ploc
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
node speed(beacon,second:bool) returns (late,early:bool);
11
var
12
  diff,incr:int;
13
let
14
  incr = if (beacon and not second) then 1
15
         else if (second and not beacon) then 2
16
         else 0;
17
  diff = COUNTER(0,incr,(beacon or second),false);
18
  early = false -> if pre early then (diff > 0)
19
                   else (diff >= 10);
20
  late = false -> if pre late then (diff < 0)
21
                  else (diff <= -10);
22
tel
23
24
node top(beacon,second:bool) returns (OK:bool);
25
var late,early: bool;
26
let
27
  (late,early) = speed(beacon,second);
28
29
  OK = true -> not late and pre early;
30
31
  --cannot go directly from early to late (valid)
32
33
  -- always was early and is not late; incorrect
34
  --%PROPERTY OK=true;
35
36
tel