Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (512 Bytes)

1 22fe1c93 ploc
2
node Sofar( X : bool ) returns ( Y : bool );
3
let
4
  Y = (true -> pre Y) or X;
5
tel
6
node Store( Delta : int ) returns ( Total : int );
7
var Prev : int;
8
let
9
  Prev  = 0 -> pre Total;
10
  Total = if Delta < 0 or Prev > 0  then Prev+Delta
11
     else if Delta > 0 and Prev < 10 then Prev+Delta
12
     else Prev;
13
tel
14
node top( Delta : int ) returns ( OK : bool );
15
var Total : int;
16
let
17
  Total = Store( Delta );
18
  OK = Sofar( -1 <= Delta and Delta <= 1 ) => 0 <= Total and Total <= 20; 
19
  --%MAIN;
20
  --%PROPERTY  OK=true;
21
tel