SYNOPSIS

prom2torx [OPTION]… input.prom

DESCRIPTION

prom2torx provides access to a labelled transition system from a specification provided in input.prom via the TorX-Explorer textual interface on stdin and stdout. Specifications are compiled with SpinS from PROMELA input models.

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

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

--por

Activate partial order reduction

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

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.

255

Some error occurred.

SUPPORT

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

SEE ALSO