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 integrator_12BSpec(BL:real; ic:real; reset:bool; T:real; TL:real; xin:real; ) returns (yout: real; );

63


64

Block Path: integrator_12B

65


66

let

67

var FTP:bool = true > false;

68

var xinpv: real = 0.0 > pre xin;

69

var ypv: real = 0.0 > pre yout;

70

var normal: bool = not reset and yout <= TL and yout >= BL;

71

var normal_yout : real = T * 0.5 * ( xin + xinpv ) + ypv;

72

assume BL <= TL;

73

assume T > 0.0;

74

guarantee "TUI002" S( ((yout <= TL and yout >= BL) and FTP), (yout <= TL and yout >= BL) );

75


76

guarantee "TUI001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP));

77


78

guarantee "TUI003V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout;

79

guarantee "TUI003" true > (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre ( not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre ( not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre ( not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));

80


81


82

tel
