## Bug #73 ยป TriplexSignalMonitorSpec.lus

 1 ```--Historically ``` ```node H(X:bool) returns (Y:bool); ``` ```let ``` ``` Y = X -> (X and (pre Y)); ``` ```tel ``` ```--Y since inclusive X ``` ```node SI(X,Y: bool) returns (Z:bool); ``` ```let ``` ```Z = Y and (X or (false -> pre Z)); ``` ```tel ``` ```--Y since X ``` ```node S(X,Y: bool) returns (Z:bool); ``` ```let ``` ```Z = X or (Y and (false -> pre Z)); ``` ```tel ``` ```--Once ``` ```node O(X:bool) returns (Y:bool); ``` ```let ``` ``` Y = X or (false -> pre Y); ``` ```tel ``` ```node First( X : bool ) returns ( Y : bool ); ``` ```let ``` ``` Y = X -> pre Y; ``` ```tel ``` ```--Timed Once: less than or equal to N ``` ```node OTlore(const N: int; X: bool; ) returns (Y: bool); ``` ``` var C:int; ``` ```let ``` ``` C = if X then 0 ``` ``` else (-1 -> pre C + (if pre C <0 then 0 else 1)); ``` ``` Y = First(X) ``` ``` -> ``` ``` (if C < 0 then false ``` ``` else C <= N ``` ``` ); ``` ```tel ``` ```-- Timed Historically: less than or equal to N ``` ```node HTlore(const N: int; X: bool) returns (Y: bool); ``` ```let ``` ``` Y = not OTlore(N, not X); ``` ```tel ``` ```-- Timed Since: less than or equal to N ``` ```node STlore(const N: int; X: bool; Y: bool; ) returns (Z: bool); ``` ```let ``` ``` Z = S(X, Y) and OTlore(N, X); ``` ```tel ``` ```-- Timed Since Inclusive: less than or equal to N ``` ```node SITlore(const N: int; X: bool; Y: bool; ) returns (Z: bool); ``` ```let ``` ``` Z = SI(X,Y) and OTlore(N, X); ``` ```tel ``` ```node abs(x:real) ``` ```returns(y:real); ``` ```let ``` ``` y = if x >= 0.0 then x else - x; ``` ```tel ``` ```(*@contract TriplexSignalMonitorSpec(Tlevel:real; ia:real; ib:real; ic:real; PCLimit: int; ) returns (FC: int; set_val: real; TC: int; PC: int); ``` ```--Block Path: triplex_12B ``` ```let ``` ``` var FTP:bool = true -> false; ``` ``` var C1:bool = abs(ia - ib) > Tlevel; ``` ``` var C2:bool = abs(ib - ic) > Tlevel; ``` ``` var C3:bool = abs(ia - ic) > Tlevel; ``` ``` var miscompare : bool = (not C1 and C2 and C3) or (C1 and not C2 and C3) or (C1 and C2 and not C3); ``` ``` var prePC: int = 0 -> pre PC; ``` ``` var pre_set_val : real = (0.0 -> pre set_val); ``` ``` var failure_in_progress : bool = miscompare and prePC <= PCLimit and PC > 0; ``` ``` var failure_must_be_latched : bool = miscompare and prePC > PCLimit; ``` ``` var no_fail : bool = (FC =0); ``` ``` var pre_no_fail : bool = (true -> pre no_fail); ``` ``` var single_fail_reported : bool = (FC=1) or (FC=2) or (FC=4); ``` ``` var mid_value : real = if ((ia <= ib and ib <= ic) ``` ``` or (ic <= ib and ib <= ia)) ``` ``` then ib ``` ``` else if ((ib <= ia and ia <= ic) ``` ``` or (ic <= ia and ia <= ib)) ``` ``` then ia ``` ``` else ic; ``` ``` -- Assumptions ``` ``` assume PCLimit > 0 ; ``` ``` -- In the no-fail state, a miscompare, which shall be characterized by one branch ``` ``` -- differing with the other two branches by a unique trip level that lasts for ``` ``` -- more than the persistence limit, shall be reported to failure management as ``` ``` -- a failure. ``` ``` 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)); ``` ``` -- In the no-fail state, the mid-value shall be the selected value. Note: a first failure in progress will not affect the method for determining the selected value. ``` ``` guarantee "TSM -002" S((( no_fail => set_val = mid_value) and FTP),(no_fail => set_val = mid_value)); ``` ``` -- In the single fail state, a good channel average of the remaining two good branches shall be used to determine the selected value. ``` ``` guarantee "TSM-003a" S( ((FC = 1 => set_val = 0.5 * ( ia + ib )) and FTP), (FC = 1 => set_val = 0.5 * ( ia + ib ))); ``` ``` guarantee "TSM-003b" S(((FC = 2 => set_val = 0.5 * ( ia + ic )) and FTP), (FC = 2 => set_val = 0.5 * ( ia + ic ))); ``` ``` guarantee "TSM-003c" S(((FC = 4 => set_val = 0.5 * ( ib + ic )) and FTP), (FC = 4 => set_val = 0.5 * ( ib + ic ))); ``` ``` -- If a second failure is in progress, the selected value shall remain unchanged from the previous selected value. ``` ``` guarantee "TSM-004" 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)); ``` ```tel ``` ```*) ```
(1-1/1)