News

January 30, 2015

LTSmin 2.1 has been released.

You can now subscribe our mailing list: ltsmin-users@lists.utwente.nl to stay up-to-date!

What is LTSmin

LTSmin, originally Minimization and Instantiation of Labelled Transition Systems, has become a language-independent model checker that offers a wide spectrum of parallel and symbolic algorithms to deal with the state space explosion of different verification problems.

Algorithmic Backends

LTSmin offers different analysis algorithms covering four disciplines (algorithmic backends):

The PINS interface divides our model checking tools cleanly into the two These algorithms each have their own strength, depending on the input model's structure and verification problem. For models with combinatorial state structure, the symbolic tools can process billions of states per second using only few memory. Models that exhibit much concurrency can be reduced significantly using partial-order reduction. Models with more dependencies can be explored with LTSmin's multi-core algorithms, which employ aggressive lossless state compression using a concurrent tree data structure. Finally, our distributed minimization techniques can aid the verification of multiple properties on a single state space.

Language Frontends

LTSmin supports language independence via its definition of a Partitioned Next-State Interface (PINS), which exposes enough internal structure of the input model to enable the highly effective algorithms above, while at the same time making it easy to connect your own language module. The interface is also simple enough to support very fast next-state functions such as SPIN's (performance comparison here). LTSmin already connects a sizeable number of existing verification tools as language modules, enabling the use of their modeling formalisms:

Moreover, LTSmin supports multiple export formats for state spaces, which allows interoperability with other tools like CADP.

PINS Interface

The Partitioned Next-State Interface (PINS) splits up the next-state function in different groups. For example, each transition group can represent a line of code in an imperative language module or a summand in a process-algebraic language module. Using the static dependency information between transition groups and state vector variables (most groups only depend on a few variables), LTSmin's algorithms can exploit the combinatorial structure of the state space. This leads to exponential gains in performance for the symbolic algorithms, which can now learn the transition relation on-the-fly in a very effectively way, because it is partitioned. Using the same principle, LTSmin provides transition storing for transition caching with negligible memory overhead.

To connect a new language module, one merely needs to implement the PINS next-state functions and provide some type information on the state vector contents, which should be encoded according to PINS unifying integer vector format. By providing additional transition/state dependency information via the PINS dependency matrices, the symbolic exploration algorithms and PINS2PINS modules (see below) can exploit their full potential. Finally, by providing few additional information on transition guards the partial order reduction algorithms become enabled.

PINS2PINS Modules

The PINS interface divides our model checking tools cleanly into the two independent parts discussed above: language modules and model checking algorithms. However it also enables us to create PINS2PINS modules, that reside between the language module and the algorithm, and modify or optimize the next-state function. These PINS2PINS modules can benefit all algorithmic backends and can be turned on and off on demand:

  • transition storing/caching speeds up slow language modules,
  • regrouping speeds up the symbolic algorithms by optimizing dependencies, and
  • partial order reduction reduces the state space by dropping irrelevant transitions.
Furthermore, we implement linear temporal logic (LTL) as a PINS2PINS module, which is automatically turned on when an LTL formula is supplied and transforms the state space on-the-fly by calculating the cross product with the formula.

Download shortcut: https://github.com/utwente-fmt/ltsmin/releases/download/2.1/ltsmin-2.1.tar.gz

References

If you were to refer to the LTSmin toolset in your academic paper, we would appreciate if you would use one of the following references (depending on the part(s) of the toolset that you are referring to):

  • Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom and Tom van Dijk: LTSmin: High-Performance Language-Independent Model Checking. TACAS 2015
  • Alfons Laarman, Jaco van de Pol and Michael Weber. Multi-Core LTSmin: Marrying Modularity and Scalability. NFM 2011
  • Stefan Blom, Jaco van de Pol and Michael Weber. LTSmin: Distributed and Symbolic Reachability. CAV 2010

Contributors

Ordered by the number of commits (March 2015) LTSmin's contributors are:

Related Papers

Selected Documentation

  • lps2lts-sym (BDD-based reachability with mCRL2 frontend)
  • dve2lts-mc (multi-core reachability with DiVinE 2 frontend)
  • prom2lts-mc (multi-core reachability with Promela SpinS frontend)
  • lpo2lts-seq (sequential enumerative reachability with muCRL frontend)
  • etf2lts-dist (distributed reachability with ETF frontend)
  • lps2torx (TorX testing tool connector with mCRL2 frontend)
  • pbes2lts-sym (Symbolic tool reachability tool with PBES frontend: example)
  • pins2lts-sym (Symbolic tool reachability tool using the dlopen API: tutorial)
  • mapa2lts-sym (Symbolic tool reachability tool with MAPA frontend)

Supported Systems

For the use of the multi-core BDD package Sylvan and the multi-core reachability algorithms (*2lts-mc), we further recommend using a 64-bit OS.

Downloads

Installation Instructions

First, install the dependencies listed in Section "Build Dependencies" below.

Next, if you are building the software from a Git repository or release snapshot, refer to Section "Building from a Git Repository" for additional set-up instructions. Otherwise, continue by executing the following build instructions:

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

To compile LTSmin execute:

# Build
$ make

For compilation with debug options, use the following command line:

# Debug mode
$ make CFLAGS="-DLTSMIN_DEBUG -g -O0"

LTSmin's tools can then be run with an option --debug=file.c, to enable debug output from a specific source code file.

To see if LTSmin will run correctly on your system you may execute:

# Run all tests
$ make check

To install LTSmin in the default or given prefix:

# 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

The following external libraries and tools are required for building LTSmin:

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 AtermDD decision diagram package will not be built.

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 release 201409.1. However note issues: 51 (-g|--pins-guards) and 52 (pbes2lts-*). Or you can compile mCRL2 yourself; in SVN revision 13391 the two issues are resolved.

Build and install mCRL2:

cmake . -DCMAKE_INSTALL_PREFIX=... -DBUILD_SHARED_LIBS=ON
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=... -DBUILD_SHARED_LIBS=ON 

libDDD

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

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-dits, 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.

CADP

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

SCOOP

To use the language frontend for MAPA (Process Algebra for Markov Automata) SCOOP's dependencies must be met. LTSmin is distributed with SCOOP, but to use LTSmin with SCOOP the following packages must be installed.
  • GHC
  • GHC's dynamic packages; e.g. on Ubuntu install these with ghc-dynamic. On some OSs GHC's dynamic packages are distributed with GHC itself, such as on Arch Linux. Thus on these OSs GHC's dynamic packages need not be explicitly installed.
  • Happy; which can be installed with cabal: cabal install --global happy
  • Optionally one can install hashmap (cabal install --global hashmap), this will also build the SCOOP binary. The SCOOP binary allows using the SCOOP tool itself, but is not necessary to use LTSmin's mapa2lts-* tools.

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
Make sure you have installed the dependencies below and then continue with the normal installation instructions.

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.

Stand-Alone Language Modules

LTSmin installs includes and installs a frontend for Promela models called SpinS. Promela models can compiled as follows:
spins model.prom
This yields a library model.prom.spins, which can be loaded by LTSmin's prom2* tools.

DiVinE

Download a patched version of DiVinE 2.4:

git clone https://github.com/utwente-fmt/divine2.git

Build with:

cd divine2
mkdir _build && cd _build
cmake .. -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=... -DMURPHI=OFF
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.
Also, on MacOS X Divine2 only compiles with the GNU std C++ library.
Thus on MacOS X one has to provide the option -DCMAKE_CXX_FLAGS="-stdlib=libstdc++"

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 dve2* tools when passing a ".dve" model, doing it manually is rarely needed.)

opaal

For UPPAAL timed automata, the opaal language module is required. The website opaal + LTSMin provides instructions on how to install it manually.

$ opaal_ltsmin --only-compile model.xml

This produces a PINS library called "model.so", which can be passed to LTSmin tool opaal2lts-mc (only multi-core reachability and LTL model checking with tree compression is support at the moment).

TBB malloc

Scalability of the UPPAAL DBM library required by opaal can be limited without a concurrent allocator. Therefore, we recommend the installation of TBB malloc. The TBB allocator can be loaded transparently using library preloading:

export LD_PRELOAD=libtbbmalloc_proxy.so
opaal2lts-mc model.so

Licence

Copyright (c) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 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

For support/questions, email: ltsmin-support@lists.utwente.nl.
For bug reports and feature suggestions, visit: LTSmin bug tracker
For news and updates, subscribe to our mailing list: ltsmin-users@lists.utwente.nl