Model Checking and LTS Minimization
LTSmin is a toolset for model checking and manipulating labelled transition systems. LTSmin already connects a sizeable number of existing (verification) tools: muCRL, mcrl2, DiVinE, SPIN via an included version of SpinJa, NIPS, CADP and opaal. 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, opaal 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), partial order reduction and linear temporal logic.
Download shortcut: http://fmt.cs.utwente.nl/tools/ltsmin/ltsmin.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):
- 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
Related Papers
- Alfons Laarman, Elwin Pater, Jaco van de Pol and Michael Weber. Guard-based Partial-Order Reduction . SPIN 2013
- Alfons Laarman, Mads Chr. Olesen and Andreas Dalsgaard, Kim G. Larsen, Jaco van de Pol. Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction . CAV 2013
- Alfons Laarman and David Farago. Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO . NASA FM 2013
- Tom van Dijk, Alfons Laarman and Jaco van de Pol. Multi-core and/or Symbolic Model Checking. AVOCS 2012
- Freark van der Berg and Alfons Laarman. SpinS: Extending LTSmin with Promela through SpinJa. PDMC 2012
- Tom van Dijk, Alfons Laarman and Jaco van de Pol. Multi-core BDD Operations for Symbolic Reachability. PDMC 2012
- Tom van Dijk. The parallelization of binary decision diagram operations for model checking. 2012. Thesis
- Sami Evangelista, Alfons Laarman, Laure Petrucci and Jaco van de Pol. Improved Multi-Core Nested Depth-First Search. ATVA 2012
- Andreas Dalsgaard, Alfons Laarman, Kim G. Larsen, Mads Chr. Olesen and Jaco van de Pol. Multi-Core Reachability for Timed Automata. FORMATS 2012
- Gijs Kant and Jaco van de Pol. Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games. Graphite 2012
- Alfons Laarman and Jaco van de Pol. Variations on Multi-Core Nested Depth-First Search. PDMC 2011
- Elwin Pater. Partial Order Reduction for PINS. 2011. Thesis
- Tien Loong Siaw. Saturation for LTSmin. 2012. Thesis
- Alfons Laarman, Rom Langerak, Jaco van de Pol, Michael Weber and Anton Wijs. Multi-Core Nested Depth-First Search. ATVA 2011
- Alfons Laarman, Jaco van de Pol and Michael Weber. Multi-Core LTSmin: Marrying Modularity and Scalability . NFM 2011
- Alfons Laarman, Jaco van de Pol and Michael Weber. Parallel Recursive State Compression for Free . SPIN 2011
- Alfons Laarman, Jaco van de Pol and Michael Weber. Boosting Multi-Core Reachability Performance with Shared Hash Tables. FMCAD 2010
- Stefan Blom, Jaco van de Pol and Michael Weber. LTSmin: Distributed and Symbolic Reachability. CAV 2010, LNCS 6174, pp. 354–359.
- 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)
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)
Supported Systems
- GNU/Linux (tested on Ubuntu, Debian, OpenSuSE 11.2)
- MacOS X, version 10.7 "Lion"
- MacOS X, version 10.6 "Snow Leopard" (except multi-core muCRL/mCRL2)
- MacOS X, version 10.5 "Leopard" (except multi-core muCRL/mCRL2)
- Cygwin/Windows (tested on Windows 7 with Cygwin 1.7)
Downloads
- Released Versions
- Snapshots (consult the build server for their constitution)
- 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 test branch)
- ltsmin.git (browsable Git repository) This is a read-only Git repository, where the master branch is equal to the released tarball, the maint branch contains fixes on top of master, and the next branch is our development branch containing (unstable) features that will be included in the next release. For direct checkout using git:
$ git clone -b next http://fmt.cs.utwente.nl/tools/scm/ltsmin.git
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
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/>.
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 201202.0. Note that all versions before SVN rev.10225 are insufficient (in particular, all versions of mCRL2 up to and including the July 2011 release).
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=...
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=... -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.
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 multi-core reachability on timed automata, the opaal frontend is required (follow the instructions in the README). After downloading and installing opaal, use the following command line to compile a UPPAAL xml model:
$ 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 is support at the moment).
TBB malloc
Scalability can be limited without a concurrent allocator, hence the opaal2lts-mc frontend is not compiled in absence of TBB malloc.
CADP
See the CADP website on how to obtain a license and download the CADP toolkit.
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-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.
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 $ ./ltsminreconfMake 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.
Apache Ant
See above.
Licence
Copyright (c) 2008, 2009, 2010, 2011, 2012, 2013, 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@cs.utwente.nl.
For bug reports and feature suggestions, visit:
LTSmin bug tracker
For news and updates, subscribe to our mailing list:
ltsmin-devel@lists.utwente.nl
