lpo-reach - Symbolic reachability analysis for muCRL models.
lpo-reach [OPTION]… file.tbf [outfile.etf]
lpo-reach performs a reachability analysis on a specification provided in file.tbf. Specifications are in tbf format and are commonly generated by mcrl(1) or mcrl22mcrl(1). outfile.etf specifies the name of the output archive, written in etf(5) format.
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 cisited 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.
Select an experimental saturation-like strategy: none, sat-like, sat-loop, sat-ddd. 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-ddd strategy repeatedly performs a fixpoint computation. All strategies except sat-ddd work in combination with the order to saturate levels. Defaults to none, i.e. no saturation.
Select the granularity of the saturation-like strategy. Defaults to 10.
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.
Find a transition labelled with ACTION. Returns with exit code 1 if such a transition is found, otherwise 0.
After computing all reachable states, evaluate the mu-formula in MUFILE
MUFILE is a file containing an 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.
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.
Find state with no outgoing transitions. Returns with exit code 1 if deadlock is found, otherwise 0.
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).
Make the state parameters visible.
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. |
Print the dependency matrix and exit.
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.
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 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 changing columns 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.
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.
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.
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.
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.
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.
Activate partial order reduction
Partial Order Reduction can reduce the state space when searching for deadlocks (-d) of accepting cycles (--ltl).
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.
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.
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).
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. |
Select type of vector set: list, tree, fdd, ddd, ldd. With list, ATermDD with list encoding are used. With tree, ATermDD with tree encoding are used. With fdd, BuDDy FDDs are used. With ldd, a non-ATermDD vector set with list encoding is used. With ddd, libDDD SDDs are used. Defaults to first available type in the list.
Set cache ration. Defaults to 64.
Set maximum increase. Defaults to 1,000,000.
Sets the minimum percentage of free nodes as integer between 0 and 100. Defaults to 20.
Sets the number of bits for each FDD variable. Defaults to 16.
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.
Increase the level of verbosity
Be quiet; do not print anything to the terminal.
Enable debugging output.
Print version string of this tool.
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.