SYNOPSIS

lpo2lts-dist [OPTION]… input.tbf [output.fmt]

DESCRIPTION

lpo2lts-dist 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. Available formats are described below.

Using the option --workers=N, this tool starts the command mpirun silently in the background with the suitable options, i.e. -np 4. 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 {manname} --mpi

OPTIONS

--nice=LEVEL

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

--write-state

Write the full state vector.

--filter=<patternlist>

Select the labels to be written to file from the state vector elements, state labels and edge labels. The argument is a semicolon separated list of shell file patterns. Each pattern may be prefixed with "!" to exclude a set of labels. If none of the patterns matches the default is to exclude the label. Hence, all labels starting with an "x" are specified as "x*". The complement all labels, except those starting with an "x" are specified as "!x*;*".

--cost=<edge label>

The given edge labels defines the cost of an edge. Based on this cost, the lowest cost for reaching every state is computed. Moreover, the order in which states are explored is such that lower cost states are explored before higher costs ones. The levels reported when this options is in effect are cost levels. The counter-example traces are guaranteed to be a lowest cost path. However, the length of the trace may not be minimal.

-n, --no-exit

Do not exit when an error is found. Just count errors. Error counts are printed with -v.

-d, --deadlock

Find state with no outgoing transitions. Returns with exit code 1 if a deadlock is found, 0 or 255 (error) otherwise.

-i, --invariant=PREDFILE|PREDEXPRESSION

Find state where the invariant is violated. The file PREDFILE contains an expression in a simple predicate language (see ltsmin-pred(5)). Its contents can also be entered directly as a PREDEXPRESSION. Returns with exit code 1 if a violation is found, 0 or 255 (error) otherwise.

-a, --action=STRING

Find state with an outgoing transition of type STRING. Returns with exit code 1 if the action is found, 0 or 255 (error) otherwise.

--trace='FILE'.gcf

When finding a deadlock state or a transition labelled with a certain action, write a trace to 'FILE'.gcf, beginning from the initial state. Traces can be pretty-printed with ltsmin-printtrace(1).

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.
-n, --no-exit

Do not exit when an error is found. Just count errors. Error counts are printed with -v.

-d, --deadlock

Find state with no outgoing transitions. Returns with exit code 1 if a deadlock is found, 0 or 255 (error) otherwise.

-i, --invariant=PREDFILE|PREDEXPRESSION

Find state where the invariant is violated. The file PREDFILE contains an expression in a simple predicate language (see ltsmin-pred(5)). Its contents can also be entered directly as a PREDEXPRESSION. Returns with exit code 1 if a violation is found, 0 or 255 (error) otherwise.

-a, --action=STRING

Find state with an outgoing transition of type STRING. Returns with exit code 1 if the action is found, 0 or 255 (error) otherwise.

--trace='FILE'.gcf

When finding a deadlock state or a transition labelled with a certain action, write a trace to 'FILE'.gcf, beginning from the initial state. Traces can be pretty-printed with ltsmin-printtrace(1).

PINS Options

--labels

Print state variable, type and value names, and state and action labels. Then exit. Useful for writing predicate (--invariant), LTL (--ltl), CTL/CTL* (--ctl), and mu-calculus (--mu) expressions.

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

--pins-guards

Use guards in combination with the long next-state function to speed up the next-state function.

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

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.

rb4w

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

--mucalc=FILE|FORMULA

Compute a parity game for the mu-calculus formula.

The mu-calculus formula is provided in the file FILE or directly as a string FORMULA. The syntax and tool support are described in ltsmin-mucalc(5).

--por

Activate partial order reduction

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

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

Hybrid Runtime Options

The Hybrid Runtime Environment provides startup options for several parallel architectures.

Posix threads options

If the application supports it and Posix threads are supported by the OS then the following option is available:

--threads[=count]

Start count worker threads. The default count is the number of CPU’s in the system.

Posix processes options

If the application supports it and Posix shared memory is supported by the OS then the following option is available:

--procs[=count]

Fork count worker processes. The default count is the number of CPUs in the system.

Note that MacOS X only supports Posix shared memory from version 10.7 (Lion) onwards.

MPI options

If the application supports it and MPI support was compiled into the binary then the following options are available:

--workers=count

Start the program with count MPI workers.

--mpirun=mpirun arguments

Invoke mpirun with the given arguments.

--mpi

Ignore --workers and --mpirun options and start the MPI runtime.

General Options

-v

Increase the level of verbosity

-q

Be quiet; do not print anything to the terminal.

--debug=file

Enable debugging output for file.

--version

Print version string of this tool.

-h, --help

Print help text

--usage

Print short usage summary.

--stats

Enable statistics gathering/printing.

--where

Include file and line number in debug messages.

--when

Include the wall time since program start in all messages.

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

EXIT STATUS

0

Successful termination.

1

Counter example found.

255

Some error occurred.

SUPPORT

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

SEE ALSO