dve2torx [OPTION]… input<_.dve_|.dve2C>


dve2torx provides access to a labelled transition system from a specification provided in input[.dve|.dveC] via the TorX-Explorer textual interface on stdin and stdout.


Compile a DVE input model with divine:

divine compile -l input.dve

The command results in a compiled model input.dve2C.

If an LTL property is present in the model, a buchi automaton is created. LTSmin can directly perform LTL model checking on such models:

dve2lts-mc --strategy=cndfs --threads=16 anderson.6.prop4.dve2C
dve2lts-seq --por --proviso=color --strategy=scc anderson.6.prop4.dve

These two examples perform LTL model checking using: multi-core NDFS (cndfs), and a sequential SCC-based algorithm with partial order reduction (--por and --proviso, where different provisos are available). Again one can provide additional options to store traces, etc.

Note that this requires a modified version of the DiVinE toolset, which adds an LTSmin compilation backend (option -l). For availability, refer to the LTSmin website.


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.