1



2

 Source Bertrand Jeannet, NBAC tutorial

3



4


5

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

6

let

7

Sofar = X > X and pre Sofar;

8

tel

9


10

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

11

let

12

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

13

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

14

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

15

tel

16


17

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

18

let

19

speed = 0 > pre(speed)+diff;

20

plus = speed <= 9;

21

minus = speed >= 11;

22

tel

23


24

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

25

var cpt: int;

26

acceptable: bool;

27

let

28

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

29

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

30

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

31

tel

32


33

@ ensures OK;

34

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

35

var speed: int;

36

plus,minus,realistic: bool;

37

let

38

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

39

realistic = Environment(diff,plus,minus);

40


41

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

42

%PROPERTY OK=true;

43

%MAIN;

44

tel
