Verification View

The Verification View provides 3 different methods to test a machine:

  • Modelchecking
  • LTL Verifications and
  • Constraint Based Checking

In each tab you can add multiple tests to check you currently selected machine.

Modelchecking

Modelchecking.png

By pressing the plus button you can add several model checking variants. The following view will be shown:

Modelchecking Stage.png

Select one of the search strategies (breadth first, depth first or a mix of both) and the checkboxes containing different possible errors like deadlocks to be checked for. By pushing the Model Check button your selected variant will be added to the list shown at the top of the Modelchecking Tab.

LTL Verifications

LTL.png

Constraint Based Checking

CBC.png