EFSM-tools is a toolset for finite-state machine (FSM) synthesis. Is is mostly based on satisfiability solvers, and uses traces (aka IO-traces, scenarios) and LTL formulae as input. EFSM means "extended finite-state machine", an FSM with variables. However, within this toolset variables are Boolean and are often treated analogously to input events. The variant of the FSM synthesis problem being solved is exact: an FSM is generated with the given number of states, or its non-existence is reported.
The toolset implements the techniques described in the following papers:
- Ulyantsev V., Tsarev F. Extended Finite-State Machine Induction using SAT-Solver / Proceedings of the Tenth International Conference on Machine Learning and Applications. - Honolulu: IEEE Computer Society, 2011. - Vol. 2. - P. 346-349
- Ulyantsev V., Buzhinsky I., Shalyto A. Exact Finite-State Machine Identification from Scenarios and Temporal Properties. International Journal on Software Tools for Technology Transfer, 2016, DOI: 10.1007/s10009-016-0442-1
- Buzhinsky I., Vyatkin V. Automatic Inference of Finite-State Plant Models from Traces and Temporal Properties. IEEE Transactions on Industrial Informatics, 2017, DOI: 10.1109/TII.2017.2670146
EFSM-tools is developed in Computer Technologies Laboratory, ITMO University. You may find related projects by the same research group below:
- Toolset for deterministic finite automata (DFA) synthesis
- MuACO toolset for EFSM synthesis based on ant colony optimization
To build the toolset, you need JDK 1.8 (or greater) and ant. The tool is intended to work on Linux and Windows. The most recent features are not tested on Windows, though. Running some examples may require bash.
EFSM-tools works with cryptominisat and lingeling SAT solvers, Choco constraint (CSP) solver and DepQBF QSAT (QBF) solver. Choco is included into the toolset as a library. As for the rest, they must be installed separately. Make them available in command line as "cryptominisat4", "lingeling" and "depqbf".
Some of the tools which work with solvers require limboole. Make it available in command line as "limboole".
Different features of the toolset require different solvers, so probably there is no need to install all of them. More information is provided in other sections.
To view generated FSMs, you need Graphviz (on Linux, you may additionally install the XDot viewer).
To build the toolset, move to the root of the project and run:
ant
The JAR executables will be generated in the jars directory. Then you can try running JAR tools like this and see the summaries of their command line options:
java -jar jars/<tool-name>.jar
In addition, recent synthesis methods by default use the incremental version of cryptominisat4. The pre-built Linux binary is located in the incremental-cryptominisat directory. Make the binary file incremental-cryptominisat-binary available in command line, e.g.:
sudo ln -s incremental-cryptominisat-binary /usr/bin
To run incremental-cryptominisat-binary, you at least need to have cryptominisat4 installed. To rebuild it yourself, you need make, g++ and cryptominisat4. Run:
make
If for some reason you are unable to use the incremental version of cryptominisat, the usual versions of cryptominisat and lingeling can be used instead (some jar tools have command line options to set the used solver).
Behavior traces, or scenarios, are represented as text files. Each scenario is a pair of two consecutive lines: the first line represents inputs and the second one represents outputs. Trace elements are separated with semicolons. Trace files may have empty lines, which are ignored.
Inputs have the formal event[<Boolean formula over input variables>]. The boolean formula can be just "1" if there are no input variables. Nontrivial Boolean formulae can use Boolean operators "&" (and), "|" (or), "~" (not). Here are some examples of input declarations:
- A[1]
- e1[x0 & ~x1]
While each input is a combination of an event and, optionally, of variable values, each output is a combination of comma-separated actions, for example:
- z0, z1, z4
- close, logout
To see complete examples of trace files, you may examine the files examples/elevator.sc and examples/clock.sc.
More notes:
- For Mealy machine synthesis, the order of actions is important (i.e. outputs are compared as action strings), while for Moore machines it is not (i.e. outputs are compared as action sets).
- For Moore machine synthesis, the first input is always dummy (represented by the empty string). Thus, each input line starts with a semicolon.
LTL properties, or LTL formulae, are represented as text files. Each line represents a single LTL formula. Formulae may use temporal operators X (next), F (future), G (globally), U (until), R (release), Boolean operators "&&" (and), "||" (or), "!" (not), and atomic propositions event(<event name or a comma-separated list of event names>), action(<action name>), variable(<variable name>).
To see complete examples of LTL property files, you may examine the files examples/elevator.ltl and examples/clock.ltl.
More notes:
- Empty lines are not permitted.
- There is a deprecated format which requires to write atomic propositions as wasAction(co.<action name>) and wasEvent(ep.<event name>). Avoid this format.
This method is described here as the "Iterative SAT-based" one:
It uses incremental cryptominisat by default, but switching to usual versions of cryptominisat or lingeling are possible using command line options. To run the tool:
java -jar jars/fast-automaton-generator.jar
Here are scripts to run several examples from the paper mentioned above:
cd examples
ln -s ../c-lib .
./clock-fast.sh # Alarm clock
./elevator-fast.sh # Elevator
./cash-dispenser-fast.sh # ATM
./editor-fast.sh # Text editor
./jhotdraw-fast.sh # JHotDraw
./cvs-fast.sh # CVS client
Additional (but generally slower) methods are also available for the same problem. They are described here:
Run the following tool:
java -jar jars/qbf-automaton-generator.jar
It supports four methods of FSM synthesis based on:
- running a QSAT (QBF) solver (this method is quite slow)
- translating the QSAT instance to a SAT one and running a SAT solver (this method may require much memory)
- backtracking (no solver is used)
- iterative SAT-solving using a non-incremental solver (not described in the paper)
The concrete method can be selected using the "--strategy" command line option. FSM completeness requirement can be switched on by adding "--completenessType NORMAL". The only supported QBF solver is DepQBF.
Here are scripts to run several examples from the paper mentioned above:
cd examples
ln -s ../c-lib .
./clock.sh # Alarm clock
./elevator.sh # Elevator
./cash-dispenser.sh # ATM
./editor.sh # Text editor
./jhotdraw.sh # JHotDraw
./cvs.sh # CVS client
This is a spin-off of the FSM synthesis project which focuses on Moore machine synthesis for a specific application. In the industrial automation domain, controllers co-exist with plants. In formal modeling, it is natural to represent plants as nondeterministic Moore machines. Read more in:
Run the tool:
java -jar jars/plant-automaton-generator.jar
Here are scripts to run some examples (the first one is from the paper):
cd evaluation/plant-synthesis
ln -s ../../c-lib .
./cylinder.sh
./water-level.sh
1. Simplified version of the previous method. If the input data does not have any LTL formulae, run plant-automaton-generator.jar with the option "--fast". This will switch the solver-based algorithm to a much simpler and faster graph algorithm. The proper number of states will be determined automatically.
2. Explicit-state method. Enhanced explicit-state plant model construction with completion of trace-unsupported transitions based on input proximity:
java -jar jars/apros-builder.jar --type explicit-state --config --dataset
Configuration files describe inputs and outputs of the plant model. A dataset file must be precompiled from traces represented in the format of the Apros continuous process simulator. Examples of configuration, a script to generate traces and a script to precompile a dataset can be found in evaluation/counter.
This method is described in:
3. Constraint-based (symbolic) method. Synthesizes purely symbolic models which are easier for the verifier NuSMV to process. Run:
java -jar jars/apros-builder.jar --type constraint-based --config --dataset --constraintBasedDisableOIO_CONSTRAINTS --constraintBasedDisableFAIRNESS_CONSTRAINTS
This method is described in:
4. Modular method. Modular explicit-state plant model construction. An example is given in evaluation/counter/modular.sh.
This method is described in:
The tool jars/plant-automaton-generator.jar can also be used to generate usual deterministic Moore machines. Add "--deterministic" (and, optionally, "--bfsConstraints") to command line options. Note that in this case all traces have to start with the same tuple of outputs.
Here are scripts to run some examples:
cd evaluation/moore-machine-synthesis
ln -s ../../c-lib .
./cylinder.sh
./water-level.sh
This set of tools is partially described in the paper:
FSM identification using the Choco CSP solver:
java -jar jars/builder.jar
FSM identification using the cryptominisat SAT solver (must be available under the name "cryptominisat4"):
java -jar jars/sat-builder.jar
Auxiliary tools (for experiments, etc.):
- automaton-generator.jar: generate a random EFSM with the given parameters
- scenarios-generator.jar: generate scenarios for the given EFSM
- isomorphism-checker.jar: check two EFSMs for isomorphism
- completeness-checker.jar: check an EFSM for completeness (completeness here means rather coverage of transitions by traces)
- consistency-checker.jar: check EFSM compliance with a set of scenarios
Regarding research collaboration, email Vladimir Ulyantsev (ulyantsev@rain.ifmo.ru) and Igor Buzhinsky (igor.buzhinsky@gmail.com).
Regarding issues with the tool, bugs, etc., email Igor Buzhinsky.