next up previous contents
Next: Example - traffic light Up: Basic concepts Previous: Resolution   Contents

Embedded assertions

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