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

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

(*@

90

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

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


122

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

123

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


126

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

127

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


130


131

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

132

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


135

 when preFC =0 TriplexSignalMonitor shall immediately satisfy set_val = mid_value

136

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


139

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

140

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


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

[RM004] 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

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

tel

151

*)
