1


2

node Sofar( X : bool ) returns ( Sofar : bool );

3

let

4

Sofar = X > X or pre Sofar;

5

tel

6

node Environment(diff: int; plus,minus: bool) returns (ok: bool);

7

let

8

ok = (4 <= diff and diff <= 4) and

9

(if (true > pre plus) then diff >= 1 else true) and

10

(if (false > pre minus) then diff <= 1 else true);

11

tel

12

node Controller(diff: int) returns (speed: int; plus,minus: bool);

13

let

14

speed = 0 > pre(speed)+diff;

15

plus = speed <= 9;

16

minus = speed >= 11;

17

tel

18

node Property(speed: int) returns (ok: bool);

19

var cpt: int;

20

acceptable: bool;

21

let

22

acceptable = 8 <= speed and speed <= 12;

23

cpt = 0 > if acceptable then 0 else pre(cpt)+1;

24

ok = true > (pre cpt<=7);

25

tel

26

node top(diff:int) returns (OK: bool);

27

@ contract guarantees OK;

28

var speed: int;

29

plus,minus,realistic: bool;

30

let

31

(speed,plus,minus) = Controller(diff);

32

realistic = Environment(diff,plus,minus);

33

OK = Sofar( realistic and 0 <= speed and speed < 16 ) => Property(speed);

34

%MAIN;

35

%PROPERTY OK=true;

36

tel
