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

@ contract guarantees OK;

39

var env : bool;

40

let

41

 we suppose that a leak lasts at most 10 steps,

42

 and that a raising edge of P implies

43

 no leak has happened since at least 300 steps.

44

env = Sofar( Age(leak) <= 10) and

45

(not RaisingEdge(P1) or (300 <= Age(not leak)) );

46


47

OK = env => ( (Age(not P1) <= 600) or

48

(2*Dursince(P1,leak) <= Age(not P1)));

49

%PROPERTY OK=true;

50

%MAIN;

51

tel
