ltl2fa is a tool that takes infix notation formula and translates it into spin neverclaim code or DVE LTL property using modified scheck tool. A modified version of xspin, that uses ltl2fa, is provided. Also, modified scheck tool that outputs Spin or DVE code, is provided. The DVE code can be used to run benchmarks on DiVinE.
The newest version is 0.1 (18.07.2008):
The source code is available under the terms of the GNU General Public License.
No installation required. Simply run the ltl2fa.py script. Also, the following tools must be installed or be available as a executable binary:
lbt - ltl2fa was tested with lbt-1.2.2, newer versions might not be compatible with ltl2fa.
scheck - the modified scheck-1.2.0 version is available here.
lbt and scheck are available under the terms of GNU General Public License.
xspin - the modified version of xspin-5.1.0 is available here. Please read the license first.
spin - Software was tested with spin version 5.1.6. See "External tools" to download the tool.
NB! Please read the licenses provided with each tool before using it. Xspin and Spin have a different license than the rest of the software!
If something doesn't work you might need to change the environment variables and/or command line commands in the software.
To use the modified xspin with ltl2fa run the xspin_ltl2fa.tcl script with ltl2fa.py in the same directory and use xspin as you normally would.
You can use ltl2fa as a standalone tool. Open command line, move to the directory, where the ltl2fa.py is, and run it with the input formula as an argument. Example:
python ltl2fa -v -d '[] wait0'
The '-v' switch will output all the steps of formula parsing.
The '-d' switch will output "#define" statements for every proposition.
NB! The output of ltl2fa depends on how the scheck tool is compiled. Look into Makefile in scheck's source code to change the output to either DVE or Spin (DDVE and DSPIN flags) before compiling it.
References to tools, without modifications to the source code.
scheck - translates safety LTL formulae to finite automata.
lbt - translates LTL formulae to Buchi automata.
spin - tool for the formal verification of distributed software systems.
DiVinE - distributed verification environment.