1. Overview and Related Reading

The main functionality of this software is to infer state machines from sequences.

The principal purpose is to implement our EFSM inference algorithm, discussed here:

  • Neil Walkinshaw, and Ramsay Taylor, and John Derrick, "Inferring Extended Finite State Machine models from software executions", Journal of Empirical Software Engineering -
  • Neil Walkinshaw and Ramsay Taylor and John Derrick, "Inferring Extended Finite State Machine models from software executions", WCRE, pp. 301-310, IEEE, 2013.

The tool also contains code to automate testing from inferred models, albeit these models are currently restricted to simple WEKA decision trees. This work is described in the following paper:

  • Petros Papadopoulos and Neil Walkinshaw, "Black-Box Test Generation from Inferred Models", RAISE 2015

However, it also includes implementations of the following algorithms, all of which can be activated from the command line:

  • K-Folds - Biermann and Feldman, "On the synthesis of finite-state machines from samples of their behaviour", IEEE Trans Computers, Vol. 21, pp. 591-597, 1972.
  • EDSM (with and without Blue-Fringe windowing) - Lang, Pearlmutter and Price, Results of the Abbadingo One DFA Learning Competition and a New Evidence-Driven State Merging Algorithm, 4th International Colloquium on Grammar Inference, LNCS, Vol. 1433, pp. 1-12, Springer, 1998.
  • Gk-Tails - Lorenzoli, Mariani and Pezzè, Automatic generation of software behavioral models, ICSE, pp. 501-510, ACM, 2008.

Further detailed instructions can be found on the wiki.

2. Copyright and License

Copyright (C) 2012,2013,2014 Neil Walkinshaw and Contributors

This file is part of EFSMTool.

EFSMTool is free software: you can redistribute it and/or modify it under the terms of the GNU Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

EFSMTool is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Public License for more details.

You should have received a copy of the GNU Public License along with EFSMTool. If not, see

The licences pertaining to the other dependencies are included in the licences file.

3. Installation

3.a. Installing dependencies (essential for running executable JAR as well as running compiled source code):

If you intend to download the executable jar file, most of the dependencies are packed into the jar with the suffix "jar-with-dependencies" (thanks to Maven). However, there is one further dependency that could not be packaged, because it is platform specific.

For certain aspects of its functionality (notably automated test generation), the tool relies upon Microsoft's Z3 constraint solver with its Java extensions. These are freely available. Please follow the the instructions here to install it for your system:

Important note - Since Z3 has moved from CodePlex to Github, you need to replace the git command in these instructions as follows:

git clone -b unstable

Having followed the rest of the instructions, you ought to have a dynamic linked library (.so in *nix, .dll in Windows, .dylib in MacOS). You need to add this to the Java runtime path for native libraries.

Now you should be able to run the executable jar file.

3.b. Downloading and compiling source code.

If you are interested in compiling the source code, perhaps with a view to contributing yourself, then you will require Mercurial and Maven to be installed on your system.

Once these are installed, first of all, use Mercurial to clone (download) the latest version of the source code to your system. At the command prompt, go to a suitable directory and type:

hg clone

This will download the source code. Now go into the efsmtool directory and compile the sources by typing:

mvn install

If you wish to set it up as an Eclipse project that can be imported directly, type:

mvn eclipse:eclipse

3.c. Adding Z3 dynamic library to the native libraries path in Eclipse.

If you are intending to run the compiled code from within Eclipse, you will need to add the Z3 dynamic library (see 2.a) to the native library path.

Right-click on EFSMTool, select "build path" and select "Configure Build Path". Click on the "Libraries" tab and select the arrow next to the JRE System Library. Select "Native Library Location", and then click the "Edit" button. There, enter the directory containing the Z3 dynamic library file.

If you are running this in Linux, your LD_LIBRARY path will have been adjusted to accommodate Z3. If you are running EFSMTool out of Eclipse, this has to be included in the runtime configurations as well.

4. Running

To infer an EFSM, you run the app.Mint class. For detailed instructions on the parameters, see the Wiki.