Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (579 Bytes)

1
--
2
-- Source: Koen Classen
3
--
4

    
5
-- given
6

    
7
node Sofar( X : bool ) returns ( Y : bool );
8
let
9
  Y = (true -> pre Y) and X;
10
tel
11

    
12
-- assignment other
13

    
14
node Store( Delta : int ) returns ( Total : int );
15
var Prev : int;
16
let
17
  Prev  = 0 -> pre Total;
18
  Total = if Delta < 0 and Prev > 0  then Prev+Delta
19
     else if Delta > 0 and Prev < 10 then Prev+Delta
20
     else Prev;
21
tel
22

    
23
node top( Delta : int ) returns ( OK : bool );
24
var Total : int;
25
let
26
  Total = Store( Delta );
27
  
28
  OK = Sofar( -1 <= Delta and Delta <= 1 ) => 0 <= Total and Total <= 20; 
29
  --%PROPERTY OK=true;
30
  --%MAIN;
31
tel