SYNOPSIS
dve2ltssym [OPTION]… input<_.dve_.dve2C> [output.etf]
DESCRIPTION
dve2ltssym performs a reachability analysis on a specification provided in input.dve/input.dve2C. Specifications are in dve format, or in dve2C format generated by the divine tool. output.etf specifies the name of the output etf(5).
DIVINE
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:
dve2ltsmc strategy=cndfs threads=16 anderson.6.prop4.dve2C
dve2ltsseq por proviso=color strategy=scc anderson.6.prop4.dve
These two examples perform LTL model checking using: multicore NDFS (cndfs),
and a sequential SCCbased 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.
OPTIONS
 order=ORDER

Select the exploration strategy: bfsprev, bfs, chainprev, or chain. With bfsprev and bfs, breadthfirst search is used. Here, bfsprev only considers the states found at the previous level, while bfs considers the whole visited set. With chainprev and chain, a chaining strategy is used. Here, chainprev at each level starts from the states found at the previous level, while chain uses the whole visited set. Defaults to bfsprev.
When using breadthfirst 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 nextstate 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, satlike, satloop, satfix, sat. The satlike strategy goes up and down the levels of the BDD used to represent the state space. The satloop strategy loops over the levels. The satfix strategy repeatedly performs a fixpoint computation using saturation. The sat strategy does saturation as described in the literature with onthefly expansion of the transition relations. Defaults to none, i.e. no saturation.
All strategies except satfix and sat work in combination with the order to saturate levels.
 satgranularity=GRANULARITY

Select the granularity of satlike and satloop strategies. The granularity indicates how many BDD levels are considered at the same time. Defaults to 10.
 savesatlevels

Save the previous states seen at saturation levels. This option has effect for any of the saturation strategies in combination with either bfsprev or chainprev.
 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.
 dot=DIR

If this option is supplied DIR is a directory to which dot files of vector sets are written to. Note that this option should only be used for smaller vector sets because of disk space.
Three type of dot files are (over)written:

currentl<L>.dot: the nodes in the vector set at level L (and only level L),

visitedl<L>.dot: the nodes in the vector set up to and included level L,

group_nextl<L>k<K>.dot: the nodes in the transition relation of group K at level L.

 mu=MUFILEMUFORMULA

After computing all reachable states, evaluate the muformula in MUFILE
MUFILE is a file containing a Mu Calculus formula (see ltsminmu(5)). Alternatively, the formula can be provide directly as MUFORMULA. This formula is a propositional formula with least and greatest fixpoint operator. It will be evaluated after generation of the complete state space.
 ctlstar=CTLFILECTLFORMULA

CTLFILE is a file containing an Linear Temporal Logic Star (CTL*) formula (see ltsminctl(5)). Which content can also be provided directly as CTLFORMULA. The formula is translated to a muformula (see ltsminmu(5)), which is evaluated after computing all reachable states.
 nomatrix

Do not print the dependency matrix if v (verbose) is used.
 nosoundnesscheck

When using pinsguards=assumetrue disable the soundness check of the model specification. The soundness check may be expensive and can be disabled when the model specification is known to be sound. A guard may not evaluate to true or false but to maybe. A guard which evaluates to maybe depends on the evaluation of another guard. For languages such as Promela and DVE it checks whether if a guard evaluates to maybe there is another guard on the left which evaluates to false. For languages such as mCRL2 it also checks whether a guard on the right evaluates to false. If for all states this holds then the model specification is sound for guardsplitting.
 precise

Compute the final number of states precisely.
 nextunion

If supported by the vset implementation; perform the computation of successor states simultaneously with unifying the current states. Simultaneously, means with a single BDD/MDD operation.
 invpar

Checks all invariants in parallel.
 invbinpar

Checks both sides of a binary operand in parallel in an invariant, requires invpar. Note that this option may actually slow down invariant checking, because parallelization of a binary operand disables shortcircuit evaluation.
 n, noexit

Do not exit when an error is found. Just count errors. Error counts are printed with
v
.  d, deadlock

Find state with no outgoing transitions. Returns with exit code 1 if a deadlock is found, 0 or 255 (error) otherwise.
 i, invariant=PREDFILEPREDEXPRESSION

Find state where the invariant is violated. The file PREDFILE contains an expression in a simple predicate language (see ltsminpred(5)). Its contents can also be entered directly as a PREDEXPRESSION. Returns with exit code 1 if a violation is found, 0 or 255 (error) otherwise.
 a, action=STRING

Find state with an outgoing transition of type STRING. Returns with exit code 1 if the action is found, 0 or 255 (error) otherwise.
 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 prettyprinted with ltsminprinttrace(1).
PINS Options
 labels

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 mucalculus (mu
) expressions.  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 nextstate function and memoizes the results. If the nextstate function is expensive this will yield substantial speedups.
 pinsguards

Use guards in combination with the long nextstate function to speed up the nextstate function.
 allowundefinededges

Allow values for edge variables in atomic predicates to be unreachable.
 allowundefinedvalues

Allow undefined values in atomic predicates for enums.
 r, regroup=SPEC

Enable regrouping optimizations on the dependency matrix.
SPEC is a commaseparated 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.
 w2W

Overapproximate all mustwrite to maywrite. Maywrite supports the copy () dependency.
 r2+

Overapproximate read to read+write. Allows read dependencies to also subsume write dependencies.
 w2+

Overapproximate mustwrite to read+write. Allows mustwrite dependencies to also subsume read dependencies.
 W2+

Overapproximate maywrite to read+write. Allows mustwrite dependencies to also subsume read dependencies.
 2r

Overapproximate copy to read. May be useful for testing whether the dependency matrix is correct.
 rb4w

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

Writes metrics of the selected (sr, sw, sc) matrix to stdout. The following metrics are printed:

Event span: the total distance between the minimum and maximum column of rows.

Normalized event span: the event span divided by the size of the matrix (rows x columns).

Weighted event span: the weighted event span, the event span, including a moment signifying the location of the span. See, Siminiceanu et al., we use moment 1.

Normalized weighted event span: the weighted event span divided by the size of the matrix (rows x column).

 sr

Select the read matrix for cs, csa, cw, ca, rs, bcm, bs, bk, vcm, vacm, vgps and mm.
 sw

Select the write matrix (default) for cs, csa, cw, ca, rs, bcm, bs, bk, vcm, vacm, vgps and mm. The write matrix is the default selection, because only write dependencies can create new nodes in decision diagrams. A bad variable order in the write matrix thus leads to a large number of peak nodes during reachability analysis. A bad variable order in the read matrix can also lead to a slow reachability analysis, but typically not as severe as a bad variable order in the write matrix. Slow reachability analysis due to a bad variable order in the read matrix causes many recursive calls to the relational product operation. Typically it is best that read dependencies are moved to the top DD level, thus left most in the read matrix.
 sc

Select the combined matrix for cs, csa, cw, ca, rs, bcm, bs, bk, vcm, vacm, vgps and mm. The combined matrix is the logical or of the read and write matrix.
 bg

Use a bipartite graph (default) for bcm, bk, bs, vcm, vacm and vgps.
 tg

Create a total graph of the bipartite graph for bcm, bk, bs, vcm, vacm and vgps. This adds more vertices and edges thus increasing computation time, but sometimes provides a better ordering.
Below, the sparse matrix algorithms prefixed with b are only available when LTSmin is compiled with Boost. Algorithms prefixed with v are only available when LTSmin is compiled with ViennaCL.
 bcm

Apply Boost’s CuthillMcKee ordering.
 bk

Apply Boost’s King ordering.
 bs

Apply Boost’s Sloan ordering.
 vcm

Apply ViennaCL’s CuthillMcKee ordering.
 vacm

Apply ViennaCL’s advanced CuthillMcKee ordering.
 vgps

Apply ViennaCl’s GibbsPooleStockmeyer ordering.
 f

Apply FORCE ordering.
 rowperm=PERM

Apply row permutation PERM, where PERM is a sequence of row numbers, separated by a comma. E.g. the vector 2,1,0 will swap row 2 with row 0.
 colperm=PERM

Apply column permutation PERM, where PERM is a sequence of column numbers, separated by a comma. E.g. the vector 2,1,0 will swap column 2 with column 0.
 colins=PAIRS

Insert columns before other columns in the dependency matrix.
PAIRS is a commaseparated sequence of pairs <(C.C,)+>'. E.g. colins=1.0 will insert column 1 before column 0. Each pair contains a source column C and a target column C'. During the application of the whole sequence, C will always be the column number that corresponds with the column before the application of the whole sequence. The column number C' will always be the column during the application of the whole sequence. This means that in for example colins=2.0,1.0, first column 2 is inserted at position 0, then column 1 is inserted at position 0. The result will be that the original column 2 will be at position 1. Another important detail is that when colins is used, all source columns will temporarily be "removed" during reordering from the dependency matrix, i.e. when the r,regroup option is given. After reordering is done, the columns will be inserted at the desired target position. In other words, reordering algorithms given by the option r,regroup, will only be applied on the dependency matrix with source columns removed.
 sloanw1=WEIGHT1

Use WEIGHT1 as the first weight for the Sloan algorithm, see https://www.boost.org/doc/libs/1_66_0/libs/graph/doc/sloan_ordering.htm.
 sloanw2=WEIGHT2

Use WEIGHT2 as the second weight for the Sloan algorithm, see https://www.boost.org/doc/libs/1_66_0/libs/graph/doc/sloan_ordering.htm.
 graphmetrics

Print Boost’s and ViennaCL’s graph metrics (only available when LTSmin is compiled with Boost or ViennaCL).
 regroupexit

Exit with 0 when regrouping is done.
 regrouptime

Print timing information of each transformation, given in sequence regroup (r).
 mucalc=FILEFORMULA

Compute a parity game for the mucalculus formula.
The mucalculus formula is provided in the file FILE or directly as a string FORMULA. The syntax and tool support are described in ltsminmucalc(5).
 por=heurdel

Activate partialorder reduction
PartialOrder Reduction (POR) can reduce the state space when searching for deadlocks (
d
) or accepting cycles (ltl
). Two POR algorithms are available: heur

Uses a costbased heuristic beamsearch to find the smallest stubborn set
 del

Uses Valmari’s deletion algorithm to find the smallest stubborn set by iteratively removing transitions while maintaining the constraints.
 weak

Use weak commutativity in partialorder reduction. Possibly yielding better reductions.
 leap

Use leaping partialorder reduction, by combining several disjoint stubborn sets sequentially.
Environment Variables
LTSmin supports the following list of environment variables.
Name  Unit  Description 

LTSMIN_MEM_SIZE 
bytes 
Sets the amount of system memory to the given value. 
LTSMIN_NUM_CPUS 
constant 
Sets the amount of CPUs to the given value. 
The variables LTSMIN_MEM_SIZE, and LTSMIN_NUM_CPUS are particularly relevant when neither sysconf(3) nor cgroups(7) is able to properly detect these limits, e.g. when LTSmin runs on Travis CI in a docker container.
Symbolic Parity Game Options
A symbolic parity game can be generated either by using the mucalc
option or by using the PBES language module.
 pgsolve

Solve the generated parity game.
 pgreduce

Reduce the generated parity game onthefly (experimental).
 pgwrite=FILE

Writes a symbolic parity game to FILE.
Symbolic Parity Game Solver Options
 attr=defaultchainparpar2

Choose attractor function.
Available attractor functions:
 default

Straightforward attractor computation.
 chain

Chaining attractor, applies transition groups in a different order than default in computing an attractor level.
 par

Spawns parallel tasks to compute forward and backward steps for each attractor level.
 par2

Spawns more parallel tasks than par, by applying forward steps in parallel to the result of the backward steps of the different transition groups.
 saturatingattractor

Use saturation in the chaining attractor.
 pgwritedot

Write dot files to disk during parity game solving for debugging.
Vector Set Options
 vset=TYPE

Select type of vector set: ldd64, ldd, list, tree, fdd, ddd, sylvan, or lddmc. With ldd64, the 64bit ListDD list encoding is used (nonATerm based). With ldd, the 32bit ListDD list encoding is used (nonATerm 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. With sylvan, the parallel BDD package Sylvan is used. With lddmc, the parallel LDD package LDDmc is used. Defaults to first available type in the list.
 vsetcachediff=diff

Influences the size of operations cache when counting precisely with bignums: cache size = floor((2log(nodestocount) + <diff>)^2). More precisely; LTSmin will bitshift <diff> bits to the left or right on the number of nodes in the vector set, depending on the signedness of <diff>. The default is 0, meaning that if the cache is full the number of bignums in memory will be equal to the number of nodes in the vector set. The default value seems to work well, even when the number vectors in the vector set is very large relative to the number of nodes. If the number of vectors relative to the number of nodes is lower, <diff> may be decreased. The user may want to set <diff> as low as possible (to save memory), while keeping the operations cache effective. Bignums are not floating point numbers and may thus consume a lot of memory.
ListDD Options
 ldd32step=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.
 ldd32cache=DIFF

Set Fibonacci difference DIFF between the cache and nodes (DIFF may be negative). Defaults to 1.
ListDD Options
 lddstep=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.
 lddcache=DIFF

Set Fibonacci difference DIFF between the cache and nodes (DIFF may be negative). Defaults to 1.
BuDDy Options
 cacheratio=RATIO

Set cache ration. Defaults to 64.
 maxincrease=NUMBER

Set maximum increase. Defaults to 1,000,000.
 minfreenodes=PERCENTAGE

Sets the minimum percentage of free nodes as integer between 0 and 100. Defaults to 20.
 fddbits=BITS

Sets the number of bits for each FDD variable. Defaults to 16.
 fddreorder=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.
Sylvan Options
 sylvanthreads=NUMBER

Set number of workers. Defaults to 1.
*sylvandqsize Sets the size of the (static) task queue for work stealing in Wool to N. Defaults to 100000.
 sylvantablesize=NUMBER

Sets the size of the BDD table to 1<<N nodes. Defaults to 23. Maximum of 29.
 sylvancachesize=NUMBER

Set the size of the memoization table to 1<<N entries. Defaults to 23.
 sylvanbits=BITS

Sets the number of bits for each integer in the state vector. Defaults to 16.
 sylvangranularity=NUMBER

Controls memoization table usage. Only use the memoization table every 1/N BDD levels. Defaults to 1, i.e., always use the table.
LDDmc Options
 lddmctablesize=NUMBER

Sets the size of the BDD table to 1<<N nodes. Defaults to 23. Maximum of 29.
 lddmccachesize=NUMBER

Set the size of the memoization table to 1<<N entries. Defaults to 23.
Lace Options
 laceworkers=NUMBER

Set number of Lace workers (threads for parallelization). Defaults to the number of available cores if parallel algorithms are used, 1 otherwise.
 lacedqsize=NUMBER

Set length of Lace task queue. Defaults to 40960000.
 lacestacksize=NUMBER

Set size of program stack in kilo bytes. Defaults to 0, which means using the default stack size.
General Options
 v

Increase the level of verbosity
 q

Be quiet; do not print anything to the terminal.
 debug=<file.c>

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

Print version string of this tool.
 h, help

Print help text
 usage

Print short usage summary.
EXIT STATUS
 0

Successful termination.
 1

Counter example found.
 255

Some error occurred.
SUPPORT
Send questions, bug reports, comments and feature suggestions to the LTSmin Support Team.