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 (arxiv preprint)
- Buzhinsky I., Vyatkin V. Plant Model Inference for Closed-Loop Verification of Control Systems: Initial Explorations. IEEE International Conference on Industrial Informatics (INDIN 2016), Poitiers, France, July 18–21, 2016 (to appear)
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
The toolset is based on Java, so you must have JRE 1.8 (or greater) to run it. You may wish to rebuild the toolset, for which 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).
The pre-build JAR executables are placed in the jars directory. If you wish to rebuild the toolset yourself, move to the root of the project and run:
ant
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>), 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 tool is described here: http://arxiv.org/abs/1601.06945. It supports four methods of FSM synthesis based on:
- iterative running of a SAT solver (also check the next section for a faster implementation of this method!)
- 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)
To run the tool:
java -jar jars/qbf-automaton-generator.jar
The desired 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 an enhanced version of the so-called "iterative" method described here: http://arxiv.org/abs/1601.06945. 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
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:
- Buzhinsky I., Vyatkin V. Plant Model Inference for Closed-Loop Verification of Control Systems: Initial Explorations. IEEE International Conference on Industrial Informatics (INDIN 2016), Poitiers, France, July 18–21, 2016 (to appear)
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
If the input data doesn't 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.
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@corp.ifmo.ru).
Regarding issues with the tool, bugs, etc., email Igor Buzhinsky.