lps2torx [OPTION]… input.lps


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


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.


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


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


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.


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.


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:


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


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.


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


Group Columns; macro for "cs,cn".


Group Rows; macro for "rs,rn".


Column Sort; sort columns lexicographically.


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


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


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


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


Row Sort; sort rows lexicographically.


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


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


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


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


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


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


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


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


Activate partial order reduction

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

General Options


Increase the level of verbosity


Be quiet; do not print anything to the terminal.


Enable debugging output for file.c (option allowed multiple times).


Print version string of this tool.

-h, --help

Print help text


Print short usage summary.



Successful termination.


Some error occurred.


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