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

History | View | Annotate | Download (2.38 KB)

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 "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 |