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,dve2)

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.

NIPS-VM(nips)

The NIPS Virtual Machine. See the NIPS-VM website.

PROMELA(spinja)

The PROMELA language. See the Spin website and the SpinJa website.

State Space Exploration Tools

The LTSmin toolset has six tools for reachability analysis:

<prefix>-reach

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

See dve-reach(1), dve2-reach(1), etf-reach(1), lps-reach(1), lpo-reach(1), nips-reach(1), and spinja-reach(1).

<prefix>2lts-grey

Sequential state space generators 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.

See dve2lts-grey(1), dve22lts-grey(1), etf2lts-grey(1), lps2lts-grey(1), lpo2lts-grey(1), nips2lts-grey(1), and spinja2lts-grey(1).

<prefix>2lts-gsea

Sequential state space generators 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-gsea(1), dve22lts-gsea(1), etf2lts-gsea(1), lps2lts-gsea(1), lpo2lts-gsea(1), nips2lts-gsea(1), and spinja2lts-gsea(1).

<prefix>2lts-mc

Concurrent (multi-core) state space generators that enumerate states and can use (tree-compressed) hash tables to represent sets of states.

See dve2lts-mc(1), dve22lts-mc(1), etf2lts-mc(1), nips2lts-mc(1), and spinja2lts-mc(1).

<prefix>2lts-mpi

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 do not work without MPI.

See dve2lts-mpi(1), dve22lts-mpi(1), etf2lts-mpi(1), lps2lts-mpi(1), lpo2lts-mpi(1), nips2lts-mpi(1), and spinja2lts-mpi(1).

<prefix>2lts-hre

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:

State Space Reduction Tools

The LTSmin toolset provides distributed minimization various bisimulations.

ltsmin-mpi

Distributed minimization modulo strong and branching bisimulation. See ltsmin-mpi(1).

sigmin-mpi

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 sigmin-mpi(1).

sigmin-one

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

ltscmp-one

Compare two transitions systems, using the same equivalences as supported by sigmine-one. See ltscmp-one(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), dve22torx(1), etf2torx(1), lps2torx(1), lpo2torx(1), nips2torx(1), and spinja2torx(1).

Trace Pretty Printing

ltsmin-tracepp

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

Conversion Tools

ltstrans

Convert LTS file formats. See ltstrans(1).

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)

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

The directory format uses multiple files to store a 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-grey brp.tbf

Assuming that the model is small and CADP is installed, we can simply generate a BCG file

lpo2lts-grey 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:

mpirun -np 4 -mca btl tcp,self lpo2lts-mpi brp.tbf brp.dir
mpirun -np 4 -mca btl tcp,self ltsmin-mpi brp.dir brp-s.dir
ltsmin-convert --segments 1 brp-s.dir brp-s.bcg

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:

mpirun -np 4 -mca btl tcp,self lpo2lts-mpi brp.tbf brp.gcf
mpirun -np 4 -mca btl tcp,self ltsmin-mpi brp.gcf brp-s.gcf
ltsmin-convert --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:

mpirun -np 4 -mca btl tcp,self lpo2lts-mpi --cache brp.tbf brp.gcf

symbolic tools

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

lpo-reach 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 necessary part of the transition relation then we can do so in the form of an ETF file:

lpo-reach 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

mpirun -np 4 -mca btl tcp,self etf2lts-mpi brp.etf brp-s.gcf