1

Historically

2

node H(X:bool) returns (Y:bool);

3

let

4

Y = X > (X and (pre Y));

5

tel

6


7

Y since inclusive X

8

node SI(X,Y: bool) returns (Z:bool);

9

let

10

Z = Y and (X or (false > pre Z));

11

tel

12


13

Y since X

14

node S(X,Y: bool) returns (Z:bool);

15

let

16

Z = X or (Y and (false > pre Z));

17

tel

18


19

Once

20

node O(X:bool) returns (Y:bool);

21

let

22

Y = X or (false > pre Y);

23

tel

24


25

node First( X : bool ) returns ( Y : bool );

26

let

27

Y = X > pre Y;

28

tel

29


30

Timed Once: less than or equal to N

31

node OTlore(const N: int; X: bool; ) returns (Y: bool);

32

var C:int;

33

let

34

C = if X then 0

35

else (1 > pre C + (if pre C <0 then 0 else 1));

36


37

Y = First(X)

38

>

39

(if pre C < 0 then false

40

else C <= N

41

);

42

tel

43


44

 Timed Historically: less than or equal to N

45

node HTlore(const N: int; X: bool) returns (Y: bool);

46

let

47

Y = not OTlore(N, not X);

48

tel

49


50

 Timed Since: less than or equal to N

51

node STlore(const N: int; X: bool; Y: bool; ) returns (Z: bool);

52

let

53

Z = S(X, Y) and OTlore(N, X);

54

tel

55


56

 Timed Since Inclusive: less than or equal to N

57

node SITlore(const N: int; X: bool; Y: bool; ) returns (Z: bool);

58

let

59

Z = SI(X,Y) and OTlore(N, X);

60

tel

61


62

contract FSMSpec(apfail:bool; limits:bool; standby:bool; supported:bool; ) returns (pullup: bool; );

63


64

Block Path: fsm_12B

65


66

let

67


68

var FTP:bool = true > false;

69


70

guarantee "FSM001" S( (((limits and not standby and not apfail and supported) => (pullup)) and FTP), ((limits and not standby and not apfail and supported) => (pullup)) );

71

guarantee "FSM001V2" limits and not standby and not apfail and supported => pullup;

72


73

tel

74

