property = BandDuration(check=..., window=..., lowerLimit=..., upperLimit=...).y;
In any (sliding) time window of length window, the longest time duration where the Boolean input check was permanently true (= maxDuration) must be ≥ parameter lowerLimit and ≤ parameter upperLimit. Whenever this property is fulfilled, Property output y = Satisfied. If this property is not fulfilled at the end of a sliding time window, y = Violated (exception: before the end of the first time window, y = Undecided provided maxDuration ≤ lowerLimit):
y = if maxDuration ≥ lowerLimit and maxDuration ≤ upperLimit then Satisfied else (if first and maxDuration ≤ upperLimit then Undecided else Violated);
Violated, Undecided, and Satisfied are elements of enumeration Property.
The property is demonstrated with the following example calling the block as:
results in
simulation result |