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


68

(*@contract TriplexSignalMonitorSpec(Tlevel:real; ia:real; ib:real; ic:real; PCLimit: int; ) returns (FC: int; set_val: real; TC: int; PC: int);

69


70

Block Path: triplex_12B

71


72

let

73


74

var FTP:bool = true > false;

75

var C1:bool = abs(ia  ib) > Tlevel;

76

var C2:bool = abs(ib  ic) > Tlevel;

77

var C3:bool = abs(ia  ic) > Tlevel;

78

var miscompare : bool = (not C1 and C2 and C3) or (C1 and not C2 and C3) or (C1 and C2 and not C3);

79


80

var prePC: int = 0 > pre PC;

81

var pre_set_val : real = (0.0 > pre set_val);

82

var failure_in_progress : bool = miscompare and prePC <= PCLimit and PC > 0;

83

var failure_must_be_latched : bool = miscompare and prePC > PCLimit;

84

var no_fail : bool = (FC =0);

85

var pre_no_fail : bool = (true > pre no_fail);

86


87

var single_fail_reported : bool = (FC=1) or (FC=2) or (FC=4);

88

var mid_value : real = if ((ia <= ib and ib <= ic)

89

or (ic <= ib and ib <= ia))

90

then ib

91

else if ((ib <= ia and ia <= ic)

92

or (ic <= ia and ia <= ib))

93

then ia

94

else ic;

95

 Assumptions

96

assume PCLimit > 0 ;

97


98

 In the nofail state, a miscompare, which shall be characterized by one branch

99

 differing with the other two branches by a unique trip level that lasts for

100

 more than the persistence limit, shall be reported to failure management as

101

 a failure.

102

guarantee "TSM 001" S((( pre_no_fail and failure_must_be_latched) => single_fail_reported) and FTP , (( pre_no_fail and failure_must_be_latched) => single_fail_reported));

103


104

 In the nofail state, the midvalue shall be the selected value. Note: a first failure in progress will not affect the method for determining the selected value.

105

guarantee "TSM 002" S((( no_fail => set_val = mid_value) and FTP),(no_fail => set_val = mid_value));

106


107

 In the single fail state, a good channel average of the remaining two good branches shall be used to determine the selected value.

108

guarantee "TSM003a" S( ((FC = 1 => set_val = 0.5 * ( ia + ib )) and FTP), (FC = 1 => set_val = 0.5 * ( ia + ib )));

109

guarantee "TSM003b" S(((FC = 2 => set_val = 0.5 * ( ia + ic )) and FTP), (FC = 2 => set_val = 0.5 * ( ia + ic )));

110

guarantee "TSM003c" S(((FC = 4 => set_val = 0.5 * ( ib + ic )) and FTP), (FC = 4 => set_val = 0.5 * ( ib + ic )));

111


112

 If a second failure is in progress, the selected value shall remain unchanged from the previous selected value.

113

guarantee "TSM004" S( ((single_fail_reported and failure_in_progress => set_val = pre_set_val) and FTP), (single_fail_reported and failure_in_progress => set_val = pre_set_val));

114

tel

115

*)
