## lustrec-tests / tests / cocospec / TriplexSignalMonitorSpec.lus @ 6ccfcb12

History | View | Annotate | Download (5.75 KB)

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 | node abs(x:real) |
||

63 | returns(y:real); |
||

64 | let |
||

65 | y = if x >= 0.0 then x else - x; |
||

66 | tel |
||

67 | node max(x1, x2:real) |
||

68 | returns(y:real); |
||

69 | let |
||

70 | y = if x1 >= x2 then x1 else x2; |
||

71 | tel |
||

72 | |||

73 | node min(x1, x2:real) |
||

74 | returns(y:real); |
||

75 | let |
||

76 | y = if x1 >= x2 then x2 else x1; |
||

77 | tel |
||

78 | |||

79 | node ToInt (X: bool) returns (N: int) ; |
||

80 | let |
||

81 | N = if X then 1 else 0 ; |
||

82 | tel |
||

83 | |||

84 | node Count (X: bool) returns (N: int) ; |
||

85 | let |
||

86 | N = ToInt(X) -> ToInt(X) + pre N ; |
||

87 | tel |
||

88 | |||

89 | bd3f748f | ploc | (*@ |

90 | f470cec6 | hbourbou | contract TriplexSignalMonitorSpec(Tlevel:real; ia:real; ib:real; ic:real; PCLimit: int; ) returns (FC: int; set_val: real; TC: int; PC: int); |

91 | |||

92 | --Block Path: triplex_12B |
||

93 | |||

94 | let |
||

95 | var FTP:bool = true -> false; |
||

96 | var absAB: real = abs(ia - ib); |
||

97 | var absAC: real = abs(ia - ic); |
||

98 | var absBC: real = abs(ib - ic); |
||

99 | var avg: real = (ia + ib + ic) / 3.0; |
||

100 | var mid_value:real = if (abs(ia - avg) > abs(ic - avg) and abs(ib - avg) > abs(ic - avg)) then ic |
||

101 | else if (abs(ia - avg) > abs(ib - avg)) then ib |
||

102 | else ia; |
||

103 | var preFC: int = 0 -> pre FC; |
||

104 | var prePC: int = 0 -> pre PC; |
||

105 | var prePCLimit: int = 0 -> pre PCLimit; |
||

106 | var prevSet_val: real = 0.0 -> pre set_val; |
||

107 | -- calculate is_a_miscompare |
||

108 | var C1:bool = absAB > Tlevel; |
||

109 | var C2:bool = absBC > Tlevel; |
||

110 | var C3:bool = absAC > Tlevel; |
||

111 | var is_a_miscompare : bool = (not C1 and C2 and C3) or (C1 and not C2 and C3) or (C1 and C2 and not C3); |
||

112 | |||

113 | -- Assumptions |
||

114 | assume PCLimit > 0 ; |
||

115 | assume true -> PCLimit = prePCLimit; |
||

116 | assume true -> Tlevel = pre Tlevel; |
||

117 | |||

118 | -- when preFC = 0 & prePC > prePCLimit TriplexSignalMonitor shall immediately satisfy FC > 0 |
||

119 | 6ccfcb12 | hbourbou | guarantee "RM001" S( (((preFC = 0 and prePC > prePCLimit) => (FC > 0)) and FTP), ((preFC = 0 and prePC > prePCLimit) => (FC > 0)) ); |

120 | guarantee "RM001V2" is_a_miscompare and prePC > PCLimit => FC > 0; |
||

121 | f470cec6 | hbourbou | |

122 | -- when FC =1 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ib) |
||

123 | 6ccfcb12 | hbourbou | guarantee "RM003a" (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )) or (S( ((set_val = 0.5 * ( ia + ib )) and ((FC = 1) and (FTP or (pre (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )))))), (set_val = 0.5 * ( ia + ib )) )); |

124 | guarantee "RM003aV2" FC = 1 => set_val = 0.5 * (ia +ib); |
||

125 | f470cec6 | hbourbou | |

126 | -- when FC =2 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ic). |
||

127 | 6ccfcb12 | hbourbou | guarantee "RM003b" (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )) or (S( ((set_val = 0.5 * ( ia + ic )) and ((FC = 2) and (FTP or (pre (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )))))), (set_val = 0.5 * ( ia + ic )) )); |

128 | guarantee "RM003bV2" FC = 2 => set_val = 0.5 * (ia +ic); |
||

129 | f470cec6 | hbourbou | |

130 | |||

131 | -- when FC =4 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ib +ic) |
||

132 | 6ccfcb12 | hbourbou | guarantee "RM003c" (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )) or (S( ((set_val = 0.5 * ( ib + ic )) and ((FC = 4) and (FTP or (pre (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )))))), (set_val = 0.5 * ( ib + ic )) )); |

133 | guarantee "RM003cV2" FC = 4 => set_val = 0.5 * (ib +ic); |
||

134 | f470cec6 | hbourbou | |

135 | -- when preFC =0 TriplexSignalMonitor shall immediately satisfy set_val = mid_value |
||

136 | 6ccfcb12 | hbourbou | guarantee "RM002" S( (((preFC = 0) => (set_val = mid_value)) and FTP), ((preFC = 0) => (set_val = mid_value)) ); |

137 | guarantee "RM002V2" FC = 0 => set_val = mid_value; |
||

138 | f470cec6 | hbourbou | |

139 | -- when (absAB > Tlevel & absAC >Tlevel) | (absAB > Tlevel & absBC > Tlevel) | (absAC > Tlevel & absBC > Tlevel) TriplexSignalMonitor shall always satisfy set_val = prevSet_val |
||

140 | 6ccfcb12 | hbourbou | guarantee "RM004" (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )) or (S( ((set_val = prevSet_val) and ((( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel )) and (FTP or (pre (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )))))), (set_val = prevSet_val) )); |

141 | f470cec6 | hbourbou | |

142 | --Explanaton from document: |
||

143 | -- -A miscompare that persists but has not yet been declared failed is known as a failure in progress. |
||

144 | -- can be expressed as "is_a_miscompare and prePC > 0 and prePC < PCLimit" |
||

145 | -- -A second failure can be expressed as "Count(FC > 0) = 1" |
||

146 | --[RM-004] If a second failure is in progress, the selected value shall remain unchanged from the previous selected value. |
||

147 | guarantee "RM004V2" Count(FC > 0) = 1 and is_a_miscompare and prePC > 0 and prePC < PCLimit => set_val = prevSet_val; |
||

148 | |||

149 | 6ccfcb12 | hbourbou | guarantee true -> Count(FC > 0) = 1 and ia <> pre ia and ib <> pre ib and ic <> pre ic and prePC > 0 and prePC < PCLimit => set_val <> prevSet_val; |

150 | f470cec6 | hbourbou | tel |

151 | bd3f748f | ploc | *) |