Example - traffic light
An assertion of the form
assert label: cond;
whenever it executes (in zero time). If
is ever false, the property named
is reported to be false. These assertions can be verified formally by SMV.