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
- --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. |
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.
EXIT STATUS
- 0
-
Successful termination.
- >0
-
Some error occurred.
SUPPORT
Send questions, bug reports, comments and feature suggestions to the LTSmin Support Team.