property = WhenFalling(condition=..., check=...).y;
At the time instants where condition has a falling edge, property is set to "BooleanToProperty(check)" (so either Satisfied or Violated) and keeps this value until the next falling edge. Before the first falling edge, property = Undecided. If condition = false during initialization, property = toProperty(check) at initialization.
Violated, Undecided, and Satisfied are elements of enumeration Property.
The property is demonstrated with the following example:
results in
simulation result |