SYNOPSIS

opaal2lts-mc [OPTION]… input<_.so|_.xml>

DESCRIPTION

opaal2lts-mc performs multi-core reachability on the labelled transition system from a compiled specification provided in input.xml or intput.so (precompiled).

https://code.launchpad.net/~opaal-developers/opaal/ opaal-ltsmin-succgen[opaal] is an open source implementation of the UPPAAL model checker. It was extended to generate successor generators for the LTSmin PINS interface. Therefore the PINS interface was extended to support the semi-symbolic states in timed automata. For more details on the multi-core timed-automata implementation, refer to Multi-Core Reachability for Timed Automata

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. TYPE can be one of the following options:

sbfs

explore state space in strict breadth-first order (default). Gives best result in the timed automata setting.

bfs

explore state space in breadth-first order.

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.

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

--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 table. In many cases the tree can compress states to two integers regardless of their length. To efficiently accommodate more than 4*10^9 states, the table is split in a root and a leaf table whose respective size can be adjusted using the --ratio option (default).

cleary-tree

use a lockless tree-compressed hash table with a parallel Cleary table to store roots. The compressed size of a state can approach one integer with this approach. The leafs table is stored as a standard tree table (two integers per subtree), which typically can be much smaller (up to the square root of the root table size). To control the respective size of the leaf table use the --ratio option.

--ratio=NUMBER

Log_2 ratio between root and leaf table in tree compression. The ratio can theoretically be as low as the square root of the root table size (see --size). This will however only work if the state vectors are perfectly combinatorial wrt their variable values. In most cases the leaf table will grow larger, but find found that a factor four (--ratio=2) works well for over 75% of the BEEM models. (default: NUMBER=2).

--size=NUMBER

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

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

--noref

Store full state vectors on queue/stack. This is usually a bit faster, but requires more memory. Incompatible with the swarmed algorithms.

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

-n, --no-exit

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=PREDFILE|PREDEXPRESSION

Find state where the invariant is violated. The file PREDFILE contains an expression in a simple predicate language (see ltsmin-pred(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 pretty-printed with ltsmin-printtrace(1).

-n, --no-exit

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=PREDFILE|PREDEXPRESSION

Find state where the invariant is violated. The file PREDFILE contains an expression in a simple predicate language (see ltsmin-pred(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 pretty-printed with ltsmin-printtrace(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 mu-calculus (--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 next-state function and memoizes the results. If the next-state function is expensive this will yield substantial speedups.

--pins-guards

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:

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

Over-approximate all must-write to may-write. May-write supports the copy (-) dependency.

r2+

Over-approximate read to read+write. Allows read dependencies to also subsume write dependencies.

w2+

Over-approximate must-write to read+write. Allows must-write dependencies to also subsume read dependencies.

W2+

Over-approximate may-write to read+write. Allows must-write dependencies to also subsume read dependencies.

rb4w

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

--mucalc=FILE|FORMULA

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

--ltl=LTLFILE|LTLFORMULA

Compute cross-product of a Buchi automaton and the specification

LTLFILE is a file containing an Linear Temporal Logic formula (see ltsmin-ltl(5)). Which content can also be provided directly as LTLFORMULA. 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|ltsmin

Change the semantics of the crossproduct generated using --ltl

Three options are available, the default is spin.

spin

Use semantics equal 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. Deadlocks in the LTS cause the Buchi to progress independently.

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. Deadlocks in the LTS do NOT cause the Buchi to progress independently.

ltsmin

Same as spin semantics, but now deadlocks in the LTS do NOT cause the Buchi to progress independently.

--por

Activate partial order reduction

Partial Order Reduction can reduce the state space when searching for deadlocks (-d) or accepting cycles (--ltl).

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

File Formats

The following file formats are supported:

  • Directory format (*.dir, *.dz and *.gcf)

  • Vector format (*.dir, *.gcd, *.gcf)

  • Binary Coded Graphs (*.bcg)

  • Aldebaran Format (*.aut)

  • FSM Format (*.fsm)

  • MRMC/Prism (*.tra+*.lab)

  • PGSolver format (*.pg)

If a tool operates in streaming mode then support for file formats is limited, as can be seen in the following table:

Format Streaming mode Load/Store mode

DIR

R/W

R/W

VEC

R/W

R/W

BCG

W

R/W

AUT

W

R/W

FSM

W

W

TRA

-

R/W

PG

-

W

The directory format uses multiple files to store an LTS. The various extension explain how these files are stored in the underlying file system. The *.dir format uses multiple files in a directory without compression. If the LTS has one edge label, no state labels and does not store state vectors then these files are backwards compatible. Neither the *.dz nor the *.gcf formats are backwards compatible. Both formats use compression. The first uses a directory for the files, second interleaves files into a single file.

If you try to open a *.dir with the old mCRL tools and you get the error message:

wrong file version: 0

then the directory is probably compressed. If that happens then you may convert the directory by typing the command:

ltsmin-convert bad.dir good.dir

LTL MODEL CHECKING

LTL model checking requires a Buchi cross product with accepting states marked with accepting state labels, and a search strategy which takes these labels into account (see ndfs / scc strategies of the sequential and multi-core tools).

For generating a cross product, the following options are supported:

  1. The input specification is already combined with a Buchi automaton, and states are appropriately marked with accepting labels. Currently two frontends support this functionality: SpinS (see documentation on prom tools), and DiVinE (see documentation on dve tools).

  2. LTSmin tools can build the cross product of input specification and Buchi automaton (through a PINS2PINS layer enabled with the --ltl option) themselves, and will annotate cross-product states appropriately when they are accepting. See also --labels option in the PINS tools.

Note
Combination with the Partial Order Reduction PINS2PINS layer (--por) requires the latter option.
Note
As of LTSmin release 1.9, our default LTL semantics mimics those of SPIN/DiVinE. Before that, LTSmin implemented textbook semantics. See the documentation on the enumerative tools for more information.

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.

SEE ALSO