lps2lts

The tool lps2lts generates a labelled transition system from a linear process (with extension .lps). While doing so, various checks can be performed, such as checks for deadlock, livelock, and the presence of certain actions.

The generated transition system can be saved in various formats (.aut, .lts, .fsm and .dot). Generally not saving, or saving in .aut format is the fastest, but it only contains information about transitions. The .lts format has the advantage that all information about the transition system is included, including data types, action declarations and state information. It is however not human readable. The .fsm format contains transition and state information, and is human readable.

A typical use of lps2lts is as follows:

lps2lts --verbose infile.lps outfile.aut

This automatically generates the file in .aut format. If no outfile is given, the transition system will be generated but not saved. The flag –verbose is the verbose flag, such that lps2lts gives some information about progress.

The labelled transition systems can be inspected using graphical tools like ltsgraph, ltsview and diagraphica. Using the tool ltsconvert the transition systems can be reduced modulo behavioural equivalences. Other tools allow to compare labelled transition systems ltsconvert, verify modal formulas lts2pbes, etc.

There are options to search for particular action labels, multi-actions with data, deadlocks and livelocks. The –trace option instructs the tool to save (a limited number) of traces to such states. Only one trace per state is saved. If the trace count is reached lps2lts stops. As a typical example, searching for an error action, saving one state and stop, can be done as follows:

lps2lts --verbose --action=error --trace=1 infile.lps

Generating a labelled transition system can be quite time consuming. Choosing the compiling rewriter using the –rewriter=jittyc can speed up the generation with a factor 10. The compiling rewriter is not available on all platforms. The use of the flag –cached may also have a dramatic influence on the generation speed, at the expense of using more memory. It caches the results of evaluating conditions in each summand in the linear process.

There are several options to traverse the state space. Default is breadth-first. But depth-first, random, and prioritised are also possible. Of special note is highway search [EGWW09]. When exploring the state space there is a stack of encountered states not yet explored. Using:

lps2lts --verbose --todo-max=100000 --action=error infile.lps

the size of this stack is limited to in this case 100000 states. If the stack exceeds this size additional states are randomly ignored. High way search does not guarantee that all states are seen, but it an effective way to explore a state space, far more effective than random simulation.

When the linear process has confluent tau actions (which can be proven using the tool lpsconfcheck) then the flag –confluent generates a state space giving priority to confluent tau’s [GM14]. In certain cases this can give an exponential reduction. The confluent tau is by default called ctau.

When generating the transition system is taking too much time, the generation can be aborted. lps2lts will attempt to save the transition system before terminating. Using the flag –max the size of the state space can also be limited a priori.

Warning

Generation of an labelled transition system typically fails when

  • The rewrite system is not terminating. A typical non terminating rewrite rule is eqn f(x) = if(x==0, 0, f(x-1)); as f can infinitely be rewritten. Use conditions in rewrite rules to avoid this. Non terminating rewrite systems lead to an overflow of the stack and a subsequent crash of lps2lts.
  • There are sums over infinite domains in the linear process. E.g. having a summand sum x:Nat. a(x).X will cause the tool to enumerate all natural numbers first, filling up all the memory, not generating any transition.
  • The size of the state space is large as some process process parameters can attain an infinite or large amount of different values. An effective way to figure this out is to generate part of the transition system in a .fsm file. At the beginning of this file all process parameters and all the values that they got in some state are listed.

[EGWW09] T.A.N. Engels, J.F. Groote, M.J. van Weerdenburg and T.A.C. Willemse. Search algorithms for automated validation. Journal of Logic and Algebraic Programming 78(4), 274-287, 2009.

[GM14] J.F. Groote and M.R. Mousavi. Modeling and analysis of communicating systems. The MIT Press 2014.

Manual page for lps2lts

Usage

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

Description

Generate an LTS from the LPS in INFILE and save the result to OUTFILE. If INFILE is not supplied, stdin is used. If OUTFILE is not supplied, the LTS is not stored.

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 betweenany pair of states. If this is not desired, such transitions can be removed byapplying a strong bisimulation reducton using for instance the tool ltsconvert.

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), ‘dot’ for the GraphViz format (no longer supported as input format), ‘fsm’ for the Finite State Machine format, or ‘lts’ for the mCRL2 LTS 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.

Command line options

-aNAMES , --actionNAMES

report whether an action from NAMES occurs in the transitions system, where NAMES is a comma-separated list. A message is printed for every occurrence of one of these action names. With the -t flag traces towards these actions are generated. When using -tN only N traces are generated after which the generation of the state space stops.

-b[NUM] , --bit-hash[NUM]

use 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. The default value for NUM is 2*10^8 (this corresponds to 25MB of memory).

--cached

use enumeration caching techniques to speed up state space generation.

-c[NAME] , --confluence[NAME]

apply prioritization of transitions with the action label NAME. (when no NAME is supplied (i.e., ‘-c’) priority is given to the action ‘ctau’. To give priority to to tau use the flag -ctau. Note that if the linear process is not tau-confluent, the generated state space is necessarily branching bisimilar to the state space of the lps. The generation algorithm that is used does not require the linear process to be tau convergent.

-D , --deadlock

detect deadlocks (i.e. for every deadlock a message is printed).

-F , --divergence

detect divergences (i.e. for every state with a divergence (=tau loop) a message is printed). The algorithm to detect the divergences is linear for every state, so state space exploration becomes quadratic with this option on, causing a state space exploration to become slow when this option is enabled.

-yBOOL , --dummyBOOL

replace free variables in the LPS with dummy values based on the value of BOOL: ‘yes’ (default) or ‘no’.

--error-trace

if an error occurs during exploration, save a trace to the state that could not be explored.

--init-tsizeNUM

set the initial size of the internally used hash tables (default is 10000).

-lNUM , --maxNUM

explore at most NUM states

-mNAMES , --multiactionNAMES

detect and report multiactions in the transitions system from NAMES, a comma-separated list. Works like -a, except that multi-actions are matched exactly, including data parameters.

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

-n , --nondeterminism

detect nondeterministic states, i.e. states with outgoing transitions with the same label to different states.

-oFORMAT , --outFORMAT

save the output in the specified FORMAT.

--prune

use summand pruning to speed up state space generation.

-QNUM , --qlimitNUM

limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for unlimited).

-rNAME , --rewriterNAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-sNAME , --strategyNAME

explore the state space using strategy NAME:

b, breadth

breadth-first search

d, depth

depth-first search

p, prioritized

prioritize single actions on its first argument being of sort Nat where only those actions with the lowest value for this parameter are selected. E.g. if there are actions a(3) and b(4), a(3) remains and b(4) is skipped. Actions without a first parameter of sort Nat and multactions with more than one action are always chosen (option is experimental)

q, rprioritized

prioritize actions on its first argument being of sort Nat (see option –prioritized), and randomly select one of these to obtain a prioritized random simulation (option is experimental)

r, random

random simulation. Out of all next states one is chosen at random independently of whether this state has already been observed. Consequently, random simultation only terminates when a deadlocked state is encountered.

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

--tauACTNAMES

consider actions with a name in the comma separated list ACTNAMES to be internal. This list is only used and allowed when searching for divergencies.

--timings[FILE]

append timing measurements to FILE. Measurements are written to standard error if no FILE is provided

--todo-maxNUM

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

-t[NUM] , --trace[NUM]

Write a shortest trace to each state that is reached with an action from NAMES with the option –action, is a deadlock with the option –deadlock, is nondeterministic with the option –nondeterminism, or is a divergence with the option –divergence 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.

-u , --unused-data

do not remove unused parts of the data specification.

Standard options

-q , --quiet

do not display warning messages

-v , --verbose

display short intermediate messages

-d , --debug

display detailed intermediate messages

--log-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Muck van Weerdenburg