### Profile

 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 pre 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 ``` ```node max(x1, x2:real) ``` ```returns(y:real); ``` ```let ``` ``` y = if x1 >= x2 then x1 else x2; ``` ```tel ``` ```node min(x1, x2:real) ``` ```returns(y:real); ``` ```let ``` ``` y = if x1 >= x2 then x2 else x1; ``` ```tel ``` ```node ToInt (X: bool) returns (N: int) ; ``` ```let ``` ``` N = if X then 1 else 0 ; ``` ```tel ``` ```node Count (X: bool) returns (N: int) ; ``` ```let ``` ``` N = ToInt(X) -> ToInt(X) + pre N ; ``` ```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 absAB: real = abs(ia - ib); ``` ``` var absAC: real = abs(ia - ic); ``` ``` var absBC: real = abs(ib - ic); ``` ``` var avg: real = (ia + ib + ic) / 3.0; ``` ``` var mid_value:real = if (abs(ia - avg) > abs(ic - avg) and abs(ib - avg) > abs(ic - avg)) then ic ``` ``` else if (abs(ia - avg) > abs(ib - avg)) then ib ``` ``` else ia; ``` ```var preFC: int = 0 -> pre FC; ``` ```var prePC: int = 0 -> pre PC; ``` ```var prePCLimit: int = 0 -> pre PCLimit; ``` ```var prevSet_val: real = 0.0 -> pre set_val; ``` ```-- calculate is_a_miscompare ``` ```var C1:bool = absAB > Tlevel; ``` ```var C2:bool = absBC > Tlevel; ``` ```var C3:bool = absAC > Tlevel; ``` ```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); ``` ```-- Assumptions ``` ```assume PCLimit > 0 ; ``` ```assume true -> PCLimit = prePCLimit; ``` ```assume true -> Tlevel = pre Tlevel; ``` ```-- when preFC = 0 & prePC > prePCLimit TriplexSignalMonitor shall immediately satisfy FC > 0 ``` ```--guarantee "RM001" S( (((preFC = 0 and prePC > prePCLimit) => (FC > 0)) and FTP), ((preFC = 0 and prePC > prePCLimit) => (FC > 0)) ); ``` ```--guarantee "RM001V2" is_a_miscompare and prePC > PCLimit => FC > 0; ``` ```-- when FC =1 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ib) ``` ```--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 )) )); ``` ```--guarantee "RM003aV2" FC = 1 => set_val = 0.5 * (ia +ib); ``` ```-- when FC =2 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ic). ``` ```--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 )) )); ``` ```--guarantee "RM003bV2" FC = 2 => set_val = 0.5 * (ia +ic); ``` ```-- when FC =4 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ib +ic) ``` ```--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 )) )); ``` ```--guarantee "RM003cV2" FC = 4 => set_val = 0.5 * (ib +ic); ``` ```-- when preFC =0 TriplexSignalMonitor shall immediately satisfy set_val = mid_value ``` ```--guarantee "RM002" S( (((preFC = 0) => (set_val = mid_value)) and FTP), ((preFC = 0) => (set_val = mid_value)) ); ``` ```--guarantee "RM002V2" FC = 0 => set_val = mid_value; ``` ```-- when (absAB > Tlevel & absAC >Tlevel) | (absAB > Tlevel & absBC > Tlevel) | (absAC > Tlevel & absBC > Tlevel) TriplexSignalMonitor shall always satisfy set_val = prevSet_val ``` ```--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) )); ``` ```--Explanaton from document: ``` ```-- -A miscompare that persists but has not yet been declared failed is known as a failure in progress. ``` ```-- can be expressed as "is_a_miscompare and prePC > 0 and prePC < PCLimit" ``` ```-- -A second failure can be expressed as "Count(FC > 0) = 1" ``` ```--[RM-004] If a second failure is in progress, the selected value shall remain unchanged from the previous selected value. ``` ```guarantee "RM004V2" Count(FC > 0) = 1 and is_a_miscompare and prePC > 0 and prePC < PCLimit => set_val = prevSet_val; ``` ```--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; ``` ```tel ```