Minimization and Instantiation of Labelled Transition Systems

Minimization and Instantiation of Labelled Transition Systems
Related Papers
Selected Documentation
Supported Systems
Downloads
Installation Instructions
Build Dependencies
Building from a Git Repository
Licence
Contact

LTSmin is a toolset for manipulating labelled transition systems. LTSmin already connects a sizeable number of existing (verification) tools: muCRL, mcrl2, DiVinE, SPIN, NIPS, CADP. Moreover, it allows to reuse existing tools with new state space generation techniques.

Implementing support for a new language module is in the order of 200–600 lines of C "glue" code, and automatically yields tools for standard reachability checking (e.g., for state space generation and verification of safety properties), reachability with symbolic state storage (vector set), fully symbolic (BDD-based) reachability, distributed reachability (MPI-based), and multi-core reachability (including multi-core compression and incremental hashing).

The synergy effects in the LTSmin implementation are enabled by a clean interface: all LTSmin modules work with a unifying state representation of integer vectors of fixed size, and the PINS dependency matrix which exploits the combinatorial nature of model checking problems. This splits model checking tools into three mostly independent parts: language modules, PINS optimizations, and model checking algorithms.

On the other hand, the implementation of a verification algorithm based on the PINS matrix automatically has access to muCRL, mcrl2, DVE, PROMELA and ETF language modules.

Finally, all tools benefit from PINS2PINS optimizations, like local transition caching (which speeds up slow state space generators), matrix regrouping (which can drastically reduce run-time and memory consumption of symbolic algorithms).

Download shortcut: http://fmt.cs.utwente.nl/tools/ltsmin/ltsmin.tar.gz

Related Papers

Selected Documentation

  • lps-reach (BDD-based reachability with mcrl2 frontend)
  • dve22lts-mc (multi-core reachability with DiVinE 2 frontend)
  • lpo2lts-grey (enumerative reachability with muCRL frontend)
  • etf2lts-mpi (distributed reachability with ETF frontend)
  • lps2torx (TorX testing tool connector with mcrl2 frontend)

Supported Systems

Downloads

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 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 mostlyclean is 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/>.

Flex

Download Flex (>= 2.5.35) from <http://flex.sourceforge.net/>.

Apache Ant

Download Apache Ant from <http://ant.apache.org/>. We tested with ant-1.8.2. Note that ant is not required for building from a distribution tarball (unless Java files were modified). Note that we require JavaCC task support for Ant.

Optional Dependencies

muCRL

Download muCRL (>= 2.18.5) from <http://www.cwi.nl/~mcrl/mutool.html>. We tested with muCRL-2.18.5. Without muCRL, the symbolic tools (spec-reach) for state space generation (e.g., lps-reach) will have degraded performance due to the absence of the AtermDD decision diagram package

Note that for 64-bit builds, you have to explicitly configure muCRL for this (otherwise, a faulty version is silently build): 

    ./configure --with-64bit

For best performance, we advise to configure muCRL like this: 

    ./configure CC='gcc -O2' --with-64bit

mCRL2

Download the latest version of mCRL2 from <http://www.mcrl2.org/>. We tested with mcrl2 SVN rev.9377. Note that all versions before SVN rev.9377 are insufficient (in particular, all versions of mcrl2 released before July 2011).

Build and install mCRL2:

cmake . -DCMAKE_INSTALL_PREFIX=...
make
make install

The graphical tools of mCRL2 are not required for ltsmin to work, hence you can also build mCRL2 without: 

  cmake . -DMCRL2_ENABLE_GUI_TOOLS=OFF -DCMAKE_INSTALL_PREFIX=...

CADP

See the CADP website on how to obtain a license and download the CADP toolkit.

DiVinE 2

Download a patched version of DiVinE 2.4: 

git clone http://fmt.cs.utwente.nl/tools/scm/divine2.git

Build with:

cd divine2
mkdir _build && cd _build
cmake .. -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=...
make
make install

(On MacOS X, option -DHOARD=OFF might have to be added to the cmake command line to make it compile without errors.
(To solve errors about missing Murphi headers, use: -DMURPHI=OFF.)

The LTSmin configure script will find the DiVinE installation automatically, if the divine binary is in the search path. With suitable options, the divine compile DVE compiler produces LTSmin compatible libraries: 

divine compile -l model.dve

This produces a file ``model.dve2C'', which can also be passed to LTSmin tools. (This step is done automatically by the LTSmin tools when passing a ``.dve'' model, doing it manually is rarely needed.)

DivinE(-cluster)

Download the latest CVS version of DiVinE-cluster; instructions can be found at <http://divine.fi.muni.cz/trac/wiki/DevelopmentIntroduction>. We tested with the version from 2009-12-01.

Alternatively, download divine-cluster 0.8.3 from <http://divine.fi.muni.cz/page.php?page=download> and apply the patch from <contrib/divine-cluster-0.8.3-ltsmin.patch> to the divine-cluster source tree:

cd divine-0.8.3
patch -p1 < divine-cluster-0.8.3-ltsmin.patch

Then, build and install divine-cluster according to their documentation.

libDDD

Download libDDD (>= 1.7) from <http://move.lip6.fr/software/DDD/>. We tested with libDDD 1.7.

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.4.4) from <http://www.methods.co.nz/asciidoc/>. We tested with asciidoc-8.4.4. 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. Note that xmlto in turn requires docbook-xsl to be installed. We tested with docbook-xsl-1.76.1.

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.68.

GNU libtool

Download libtool (>= 2.2.6) from <http://www.gnu.org/software/libtool/>. We tested with libtool-2.4.

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.

Apache Ant

See above.

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.