Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / ex8.lus @ 65f71d05

History | View | Annotate | Download (888 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 65f71d05 ploc
--@ ensures OK;
25 22fe1c93 ploc
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 late and pre early;
31
32
  --cannot go directly from early to late (valid)
33
34
  -- always was early and is not late; incorrect
35
  --%PROPERTY OK=true;
36
37
tel