Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (782 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
node speed(beacon,second:bool) returns (late,early:bool);
10
var
11
  diff,incr:int;
12
let
13
  incr = if (beacon and not second) then 1
14
         else if (second and not beacon) then 2
15
         else 0;
16
  diff = COUNTER(0,incr,(beacon and second),false);
17
  early = false -> if pre early then (diff > 0)
18
                   else (diff >= 10);
19
  late = false -> if pre late then (diff < 0)
20
                  else (diff <= -10);
21
tel
22
node top(beacon,second:bool) returns (OK:bool);
23
var late,early: bool;
24
let
25
  (late,early) = speed(beacon,second);
26
  OK = true -> not pre early or not late;
27
  --%MAIN;
28
  --%PROPERTY OK=true;
29
tel