The Non-Determinism Analysis View
Introduction
AF3 provides a deep integration of the Z3 SMT-solver
in order to quickly check for potential non-determinism.
Installing Z3
To use the non-determinism checking functionality in AF3, firstly we have to install the
Z3 SMT solver. You only have to make sure that Z3 is in the PATH. To check whether
AF3 can access Z3, just press the "Z3 Version" button from the
"Non-determinism Analyses View". If Z3 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.
- 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.