## lustrec-tests/tests/cocospec/integrator_12BWithoutModesAndInitialization.lus @ f470cec6

1 | f470cec6 | hbourbou | ```
--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 "TUI-002" S( ((yout <= TL and yout >= BL) and FTP), (yout <= TL and yout >= BL) ); |
||

75 | |||

76 | guarantee "TUI-001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP)); |
||

77 | |||

78 | guarantee "TUI-003-V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout; |
||

79 | ```
--guarantee "TUI-003" 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
``` |