User manual/lps2lts

From MCRL2

< User manual(Redirected from User manual/Lps2lts)

Jump to: navigation, search

User manual

Tool manual pages

Contents

Generate an LTS from an LPS.

1 Synopsis
2 Short description
3 Options
4 Author
5 Reporting bugs

Synopsis

lps2lts [OPTION]... [INFILE [OUTFILE]]

Short description

The lps2lts tool generates a labelled transition system (LTS) from the linear process specification (LPS) in INFILE and saves the result to OUTFILE. If OUTFILE is not supplied, the LTS is not stored. If INFILE is not supplied, stdin is used.

The format of OUTFILE is determined by its extension (unless it is specified by an option). The supported formats are:

aut: for the Aldebaran format (CADP)
bcg: for the Binary Coded Graph format (CADP) (if BCG support is enabled)
dot: for the GraphViz format
fsm: for the Finite State Machine format
mcrl: for the mCRL SVC format
mcrl2: for the mCRL2 format (default)
svc: for the (generic) SVC format

If the jittyc rewriter is used, then the MCRL2_COMPILEREWRITER environment variable (default value: mcrl2compilerewriter) determines the script that compiles the rewriter, and MCRL2_COMPILEDIR (default value: '.') determines where temporary files are stored.

Note that lps2lts can deliver multiple transitions with the same label between any pair of states. If this is not desired, such transitions can be removed by applying a strong bisimulation reducton using for instance the tool ltsconvert.

Options

OPTION can be any of the following:

-aNAMES, --action=NAMES: Detect and report actions in the transition system that have action names from the list NAMES. This is for instance useful to find (or prove the absence) of an action error. The list NAMES is a comma separated list of action names. A message is printed for every occurrence of an action with action names in the list. With the -t flag traces towards these actions are generated.

-b[NUM], --bit-hash[=NUM]: Make use of bit hashing to store states and store at most NUM states. This means that instead of keeping a full record of all states that have been visited, a bit array is used that indicate whether or not a hash of a state has been seen before. Although this means that this option may cause states to be mistaken for others (because they are mapped to the same hash), it can be useful to explore very large LTSs that are otherwise not explorable. If NUM is not supplied, then approximately 200 million is taken (this corresponds to about 25MB of memory).

-c[NAME], --confluence[=NAME]: Apply on-the-fly confluence reduction where action NAME is considered to denote a confluent silent step. If NAME is not supplied, ctau is assumed to be the confluent silent step.

-D, --deadlock: Detect deadlocks (i.e. for every deadlock a message is printed). A deadlock is a state from which no transitions are possible.

-F, --divergence: Detect divergences. For every state with a divergence (=tau loop) a message is printed. The algorithm to detect the divergences is linear for every state, and so state space exploration becomes quadratic with this option on. State space exploration can become slow with this option.

--error-trace: If an error occurs during exploration, a trace to the state that could not be explored is saved to a trace file.

-fNAME, --state-format=NAME

Store state internally in format NAME:

vector: for a vector (fastest, default in older versions of the toolset)
tree: for a tree (for memory efficiency, default in toolset versions from autumn 2011)

--init_tsize=NUM: Set the initial size of the internally used hash tables. The default size is 10000.

-lNUM, --max=NUM: Explore at most NUM states. After exploring of NUM states lps2lts will stop, having generated a partial LTS.

--no-info: Do not add state information to OUTFILE. Without this option lps2lts adds state vector to the LTS. This option causes this information to be discarded and states are only indicated by a sequence number. Explicit state information is useful for visualisation purposes, for instance, but can cause the OUTFILE to grow considerably. Note that this option is implicit when writing in the AUT format.

-oFORMAT, --out=FORMAT: Use FORMAT as the output format.

-rNAME, --rewriter=NAME: Use rewrite strategy NAME. lps2lts uses a term rewriting engine to manipulate data terms of the LPS. The choice of the rewriter can have influence on the performance.

-sNAME, --strategy=NAME

Explore the state space using strategy NAME:

b, breadth: breadth-first search (default)
d, depth: depth-first search
r, random: random simulation

--suppress: in verbose mode, do not print progress messages indicating the number of visited states and transitions. For large state spaces the number of progress messages can be quite horrendous. This feature helps to suppress those. Other verbose messages, such as the total number of states explored, just remain visible.

-t[NUM], --trace[=NUM]: Write a shortest trace to each state that is reached with an action from NAMES from option --action or is a deadlock detected with --deadlock to a file. No more than NUM traces will be written. If NUM is not supplied the number of traces is unbounded.

For each trace that is to be written a unique file with extension .trc (trace) will be created containing a shortest trace from the initial state to the deadlock state. The traces can be pretty printed and converted to other formats using tracepp.

--todo-max=NUM: Keep at most NUM states in todo lists; this option is only relevant for breadth-first search with bithashing, where NUM is the maximum number of states per level, and for depth first, where NUM is the maximum depth.

-u, --unused-data: Do not remove unused parts of the data specification.

-yBOOL, --dummy=BOOL: Replace free variables in the LPS with dummy values based on the value of BOOL: yes (default) or no.

Standard options:

-q, --quiet: Do not display warning messages.

-v, --verbose: Display short intermediate messages. This includes detailed status of the generation process. Once a level (in terms of breadth-first search) is completed, a message stating this is printed. After exploration of every 1000 states the following information is printed: current level, states explored, transitions explored, states seen. A state is explored if all its outgoing transitions have been explored. A state is seen if (at least) one of the transitions leading to it has been explored.