lps2torx(1)

SYNOPSIS

lps2torx [OPTION]… input.lps

DESCRIPTION

lps2torx provides access to a labelled transition system from a specification provided in input.lps via the TorX-Explorer textual interface on stdin and stdout. Specifications are in lps format and are commonly generated by mcrl22lps(1).

OPTIONS

mCRL2 Options

--mcrl2=OPTIONS: Pass options to the mCRL2 library. Defaults to "--rewriter=jittyc".

The "--rewriter=<rewriter>" option is the only recognized option. Possible rewriters are jitty and jittyc.
--mcrl2-finite-types: Use mCRL2 finite type information.

Enabling this option may cause premature termination in case non-normal-form instances of finite types occur in the state space. This will be the case, e.g., when the specification has been pre-processed using lpsparunfold(1).
--mcrl2-readable-edge-labels: Use human readable edge labels.

Enabling this option may cause problems during bisimulation reduction, e.g., the edge labels l(0) with 0 of type Nat and l(0) with 0 of type Pos will be mapped to the same string.

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.

--allow-undefined-edges

Allow values for edge variables in atomic predicates to be unreachable.

--allow-undefined-values

Allow undefined values in atomic predicates for enums.

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

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

Event span: the total distance between the minimum and maximum column of rows.
Normalized event span: the event span divided by the size of the matrix (rows x columns).
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.
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.

--row-perm=PERM

Apply row permutation PERM, where PERM is a sequence of row numbers, separated by a comma. E.g. the vector 2,1,0 will swap row 2 with row 0.

--col-perm=PERM

Apply column permutation PERM, where PERM is a sequence of column numbers, separated by a comma. E.g. the vector 2,1,0 will swap column 2 with column 0.

--col-ins=PAIRS

Insert columns before other columns in the dependency matrix.

PAIRS is a comma-separated sequence of pairs <(C.C,)+>'. E.g. --col-ins=1.0 will insert column 1 before column 0. Each pair contains a source column C and a target column C'. During the application of the whole sequence, C will always be the column number that corresponds with the column before the application of the whole sequence. The column number C' will always be the column during the application of the whole sequence. This means that in for example --col-ins=2.0,1.0, first column 2 is inserted at position 0, then column 1 is inserted at position 0. The result will be that the original column 2 will be at position 1. Another important detail is that when --col-ins is used, all source columns will temporarily be "removed" during reordering from the dependency matrix, i.e. when the -r,--regroup option is given. After reordering is done, the columns will be inserted at the desired target position. In other words, reordering algorithms given by the option -r,--regroup, will only be applied on the dependency matrix with source columns removed.

--sloan-w1=WEIGHT1

Use WEIGHT1 as the first weight for the Sloan algorithm, see https://www.boost.org/doc/libs/1_66_0/libs/graph/doc/sloan_ordering.htm.

--sloan-w2=WEIGHT2

Use WEIGHT2 as the second weight for the Sloan algorithm, see https://www.boost.org/doc/libs/1_66_0/libs/graph/doc/sloan_ordering.htm.

--graph-metrics

Print Boost’s and ViennaCL’s graph metrics (only available when LTSmin is compiled with Boost or ViennaCL).

--regroup-exit

Exit with 0 when regrouping is done.

--regroup-time

Print timing information of each transformation, given in sequence --regroup (-r).

--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=heur|del

Activate partial-order reduction

Partial-Order Reduction (POR) can reduce the state space when searching for deadlocks (-d) or accepting cycles (--ltl). Two POR algorithms are available:

heur: Uses a cost-based heuristic beam-search to find the smallest stubborn set
del: Uses Valmari’s deletion algorithm to find the smallest stubborn set by iteratively removing transitions while maintaining the constraints.

--weak

Use weak commutativity in partial-order reduction. Possibly yielding better reductions.

--leap

Use leaping partial-order reduction, by combining several disjoint stubborn sets sequentially.

Environment Variables

LTSmin supports the following list of environment variables.

Table 1. Environment Variables:
Name	Unit	Description
LTSMIN_MEM_SIZE	bytes	Sets the amount of system memory to the given value.
LTSMIN_NUM_CPUS	constant	Sets the amount of CPUs to the given value.

The variables LTSMIN_MEM_SIZE, and LTSMIN_NUM_CPUS are particularly relevant when neither sysconf(3) nor cgroups(7) is able to properly detect these limits, e.g. when LTSmin runs on Travis CI in a docker container.

General Options

-v: Increase the level of verbosity
-q: Be quiet; do not print anything to the terminal.
--debug=<file.c>: Enable debugging output for file.c (option allowed multiple times).
--version: Print version string of this tool.
-h, --help: Print help text
--usage: Print short usage summary.

EXIT STATUS

0: Successful termination.
255: Some error occurred.

SUPPORT

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

lps2torx(1) Manual Page

NAME