SYNOPSIS

This man page provides an overview of the tools in the LTSmin toolset.

Language Modules

The LTSmin toolset was designed to support multiple languages. All tools for a specific language start with a prefix that indicates the language. Below, we list the languages and the prefixes that are supported in this release:

DVE (dve)

The DVE language. See the DiVinE website.

ETF (etf)

The Enumerated Table Format is an intermediate format for models in the LTSmin toolset. See etf(5).

mCRL2 (lps)

The mCRL2 language. See the mCRL2 website.

muCRL (lpo)

The muCRL language. See the muCRL website.

Promela (prom)

The Promela language is supported via the included version of SpinS, which generates C code implementing the PINS interface. See Spin website and SpinS: Extending LTSmin with Promela through SpinJa.

UPPAAL (opaal)

The UPPAAL xml language for timed automata is supported via the opaal successor generator. Currently only multi-core reachability is supported (opaal2lts-mc(1)). See the opaal website: opaal website

PBES (pbes)

Specifications in pbes format generated by lps2pbes(1) are reduced to parity games. These can then be solved (symbolically) by spgsolver(1).

C-code (pins)

LTSmin enables linking to language modules provided as .so-files. The file dlopen-api.h needs to be included in the C-code. The pins2lts tools will load the binary at runtime. See pins2lts-seq(1), pins2lts-mc(1), pins2lts-dist(1), pins2lts-sym(1).

State Space Exploration and Analysis Tools

The LTSmin toolset has four different tools for reachability, checking for deadlocks, actions and invariants and verification of properties in Linear Temporal Logic (LTL) or modal mu-calculus.

<prefix>2lts-sym

Symbolic tools that use decision diagrams for manipulating sets of states. The optional output produced by these tools is an ETF model.

See dve2lts-sym(1), etf2lts-sym(1), lps2lts-sym(1), lpo2lts-sym(1), pbes2lts-sym(1), mapa2lts-sym(1) and prom2lts-sym(1).

To use multi-core decision diagrams, choose either Sylvan or LDDmc as DD package using the --vset option.

<prefix>2lts-seq

Sequential tools that enumerate states and can use both decision diagrams and (tree-compressed) hash tables to represent sets of states. The optional output produced by these tools is an explicit LTS. These tools are based on an extended version of the General State Exploring Algorithm (GSEA).

See dve2lts-seq(1), etf2lts-seq(1), lps2lts-seq(1), lpo2lts-seq(1), pbes2lts-seq(1) and prom2lts-seq(1).

<prefix>2lts-mc

Concurrent (multi-core) state space generators and model checkers. Enumeration uses lockless (tree-compressed) hash tables to represent sets of states. Model checking of LTL is supported by a set of multi-core NDFS algorithms. To input LTL-formulae, one can use the PINS2PINS wrapper (--ltl) or an LTL cross-product computed by the frontend (DiVinE 2 property models or PROMELA models via SpinS with never claim).

See dve2lts-mc(1), etf2lts-mc(1), lps2lts-mc(1), lpo2lts-mc(1), pbes2lts-mc(1), opaal2lts-mc(1), prom2lts-mc(1) and ltsmin-ltl(5).

  • MacOS X only supports the multiple process architecture from version 10.7 (Lion).

<prefix>2lts-dist

Distributed state space generators that enumerate states and use distributed hash tables for storing sets of states. The optional output produced by these tools is an explicit LTS. These tools work with MPI, multiple threads or multiple process whenever possible and available. For example:

  • MacOS X does not support the multiple process architecture at this time.

See dve2lts-dist(1), etf2lts-dist(1), lps2lts-dist(1), lpo2lts-dist(1), pbes2lts-dist(1), mapa2lts-dist(1), nips2lts-dist(1), and spinja2lts-dist(1)

Pins-to-pins wrappers

Most of the analysis tools offer the following options, which are implemented as a layer between the language modules and the analysis algoritms.

caching

Enable transition caching with the -c option.

regrouping

Choose regrouping and reordering heuristics with the -r option. The following regroup macros are available.

gs

Group Safely; macro for "gc,gr,cw,rs"; almost always a win.

ga

Group Aggressively (row subsumption); macro for "gc,rs,ru,cw,rs"; can be a huge win, but in some cases causes slower state space generation.

gsa

Group Simulated Annealing; macro for "gc,gr,csa,rs"; almost always a win; usually better than gs.

gc

Group Columns; macro for "cs,cn".

gr

Group Rows; macro for "rs,rn".

cs

Column Sort; sort columns lexicographically.

cn

Column Nub; (temporarily) group duplicate columns, thereby making ca more tractable. Requires cs.

cw

Column sWap; minimize distance between columns by swapping them heuristically. This reordering improves performance of the symbolic data structures.

ca

Column All permutations; try to find the column permutation with the best cost metric. Potentially, this is an expensive operation.

csa

Column Simulated Annealing; minimize distance between columns by swapping them using simulated annealing.

rs

Row Sort; sort rows lexicographically.

rn

Row Nub; remove duplicate rows from the dependency matrix. This is always a win. Requires rs.

ru

Row sUbsume; try to remove more rows than nubbing, thereby trading speed for memory. Requires rs.

w2W

Over-approximate all must-write to may-write. May-write supports the copy (-) dependency.

r2+

Over-approximate read to read+write. Allows read dependencies to also subsume write dependencies.

w2+

Over-approximate must-write to read+write. Allows must-write dependencies to also subsume read dependencies.

W2+

Over-approximate may-write to read+write. Allows must-write dependencies to also subsume read dependencies.

-2r

Over-approximate copy to read. May be useful for testing whether the dependency matrix is correct.

rb4w

Use special heuristics to move read dependencies before write dependences. Often a win in symbolic state space generation.

mm

Writes metrics of the selected (sr, sw, sc) matrix to stdout. The following metrics are printed:

  1. Event span: the total distance between the minimum and maximum column of rows.

  2. Normalized event span: the event span divided by the size of the matrix (rows x columns).

  3. Weighted event span: the weighted event span, the event span, including a moment signifying the location of the span. See, Siminiceanu et al., we use moment 1.

  4. Normalized weighted event span: the weighted event span divided by the size of the matrix (rows x column).

sr

Select the read matrix for cs, csa, cw, ca, rs, bcm, bs, bk, vcm, vacm, vgps and mm.

sw

Select the write matrix (default) for cs, csa, cw, ca, rs, bcm, bs, bk, vcm, vacm, vgps and mm. The write matrix is the default selection, because only write dependencies can create new nodes in decision diagrams. A bad variable order in the write matrix thus leads to a large number of peak nodes during reachability analysis. A bad variable order in the read matrix can also lead to a slow reachability analysis, but typically not as severe as a bad variable order in the write matrix. Slow reachability analysis due to a bad variable order in the read matrix causes many recursive calls to the relational product operation. Typically it is best that read dependencies are moved to the top DD level, thus left most in the read matrix.

sc

Select the combined matrix for cs, csa, cw, ca, rs, bcm, bs, bk, vcm, vacm, vgps and mm. The combined matrix is the logical or of the read and write matrix.

bg

Use a bipartite graph (default) for bcm, bk, bs, vcm, vacm and vgps.

tg

Create a total graph of the bipartite graph for bcm, bk, bs, vcm, vacm and vgps. This adds more vertices and edges thus increasing computation time, but sometimes provides a better ordering.

Below, the sparse matrix algorithms prefixed with b are only available when LTSmin is compiled with Boost. Algorithms prefixed with v are only available when LTSmin is compiled with ViennaCL.

bcm

Apply Boost’s Cuthill-McKee ordering.

bk

Apply Boost’s King ordering.

bs

Apply Boost’s Sloan ordering.

vcm

Apply ViennaCL’s Cuthill-McKee ordering.

vacm

Apply ViennaCL’s advanced Cuthill-McKee ordering.

vgps

Apply ViennaCl’s Gibbs-Poole-Stockmeyer ordering.

f

Apply FORCE ordering.

partial order reduction

Enable POR with the --por option.

ltl

Generate a Büchi automaton and enable detection of accepting cycles with the --ltl option. Only available in the *2lts-seq and *2lts-mc tools. See ltsmin-ltl(5).

mu-calculus

Generate a parity game with the --mucalc option. See ltsmin-mucalc(5).

State Space Reduction Tools

The LTSmin toolset provides distributed minimization with respect to various bisimulations.

ltsmin-reduce

Sequential minimization modulo strong and branching bisimulation, as well as modulo lumping of CTMCs. See ltsmin-reduce(1).

ltsmin-reduce-dist

Distributed minimization modulo strong and branching bisimulation. This tool has an implementation of the new inductive signature algorithms that work on tau-cycle free LTSs. See ltsmin-reduce-dist(1).

ltsmin-compare

Compare two transitions systems, using the same equivalences as supported by ltsmin-reduce. See ltsmin-compare(1).

Tau Cycle Elimination Tool

The LTSmin toolset provides distributed tau-cycle elimination.

ce-mpi

Distributed tau cycle elimination. See ce-mpi(1).

TorX RPC interfaces

The LTSmin toolset provides TorX RPC interfaces.

<prefix>2torx

TorX RPC interface.

See dve2torx(1), etf2torx(1), lps2torx(1), lpo2torx(1), and prom2torx(1).

Trace Pretty Printing

ltsmin-printtrace

Pretty print traces. See ltsmin-printtrace(1).

Conversion Tools

etf-convert

Translate ETF to DVE. See etf-convert(1).

ltsmin-convert

Convert LTS file formats. See ltsmin-convert(1).

gcf

Utility for creating and extracting Generic Container Format archives. See gcf(1).

File Formats

The following file formats are supported:

  • Directory format (*.dir, *.dz and *.gcf)

  • Vector format (*.dir, *.gcd, *.gcf)

  • Binary Coded Graphs (*.bcg)

  • Aldebaran Format (*.aut)

  • FSM Format (*.fsm)

  • MRMC/Prism (*.tra+*.lab)

  • PGSolver format (*.pg)

If a tool operates in streaming mode then support for file formats is limited, as can be seen in the following table:

Format Streaming mode Load/Store mode

DIR

R/W

R/W

VEC

R/W

R/W

BCG

W

R/W

AUT

W

R/W

FSM

W

W

TRA

-

R/W

PG

-

W

The directory format uses multiple files to store an LTS. The various extension explain how these files are stored in the underlying file system. The *.dir format uses multiple files in a directory without compression. If the LTS has one edge label, no state labels and does not store state vectors then these files are backwards compatible. Neither the *.dz nor the *.gcf formats are backwards compatible. Both formats use compression. The first uses a directory for the files, second interleaves files into a single file.

If you try to open a *.dir with the old mCRL tools and you get the error message:

wrong file version: 0

then the directory is probably compressed. If that happens then you may convert the directory by typing the command:

ltsmin-convert bad.dir good.dir

Mini Tutorial

As running example, we use a model of the bounded retransmission protocol from the mCRL examples. Assuming we have copied the file brp.mcrl to our working directory, we can linearize the model with the following command:

mcrl -regular -nocluster brp.mcrl

This produces a file named brp.tbf. This is the input for the state space generator. Just to see how many states and transitions are produced, we can run the command

lpo2lts-seq brp.tbf

Assuming that the model is small and CADP is installed, we can simply generate a BCG file (this requires BFS exploration order)

lpo2lts-seq --strategy=bfs brp.tbf brp.bcg

and then use CADP.

If it turns out that the LTS was very big then we might want to use the distributed tools to generate and reduce the LTS:

lpo2lts-dist --workers=4 brp.tbf brp.dir
ltsmin-reduce-dist --workers=4 brp.dir brp-s.dir
ltsmin-convert --rdwr --segments 1 brp-s.dir brp-s.bcg

The tools start the command mpirun silently in the background with the suitable options. Alternatively, one may wish to call mpirun with additional options. This can be done using the --mpi option, e.g.:

mpirun -np 4 -mca btl tcp,self lpo2lts-dist --mpi brp.tbf brp.dir

The dir format used to store the LTS in the example is backwards compatible with the mCRL toolset. We also support a newer format that adds compression:

lpo2lts-dist --workers=4 brp.tbf brp.gcf
ltsmin-reduce-dist --workers=4 brp.gcf brp-s.gcf
ltsmin-convert --rdwr --segments 1 brp-s.gcf brp-s.bcg

When the model is suitable, state space generation can be speeded up by memoizing next state calls:

lpo2lts-dist --workers=4 --cache brp.tbf brp.gcf

Symbolic tools

The LTSmin toolset also has a symbolic reachability tool. If we want to know the number of states, we can give the command:

lpo2lts-sym brp.tbf

This command will compute the necessary part of the transition relation and the set of reachable states. If we want to record the transition relation symbolically then we can do so in the form of an ETF file:

lpo2lts-sym brp.tbf brp.etf

This etf file can be translated to DVE for model checking:

etf-convert brp.etf brp.dve

It can also serve as the input for state space generation

etf2lts-dist --workers=4 brp.etf brp-s.gcf

Parity game solver

The LTSmin toolset finally includes a parity game solver:

etf2lts-sym --mucalc=property.mcf model.etf --pg-write=game.spg
spgsolver game.spg

To tool reports whether the game successfully terminates.