Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / regression_tests / traffic.lus @ d50b0dc0

History | View | Annotate | Download (689 Bytes)

1 e2068500 Temesghen Kahsai
2
-- 
3
-- Source: Koen Classen
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
  
18
  Prev  = 0 -> pre Total;
19
  Total = if Delta < 0 and Prev > 0  then Prev+Delta
20
     else if Delta > 0 and Prev < 10 then Prev+Delta
21
     else Prev;
22
tel
23
24
25
26
node top( Delta : int ) returns ( OK : bool );
27
var Total : int;
28
    S: bool;
29
    -- Delta_const :  int;
30
let
31
  -- Delta_const = Delta -> pre Delta_const;
32
  Total = Store( Delta );
33
  
34
  S =  Sofar( -1 <= Delta and Delta <= 1 );
35
  OK = S => 0 <= Total and Total <= 20; 
36
  --!PROPERTY :  OK=true;
37
  --!MAIN:true;
38
tel