SYNOPSIS

mpirun <nodespec> lpo2lts-mpi [OPTION]… input.tbf [output.fmt]

DESCRIPTION

lpo2lts-mpi generates a labelled transition system from a specification provided in input.tbf. Specifications are in tbf format and are commonly generated by mcrl(1) or mcrl22mcrl(1). output.fmt specifies the name of the output archive. The desired format is deduced from the filename extension.

The tool uses MPI for distributed computation, thus it has to be started via mpirun. nodespec determines which processors the tool is run on.

The workers send messages to themselves. So if you use Open MPI, you have to use mpirun -mca btl CONNECT,self NODESPEC where CONNECT can be tcp, mx, ib, etc..

OPTIONS

--nice=LEVEL

Set the nice level of all worker processes. This is useful when running on other people’s workstations.

mCRL Options

--state-names

Make the state parameters visible.

--mcrl=OPTIONS

Pass options to the mcrl(1) library. Defaults to "-alt rw".

Allowed values depend on the mcrl(1) library.

Note
 Some option combinations can lead to incorrect results, e.g., tau confluence when caching is enabled. Therefore, the use of tau confluence has been disabled, but there may be other combinations.

PINS Options

--matrix

Print the dependency matrix and exit.

-c, --cache

Enable caching of greybox calls.

If this option is used, the state space generator makes calls to the short version of the greybox next-state function and memoizes the results. If the next-state function is expensive this will yield substantial speedups.

-r, --regroup=SPEC

Enable regrouping optimizations on the dependency matrix.

SPEC is a comma-separated sequence of transformations <(T,)+> which are applied in this order to the dependency matrix. The following transformations T 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.

--ltl=LTLFILE

Compute cross-product of a Buchi automaton and the specification

LTLFILE is a file containing an Linear Temporal Logic formula (see ltsmin-ltl(5)). This formula will be converted to a Buchi automaton. Then the synchronous cross product with the original specification is computed on-the-fly. A state label is added to encode accepting states.

--ltl-semantics=spin|textbook

Change the semantics of the crossproduct generated using --ltl

Change the semantics to use incoming or outgoing edges. Two options are available, the default is spin.

spin

Use semantics similar to the spin model checker. From the source state all transitions are generated. Then, state predicates are evaluated on the source state. The Buchi automaton now moves according to these predicates.

textbook

Use textbook semantics. A new initial state is generated with an outgoing transition to the initial state. Now, predicates are evaluated on the target state and the Buchi automaton moves according to these predicates.

--por

Activate partial order reduction

Partial Order Reduction can reduce the state space when searching for deadlocks (-d) of accepting cycles (--ltl).

--proviso=closedset|stack|color

Change the proviso implementation for partial order reduction (ltl)

Change the proviso used to detect that an accepting cycle is closed. Three options are available, the default is closedset.

closedset

The closed set proviso is the default proviso which requires almost no extra work/memory. It might however result in less reduction than the stack or color proviso. It works with both the dfs- and bfs exploration strategy.

stack

The stack proviso is the proviso used for example by the spin model checker. It requires some extra work/memory but may result in a better reduction than closedset. It works only for a dfs/scc search strategy (since bfs has no stack).

color

The color proviso requires a lot of extra work and memory but can significantly improve the reduction. It too works only with the dfs/scc search strategies.

Note
 The proviso option might be used to produce shorter error traces.

Container I/O Options

--block-size=BYTES

Size of a block in bytes. Defaults to 32,768.

--cluster-size=BLOCKS

Number of blocks in a cluster. Defaults to 32.

--plain

Disable compression of output containers.

General Options

-v

Increase the level of verbosity

-q

Be quiet; do not print anything to the terminal.

--debug

Enable debugging output.

--version

Print version string of this tool.

-h, --help

Print help text

--usage

Print short usage summary.

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

EXIT STATUS

0

Successful termination.

>0

Some error occurred.

SUPPORT

Send questions, bug reports, comments and feature suggestions to the LTSmin Support Team.

SEE ALSO

ltsmin(7), ltsmin-mpi(1), ltsmin-convert(1), etf(5), muCRL, mCRL2, NIPS, DiVinE-cluster, DiVinE-2.2, MPI Forum