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.
- orphan:
Usage
lps2lts [OPTION]... [INFILE [OUTFILE]]
Description
Transforms the LPS in INFILE and writes a corresponding LTS to OUTFILE. If OUTFILE is not present or ‘-’ and an output format is specified, stdout is used. If INFILE is not present or ‘-’, stdin is used.
Command line options
-aNAMES , --action=NAMES
report actions in the transition system that occur in the comma-separated list of action names NAMES. The flag –trace can be used to generate traces to these actions.
--cached
use enumeration caching techniques to speed up state space generation.
-c[NAME] , --confluence[=NAME]
apply prioritization of transitions with the action label NAME (default ‘ctau’). To give priority to tau use the flag -ctau. Only if the linear process is tau-confluent, the generated state space is 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
report deadlocks (i.e. states with no outgoing transitions). The flag –trace can be used to generate traces to these deadlocks.
-F , --divergence
report divergences (i.e. states with a tau loop). The algorithm to detect divergences is linear for every state, so state space exploration becomes quadratic with this option enabled.The flag –trace can be used to generate traces to these divergences.
-lNUM , --max=NUM
explore at most NUM states
-mNAMES , --multiaction=NAMES
report occurrences of multi-actions in the transition system that occur in the comma-separated list of actions NAMES. Works like –action, except that multi-actions are matched exactly, including data parameters. The flag –trace can be used to generate traces to these multi-actions.
--no-info
do not add state label information to OUTFILE. This option only applies to .lts files.
--no-probability-checking
do not check if probabilities in stochastic specifications have sensible values
-n , --nondeterminism
report nondeterministic states, i.e. states with outgoing transitions with the same label to different states. The flag –trace can be used to generate traces to these nondeterministic states.
-oFORMAT , --out=FORMAT
save the output in the specified FORMAT.
-QNUM , --qlimit=NUM
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
-rNAME , --rewriter=NAME
use rewrite strategy NAME:
jittyjitty rewriting
jittyccompiled jitty rewriting
jittypjitty rewriting with prover
--save-at-end
delay saving of the generated LTS until the end. This option only applies to .aut and .lts files, which are by default saved on the fly.
-sNAME , --strategy=NAME
explore the state space using strategy NAME:
b,breadthbreadth-first search
d,depthdepth-first search
h,highwayhighway search. Only part of the state space is explored, by restricting the size of the todo list. N.B. The implementation deviates slightly from the published version.
--suppress
in verbose mode, do not print progress messages indicating the number of visited states and transitions.
--tau=NAMES
consider actions that occur in the comma-separated list of action names NAMES to be internal. This setting only affects the option –divergence.
--threads=NUM
run with NUM threads (default=1). With multiple threads the stack size on a Mac is limited which can lead to bus errors.
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
--todo-max=NUM
keep at most NUM states in the todo list; this option is only relevant for highway search, where NUM is the maximum number of states per level per thread.
-t[NUM] , --trace[=NUM]
write a trace to states that are reported using one of the flags –action, –deadlock, –divergence, –multiaction or –nondeterminism. After NUM traces have been written state space generation stops. If NUM is not supplied the number of traces is not limited. For each trace a unique file with extension .trc (trace) will be created containing a shortest trace starting from the initial state. The traces can be pretty printed and converted to other formats using tracepp. If the maximum amount of traces has been reached, state space generation is aborted. There is no guarantee that the traces are fully contained in the partial state space.
Standard options
-q , --quiet
do not display warning messages
-v , --verbose
display short log messages
-d , --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h , --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options