Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / Gas.lus @ 22fe1c93

History | View | Annotate | Download (1.19 KB)

1

    
2
-- Source: Bertrand Jeannet
3

    
4

    
5
node Sofar( X : bool ) returns ( Sofar : bool );
6
let
7
    Sofar = X -> X and pre Sofar;
8
tel
9

    
10
-- Counts the number of steps P has been continuously true
11
node Age(P1: bool) returns (Count:int);
12
let
13
  Count = 0 -> if pre(P1) then pre(Count)+1 else 0;             
14
tel 
15

    
16
-- Counts the number of time Q has been true 
17
-- since P has became false
18
node Dursince(P1,Q:bool) returns (Count:int);
19
let
20
  Count = 0 -> 
21
	if pre(P1) 
22
	then 0
23
        else (if pre(Q) then pre(Count)+1 else pre(Count));
24
tel
25

    
26
node RaisingEdge(P1 : bool) returns (res : bool);
27
let
28
  res = false -> not pre(P1) and P1;
29
tel
30

    
31
-- original version
32

    
33
-- leak is an input indicating a leak
34
-- P is a an input used to define the start of an observation
35

    
36
-- Not provable?
37
node top (leak,P1:bool) returns (OK : bool);
38
   var env : bool;
39
let
40
 -- we suppose that a leak lasts at most 10 steps,
41
 -- and that a raising edge of P implies
42
 -- no leak has happened since at least 300 steps.
43
    env = Sofar( Age(leak) <= 10) and
44
                 (not RaisingEdge(P1) or (300 <= Age(not leak)) );
45

    
46
     OK = env => ( (Age(not P1) <= 600) or
47
                   (2*Dursince(P1,leak) <= Age(not P1)));
48
     --%PROPERTY OK=true;
49
     --%MAIN;
50
 tel