SYNOPSIS

prom2lts-seq [OPTION]… input.prom [output.fmt]

DESCRIPTION

prom2lts-seq generates a labelled transition system from a specification provided in input.prom by enumerative reachability analysis using a general state expanding algorithm. output.fmt specifies the name of the output archive. The desired format is deduced from the filename extension. Available formats are described below.

SpinS

Use SpinS (distributed as submodule LTSmin) to compile PROMELA model leader.pm to leader.pm.spins:

spins -o3 leader.pm

The optional flag -o3 turns off control flow optimizations.

On the resulting compiled SpinS module, all SpinS-related LTSmin tools can be used:

prom2lts-sym -rgs --order=chain leader.pm.spins leader.etf
prom2lts-mc --assert -prr --threads=16 leader.pm.spins
prom2lts-seq --por -d --trace=t.gcf leader.pm.spins

These three examples perform: full symbolic reachability with chaining order (--order) and reordering (-rgs) storing the state space in ETF format, doing a randomized (-prr) parallel (--threads) search for assertion violations (--assert) in the model, and searching for deadlocks (-d) storing the first counter example in t.gcf (--trace).

If a never claim is present in the model, a Buchi automaton is created. LTSmin can directly perform LTL model checking on such models:

prom2lts-mc --strategy=cndfs --threads=16 leader-never.pm.spins
prom2lts-seq --por --proviso=color --strategy=scc leader-never.pm.spins

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.

See the man pages of the respective tools for further options.

Note
SpinS is an adaptation of the SpinJa model checker, which generates C code implementing the PINS interface instead of Java code.

OPTIONS

--strategy=TYPE

Select exploration strategy. TYPE can be one of the following options:

bfs

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

dfs

explore state space in depth-first order.

scc

perform LTL model checking based on Buchi automata with Couvreur’s algorithm (accepting cycle detection). This requires an accepting state label to be present. See below.

--state=TYPE

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

tree

use a tree-compressed hash table (default).

table

use a hash table.

vset

use a vector set (decision diagram).

--max=DEPTH

Maximum search depth, search until DEPTH.

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

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

--allow-undefined-edges

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

--allow-undefined-values

Allow undefined values in atomic predicates for enums.

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

-2r

Over-approximate 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:

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

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

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

  4. 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 Cuthill-McKee ordering.

bk

Apply Boost’s King ordering.

bs

Apply Boost’s Sloan ordering.

vcm

Apply ViennaCL’s Cuthill-McKee ordering.

vacm

Apply ViennaCL’s advanced Cuthill-McKee ordering.

vgps

Apply ViennaCl’s Gibbs-Poole-Stockmeyer ordering.

f

Apply FORCE ordering.

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

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

--col-ins=PAIRS

Insert columns before other columns in the dependency matrix.

PAIRS is a comma-separated sequence of pairs <(C.C,)+>'. E.g. --col-ins=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 --col-ins=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 --col-ins 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.

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

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

--graph-metrics

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

--regroup-exit

Exit with 0 when regrouping is done.

--regroup-time

Print timing information of each transformation, given in sequence --regroup (-r).

--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 automatically chosen based on the atomic predicates in the formula.

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. This option is incompatible with edge-based atomic predicates. This option is the default if no edge-based atomic predicates are found in the LTL formula.

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. This option is incompatible with edge-based atomic predicates.

ltsmin

Same as spin semantics, but now deadlocks in the LTS do NOT cause the Buchi to progress independently. This option is the default if edge-based atomic predicates are found in the LTL formula.

--por=heur|del

Activate partial-order reduction

Partial-Order Reduction (POR) can reduce the state space when searching for deadlocks (-d) or accepting cycles (--ltl). Two POR algorithms are available:

heur

Uses a cost-based heuristic beam-search 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 partial-order reduction. Possibly yielding better reductions.

--leap

Use leaping partial-order reduction, by combining several disjoint stubborn sets sequentially.

Environment Variables

LTSmin supports the following list of environment variables.

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

Vector Set Options

--vset=TYPE

Select type of vector set: ldd64, ldd, list, tree, fdd, ddd, sylvan, or lddmc. With ldd64, the 64-bit ListDD list encoding is used (non-ATerm based). With ldd, the 32-bit ListDD list encoding is used (non-ATerm 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.

vset-cache-diff=diff

Influences the size of operations cache when counting precisely with bignums: cache size = floor((2log(nodes-to-count) + <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

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

--ldd32-cache=DIFF

Set Fibonacci difference DIFF between the cache and nodes (DIFF may be negative). Defaults to 1.

ListDD Options

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

--ldd-cache=DIFF

Set Fibonacci difference DIFF between the cache and nodes (DIFF may be negative). Defaults to 1.

BuDDy Options

--cache-ratio=RATIO

Set cache ration. Defaults to 64.

--max-increase=NUMBER

Set maximum increase. Defaults to 1,000,000.

--min-free-nodes=PERCENTAGE

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

--fdd-bits=BITS

Sets the number of bits for each FDD variable. Defaults to 16.

--fdd-reorder=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

--sylvan-threads=NUMBER

Set number of workers. Defaults to 1.

*--sylvan-dqsize Sets the size of the (static) task queue for work stealing in Wool to N. Defaults to 100000.

--sylvan-tablesize=NUMBER

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

--sylvan-cachesize=NUMBER

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

--sylvan-bits=BITS

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

--sylvan-granularity=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

--lddmc-tablesize=NUMBER

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

--lddmc-cachesize=NUMBER

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

Lace Options

--lace-workers=NUMBER

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

--lace-dqsize=NUMBER

Set length of Lace task queue. Defaults to 40960000.

--lace-stacksize=NUMBER

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

LTS I/O Options

--block-size=BYTES

Size of a block in bytes. Defaults to 32,768.

--cluster-size=BLOCKS

Number of blocks in a cluster. Defaults to 32.

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