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"