SYNOPSIS
lps-reach [OPTION]… input.lps [output.etf]
DESCRIPTION
lps-reach performs a reachability analysis on a specification provided in input.lps. Specifications are in lps format and are commonly generated by mcrl22lps(1). output.etf specifies the name of the output archive, written in etf(5) format.
OPTIONS
- --order=ORDER
-
Select the exploration strategy: bfs-prev, bfs, chain-prev, or chain. With bfs-prev and bfs, breadth-first search is used. Here, bfs-prev only considers the states found at the previous level, while bfs considers the whole visited set. With chain-prev and chain, a chaining strategy is used. Here, chain-prev at each level starts from the states found at the previous level, while chain uses the whole visited set. Defaults to bfs-prev.
When using breadth-first search, the tool performs the next state computation for all edge groups on the current level or current set of visited states. Chaining means to apply next state for the first group to the visited states, then apply next-state for the second group to the result, etc. Thus, a chaining analysis can be completed in much less iterations than a BFS analysis.
- --saturation=SATURATION
-
Select a saturation strategy: none, sat-like, sat-loop, sat-fix, sat. The sat-like strategy goes up and down the levels of the BDD used to represent the state space. The sat-loop strategy loops over the levels. The sat-fix strategy repeatedly performs a fixpoint computation using saturation. The sat strategy does saturation as described in the literature with on-the-fly expansion of the transition relations. Defaults to none, i.e. no saturation.
All strategies except sat-fix and sat work in combination with the order to saturate levels.
- --sat-granularity=GRANULARITY
-
Select the granularity of sat-like and sat-loop strategies. The granularity indicates how many BDD levels are considered at the same time. Defaults to 10.
- --save-sat-levels
-
Save the previous states seen at saturation levels. This option has effect for any of the saturation strategies in combination with either bfs-prev or chain-prev.
- --action=ACTION
-
Find a transition labeled with ACTION. Returns with exit code 1 if such a transition is found, otherwise 0.
- --guidance=STRATEGY
-
Select a search strategy for searching for actions: unguided, directed. The unguided strategy considers all transition groups. The directed strategy focuses the search on the transition groups in which the action occurs. Defaults to unguided.
- --mu=MUFILE
-
After computing all reachable states, evaluate the mu-formula in MUFILE
MUFILE is a file containing a Mu Calculus formula (see ltsmin-mu(5)). This formula is a propositional formula with least and greatest fixpoint operator. It will be evaluated after generation of the complete state space.
- --ctl*=CTLFILE
-
Convert a ctl* formula given in CTLFILE (see ltsmin-ctl(5)) to a mu-formula (see ltsmin-mu(5)), and evaluate the mu-formula after computing all reachable states.
- -d, --deadlock
-
Find state with no outgoing transitions. Returns with exit code 1 if deadlock is found, otherwise 0.
- --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-tracepp(1).
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. |
Vector Set Options
- --vset=TYPE
-
Select type of vector set: ldd, list, tree, fdd, or ddd. With ldd, the ListDD list encoding is used (non-ATerm based). With list, ATermDD with list encoding is used. With tree, ATermDD with tree encoding is used. With fdd, BuDDy FDDs are used. With ddd, libDDD SDDs are used. Defaults to first available type in the list.
ListDD Options
- --ldd-step=STEP
-
The internal tables of ListDD resize according to the Fibonacci series. This option sets the initial size to the Fibonacci number STEP. Defaults to 30.
BuDDy Options
- --cache-ratio=RATIO
-
Set cache ration. Defaults to 64.
- --max-increase=NUMBER
-
Set maximum increase. Defaults to 1,000,000.
- --min-free-nodes=PERCENTAGE
-
Sets the minimum percentage of free nodes as integer between 0 and 100. Defaults to 20.
- --fdd-bits=BITS
-
Sets the number of bits for each FDD variable. Defaults to 16.
- --fdd-reorder=STRATEGY
-
Sets the strategy for dynamic variable reordering. Valid options are none, win2, win2ite, win3, win3ite, sift, siftite, random. Refer to the BuDDy manual for details. Defaults to none.
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.