The Non-Determinism Analysis View of AutoFOCUS3 (AF3)

The Non-Determinism Analysis View

Introduction

AF3 provides a deep integration of the Yices SMT solver in order to quickly check for potential non-determinism.

Installing YICES

To use the non-determinism checking functionality in AF3, firstly we have to install the Yices SMT solver. You only have to make sure that Yices is in the PATH. To check whether AF3 can access Yices, just press the "Yices Version" button from the "Non-determinism Analyses View". If Yices is correctly installed, a dialog showing its version is displayed (as below), otherwise an error message will be displayed.

Using the "Nondeterminism Analyzer"

Step 1 - Open the "Non-determinism Analyzes" view by clicking on the button from the toolbar. Non-determinism Analyzes Icon

Step 2 - Open a state-automaton in the graphical editor and press the "Check non-determinism" button.

Step 3 - In case when potential non-deterministic transitions are found, they will be displayed in the table on the left side. On the right-side an evidence about the non-determinism will be shown.