prom2lts-sym [OPTION]… input.prom [output.etf]


prom2lts-sym performs a reachability analysis on a specification provided in input.prom. Specifications are compiled with SpinS from PROMELA input models. output.etf specifies the name of the output archive, written in etf(5) format.


Use SpinS (distributed as submodule LTSmin) to compile PROMELA model to

spins -o3

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.etf
prom2lts-mc --assert -prr --threads=16
prom2lts-seq --por -d --trace=t.gcf

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
prom2lts-seq --por --proviso=color --strategy=scc

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.

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



Select the exploration strategy: bfs-prev, bfs, chain-prev, or chain. With bfs-prev and bfs, breadth-first search is used. Here, bfs-prev only considers the states found at the previous level, while bfs considers the whole visited set. With chain-prev and chain, a chaining strategy is used. Here, chain-prev at each level starts from the states found at the previous level, while chain uses the whole visited set. Defaults to bfs-prev.

When using breadth-first 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 next-state for the second group to the result, etc. Thus, a chaining analysis can be completed in much less iterations than a BFS analysis.


Select a saturation strategy: none, sat-like, sat-loop, sat-fix, sat. The sat-like strategy goes up and down the levels of the BDD used to represent the state space. The sat-loop strategy loops over the levels. The sat-fix strategy repeatedly performs a fixpoint computation using saturation. The sat strategy does saturation as described in the literature with on-the-fly expansion of the transition relations. Defaults to none, i.e. no saturation.

All strategies except sat-fix and sat work in combination with the order to saturate levels.


Select the granularity of sat-like and sat-loop strategies. The granularity indicates how many BDD levels are considered at the same time. Defaults to 10.


Save the previous states seen at saturation levels. This option has effect for any of the saturation strategies in combination with either bfs-prev or chain-prev.


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.


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:

  1. current-l<L>.dot: the nodes in the vector set at level L (and only level L),

  2. visited-l<L>.dot: the nodes in the vector set up to and included level L,

  3. group_next-l<L>-k<K>.dot: the nodes in the transition relation of group K at level L.


After computing all reachable states, evaluate the mu-formula in MUFILE

MUFILE is a file containing a Mu Calculus formula (see ltsmin-mu(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.


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


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


When using --pins-guards=assume-true 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 guard-splitting.

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


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.


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


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

Symbolic Parity Game Options

A symbolic parity game can be generated either by using the --mucalc option or by using the PBES language module.


Solve the generated parity game.


Reduce the generated parity game on-the-fly (experimental).


Writes a symbolic parity game to FILE.

Symbolic Parity Game Solver Options


Choose attractor function.

Available attractor functions:


Straightforward attractor computation.


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


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


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


Use saturation in the chaining attractor.


Write dot files to disk during parity game solving for debugging.

Vector Set Options


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.

ListDD Options


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.


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

ListDD Options


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.


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

BuDDy Options


Set cache ration. Defaults to 64.


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


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


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


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


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.


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


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


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


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


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


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

Lace Options


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


Set length of Lace task queue. Defaults to 40960000.


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

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.


Counter example found.


Some error occurred.


Send questions, bug reports, comments and feature suggestions to the LTSmin Support Team.