SYNOPSIS

dve22lts-mc [OPTION]… input[.dve|.dve2C]

DESCRIPTION

dve22lts-mc generates a labelled transition system from a compiled specification provided in input.dve or input.dve2C (precompiled). It does this concurrently for any given number of threads.

DIVINE

Compile a DVE input model with divine:

divine compile -l input.dve

The command results in a compiled model input.dve2C.

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

--threads=NUMBER

Number of threads to use for state space exploration (default: NUMBER=NUM_CORES). Maximum is 64.

--strategy=TYPE

Select an exploration strategy. Two kinds of algorithms are available: LTL model checking and reachability. The multi-core LTL algorithms (Nested DFS) are implemented in a swarmed fashion, however with a shared state storage. On top of that, MCNDFS and ENDFS offer work sharing between threads and can deliver speedups for some models. Note that the LTL algorithms require buchi automata as input. Such a model can be provided directly by the language frontend, i.e., DiVinE property models are supported, or by the LTL layer (see --ltl). Note finally that strict reachability exploration orders are not guaranteed by the multi-core version. TYPE can be one of the following options:

bfs

explore state space in breadth-first order (default).

dfs

explore state space in relaxed depth-first order. Relaxed meaning that the inclusion check on the set of visited states is executed immediately after generating a state. This saves stack space and improves performance of the parallel reachability analysis.

ndfs

multi-core swarmed Nested Depth-First Search (Courcoubetis et al.).

nndfs

multi-core swarmed New Nested Depth-First Search (Schwoon, Esparza).

mcnndfs

Multi-Core Nested Depth-First Search (Laarman, Langerak, van de Pol, Weber, Wijs).

mcndfs

Idem. No difference with MCNNDFS. Multi-Core Nested Depth-First Search (Laarman, Langerak, van de Pol, Weber, Wijs).

endfs

Multi-Core Nested Depth-First Search by Evangelista er al. The algorithm has been adapted with the cyan color encoding and early cycle detection, as described in "Variations on Multi-Core Nested Depth-First Search" (Laarman, van de Pol). Note that ENDFS requires a repair procedure, NNDFS is chosen by default. Alternatives can be chosen by providing a list of strategies, for example: "endfs,mcndfs", yields the NMC-NDFS algorithm as described in the Variations paper (with load balancing). Finally, we also allow multiple levels of ENDFS to be combined: "endfs,endfs,nndfs".

--nar

No All Red. Turn off all-red optimization in NNDFS/MCNDFS.

--perm=TYPE

Select the transition permutation, which is used to guide different threads to different parts of the state space. A good permutation can significantly speed up bug hunting. TYPE can be one of the following options, each has different properties in terms of performance and effectiveness summarized as (perf./eff.) :

dynamic

use "fresh successor heuristics" described in "Variations on Multi-Core Nested Depth-First Search" (Laarman, van de Pol). (decent/very good for bug hunting). Default for LTL.

sort

sort on the unique id of the successor state (decent/good)

random

use multiple fixed random permutation schemes per worker (decent/good).

rr

randomized using a full random sort order on the states. This is more random than the previous option, but requires more pre-computation time for the random array (decent/almost perfect).

sr

sort according to one fixed random permutation scheme per worker (decent/decent).

shift

shift the order of transitions by a fixed value per worker (fast/decent).

shiftall

as shift, but with a equal load for all workers (a bit slower/decent).

otf

sort according to a dynamic permutation scheme (slow/perfect).

none

use the same exploration order for all workers. Default for reachability.

--no-red-perm

Turns the permutation layer of for the nested DFSs of the swarmed algorithms.

--state=TYPE

Select type of data structure for storing visited states. TYPE can be one of the following options:

table

use a lockless hash table.

tree

use a lockless tree-compressed hash table (default).

--size=NUMBER

Log_2 hash table size in elements (default: NUMBER=24). This is also used for the internal node table of the tree.

--lb=TYPE

Select load-balancing strategy. TYPE can be one of the following options:

srp

synchronous random polling.

static

initial BFS run, with static hand-off to all threads.

combined

Starts with static balancing and moves to SRP when needed (default).

none

turn load balancer off. Default for swarmed algorithms, for which threads in principle explore the state space independently (see --strategy).

--handoff=NUMBER

Maximum number of states to hand off to a thread requesting load (default: NUMBER=100). The operation may be expensive, depending on the size of the states.

--gran=NUMBER

Granularity at which control is handed back to the load balancer (default: NUMBER=100). Higher values may reduce runtime overhead, but decrease the performance of the load balancer. The state space explorer uses the number of transitions as work counter.

--ref

Save space by storing references to table/tree on the stack/queue. Normally full states are stored. The swarmed algorithms always use references.

--zobrist=NUMBER

Save time by using zobrist incremental state hashing. NUMBER defines the (log_2) size of the random number table (default: 0=OFF). Large tables mean better hash distributions, but more cache misses due to memory size. Experiments have shown that small tables (2^6) suffice for good distributions (equal or better than Jenkin’s hash). Improvements are only noticable for fast state generators, like DiVinE 2.2 (dve22lts-mc(1)).

--max=NUMBER

Maximum search depth.

-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).

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.

Development Options

--grey

Make use of GetTransitionsLong calls.

A language module can have three next state calls: GetTransitionsAll, GetTransitionsLong and GetTransitionsShort. The first call is used by default, the second call is used when this flag is passed and the third form is used if --cache is enabled. This allows all three calls in a language module to be tested.

--write-state

Write the full state vector.

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.

SEE ALSO

ltsmin(7), ltsmin-tracepp(1), etf(5), NIPS, DiVinE-cluster, DiVinE-2.2,