lts2pbes reads a modal formula as well as a labelled transitions system in .lts, .aut or
.fsm format and generates a parameterised boolean equation system (PBES) of which the solution
of the initial variable indicates whether the
formula is valid in the initial state of the transition system. The generated PBES can be solved
using tools such as pbes2bool, pbessolve or pbespgsolve.
When the labelled transition file is of type .aut or .fsm, the information about data types and
actions is not available and must be provided explicitly using the
--mcrl2 flag. A .lts file contains such information.
When using particular formulas, for instance such as:
then the standard translation to PBESs can yield a very PBES which is very elaborate to generate and can
become large. This is due to the fact
that the subformula
<a.b.c.d.e.f.g.h> is translated into one PBES equation with a huge right hand side.
This right hand side essentially reflects for any state of the lts whether a trace
a.b.c.d.e.f.g.h is possible.
When using the flag
--preprocess-modal-operators the formula is first transformed into the equivalent
[true*]mu X1.<a>mu X2.<b>mu X3.<c>mu X4.<d>mu X5.<d>mu X6.<e>mu X7.<f>mu X8.<g>mu X9.<h>true
This formula replaces the single very large equation by 9 ones, where the right hand sides only contain the information whether a single action can be done. This is generally faster and yields a substantially smaller PBES.
The tool pbessolve is capable of generating a counter example in the form of labelled transition systems,
provided the PBES is generated
using lts2pbes (or lps2pbes) using the
--counter-example flag. The generated PBES is more complicated
and may be harder to solve. Yet, these counter examples are very helpful in determining whether formulas do
not hold. If formulas are valid, this flag can also be used to determine witnesses, i.e., evidence when formulas
are valid. The tool pbes2bool can generate counter examples without the use of this flag. These
counter-examples are solely based on the provided PBES and they must be manually be related to the original
lts2pbes [OPTION]... [INFILE [OUTFILE]]
Translates an LTS in INFILE and writes the resulting PBES to OUTFILE. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.
Command line options
add counter example equations to the generated PBES
use FILE as the data and action specification. FILE must be a .mcrl2 file which does not contain an init clause.
use the state formula from FILE
use FILE for the data and action specification. FILE must be a .lps file.
use FILE as the data and action specification for the LTS. FILE must be a .mcrl2 file.
use output format FORMAT:
BES in internal format
PBES in internal format
BES in PGSolver format
PBES in textual (mCRL2) format
insert dummy fixpoints in modal operators, which may lead to smaller PBESs
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
do not display warning messages
display short intermediate messages
display detailed intermediate messages
display intermediate messages up to and including level
display help information
display version information
display help information, including hidden and experimental options