Project

General

Profile

Revision 6ccfcb12 tests/cocospec/TriplexSignalMonitorSpec.lus

View differences:

tests/cocospec/TriplexSignalMonitorSpec.lus
116 116
assume true -> Tlevel = pre Tlevel;
117 117

  
118 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;
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 121

  
122 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);
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 125

  
126 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);
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 129

  
130 130

  
131 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);
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 134

  
135 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;
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 138

  
139 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) ));
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 141

  
142 142
--Explanaton from document: 
143 143
--    -A miscompare that persists but has not yet been declared failed is known as a failure in progress.
......
146 146
--[RM-004] If a second failure is in progress, the selected value shall remain unchanged from the previous selected value.
147 147
guarantee "RM004V2"  Count(FC > 0) = 1   and is_a_miscompare and prePC > 0 and prePC < PCLimit => set_val = prevSet_val;
148 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;
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 150
tel
151 151
*)

Also available in: Unified diff