Minimization and Instantiation of Labelled Transition Systems
LTSmin is a toolset for manipulating labelled transition systems. The main tool in this release is ltsmin-mpi, which is a distributed implementation of signature-based bisimulation reduction for strong bisimulation and branching bisimulation. The input for this tool is a labelled transition system (LTS) in DIR format.
Various sequential, symbolic and distributed tools are provided for
the creation of LTSs, for example from muCRL, mCRL2 and PROMELA (via
NIPS) specifications. Alternatively, LTSs in DIR format can be
created by third-party tools, for example instantiators and dmp2dir
from the muCRL toolset.
The tools in this release support compression of DIR files as well as
putting a DIR in an archive file. The ltsmin-convert utility can
convert files from one DIR variant to another, and to the BCG file
format from the CADP toolset.
Download shortcut: http://fmt.cs.utwente.nl/tools/ltsmin/ltsmin.tar.gz
Related Papers
- Stefan Blom, Jaco van de Pol and Michael Weber. Bridging the Gap between Enumerative and Symbolic Model Checkers, Technical Report TR-CTIT-09-30, CTIT, University of Twente, Enschede. (2009)
- Stefan Blom, Bert Lisser, Jaco van de Pol, and Michael Weber. A Database Approach to Distributed State Space Generation. J Logic Computation (2009)
- Stefan Blom, Jaco van de Pol: Symbolic Reachability for Process Algebras with Recursive Data Types. ICTAC 2008: pp. 81-95
- Stefan Blom, Bert Lisser, Jaco van de Pol, and Michael Weber. A Database Approach to Distributed State Space Generation. ENTCS 198(1): pp. 17-32 (2007)
- Stefan Blom, Simona Orzan: Distributed state space minimization. STTT 7(3): pp. 280-291 (2005)
- Stefan Blom, Simona Orzan: A distributed algorithm for strong bisimulation reduction of state spaces. STTT 7(1): pp. 74-86 (2005)
- Stefan Blom, Izak van Langevelde, Bert Lisser: Compressed and Distributed File Formats for Labeled Transition Systems. ENTCS 89(1): (2003)
- Stefan Blom, Simona Orzan: Distributed Branching Bisimulation Reduction of State Spaces. ENTCS 89(1): (2003)
- Stefan Blom, Simona Orzan: Distributed State Space Minimization. ENTCS 80: (2003)
- Stefan Blom, Simona Orzan: A Distributed Algorithm for Strong Bisimulation Reduction of State Spaces. ENTCS 68(4): (2002)
Supported Systems
- GNU/Linux (tested on Debian, Fedora 9, OpenSuSE 10.2 and 10.3)
- MacOS X, version 10.6 "Snow Leopard"
- MacOS X, version 10.5 "Leopard"
- MacOS X, version 10.4 "Tiger"
Downloads
- Released Versions
- Snapshots
- ltsmin-master.tgz (current snapshot of the master release branch)
- ltsmin-maint.tgz (current snapshot of the maint maintenance branch)
- ltsmin-next.tgz (current snapshot of the next release branch)
- ltsmin.git (browsable Git repository)
git clone http://fmt.cs.utwente.nl/tools/scm/ltsmin.git
cd ltsmin && git submodule update --init
(read-only Git repository)
Installation Instructions
If you are building the software from a Git repository rather than a release tarball, refer to Section "Building from a Git Repository" for additional set-up instructions. Then install the dependencies listed in Section "Build Dependencies" below.
# Unpack the tarball $ tar xvzf ltsmin-<version>.tar.gz $ cd ltsmin-<version> # Configure $ ./configure --disable-dependency-tracking --prefix /path/
It is a good idea to check the output of ./configure, to see whether
all dependencies were found.
# Build $ make # Install $ make install
Additional Build Options
configure Options
For one-shot builds, the following option speeds up the build process by not recording dependencies:
./configure --disable-dependency-tracking ...
Non-standard compilers, etc., can be configured by using variables:
./configure CFLAGS='-O3' CXXFLAGS='-O3' \ CC='gcc -m64' \ MPICC='/sw/openmpi/1.2.8/bin/mpicc -m64' \ MPICXX='/sw/openmpi/1.2.8/bin/mpicxx -m64' \ ...
This would add some options to the standard CFLAGS and CXXFLAGS
settings used for building to enable more optimizations and force a
64-bit build (for the GCC C compiler). Furthermore, the MPI compiler
wrappers are set explicitly instead of searching them in the current
shell PATH.
Note that for libraries installed in non-standard places need special attention: to be picked up by the configure script, library and header search paths must be added, e.g.:
./configure LDFLAGS=-L/opt/local/lib CPPFLAGS=-I/opt/local/include
Additional setting of (DY)LD_LIBRARY_PATH might be needed for the
dynamic linker/loader (see, e.g., "man ld.so" or "man dyld").
See ./configure --help for the list of available variables,
and file INSTALL for further details.
make Targets
The following additional make targets are supported:
- all
- Builds everything.
- install
-
Installs the software into path
$prefix(default:/usr/local/). - mostlyclean
- clean
- distclean
-
Clean the source tree to various degrees. Using
mostlycleanis enough in many cases. - doxygen-doc
- Builds Doxygen documentation for the source code.
Build Dependencies
We list the external libraries and tools which are required to build this software.
popt
Download popt (>= 1.7) from <http://rpm5.org/files/popt/>. We tested with popt 1.14.
zlib
Download zlib from <http://www.zlib.net/>.
GNU make
Download GNU make from <http://www.gnu.org/software/make/>.
Optional Dependencies
muCRL
Download muCRL from <http://www.cwi.nl/~mcrl/mutool.html>. We tested with muCRL-2.18.4. Without muCRL, the distributed tool for state space generation (lpo2lts-mpi) will not be built, and neither will all NIPS-based tools.
mCRL2
Download the latest released version of mCRL2 from <http://www.mcrl2.org/>. We tested with mcrl2-200901. Build and install mCRL2 as usual:
./configure <options> make make install
Unless mcrl2 is configured to use an external Boost library instead of its own copy, the headers have to be installed as well:
./build/bin/bjam --install --install-boost-headers
Ensure that these headers are actually used to compile the PINS support for mcrl2 (instead of, e.g., system-provided Boost headers).
CADP
See the CADP website on how to obtain a licence and download the CADP toolkit.
MPI
In principle, any MPI library which supports MPI-IO should work. However, we tested only with Open MPI <http://www.open-mpi.org/>. Without MPI, the distributed tools (xxx2lts-mpi, ltsmin-mpi) will not be built.
AsciiDoc
Download AsciiDoc (>= 8) from <http://www.methods.co.nz/asciidoc/>. We tested with asciidoc-8.2.7. Without asciidoc, documentation cannot be rebuilt. For convenience, release tarballs are shipping with pre-built man pages and HTML documentation.
xmlto
Download xmlto from <http://cyberelk.net/tim/software/xmlto/>. We tested with xmlto-0.0.18. Without xmlto, man pages cannot be rebuilt.
Doxygen
Download Doxygen from <http://www.doxygen.org/>. We tested with doxygen-1.5.5. Without doxygen, internal source code documentation cannot be generated.
MacOS X
For cross-compilation builds on MacOS X, the Apple Developer SDKs must be installed. They are available from Apple <http://developer.apple.com/tools/download/>, or from the MacOS X installation CDs.
Building from a Git Repository
Before building the software as described above, the following commands have to be executed in the top-level source directory:
# Rebuid autotools support $ git submodule update --init $ ./ltsminreconf
Dependencies
Building from another source than a release tarball requires some extra tools to be installed:
GNU automake
Download automake (>= 1.10) from <http://www.gnu.org/software/automake/>. We tested with automake-1.10.
GNU autoconf
Download autoconf (>= 2.60) from <http://www.gnu.org/software/autoconf/>. We tested with autoconf-2.61.
GNU libtool
Download libtool (>= 1.5.26) from <http://www.gnu.org/software/libtool/>. We tested with libtool-1.5.26.
AsciiDoc
See above. Note that AsciiDoc is a required dependency unless building from source tarballs.
xmlto
See above. Note that xmlto is a required dependency unless building from source tarballs.
Licence
Copyright (c) 2008, Formal Methods and Tools, University of Twente
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the University of Twente nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Contact
Send questions, bug reports, comments and feature suggestions to ltsmin-support@cs.utwente.nl.
