symbolic_exploration

This tool uses a symbolic approach for PBES instantiation, based on the work of Tom Boshoven. It is highly experimental, and using it is not recommended.

Manual page for symbolic_exploration

Usage

symbolic_exploration   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and applies ??? normalization to it. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

-c , --clustered

generate a clustered PBES

-iFORMAT , --in=FORMAT

use input format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-I , --instantiate

instantiate the PBES

-O[NAME] , --optimize[=NAME]

simplify the PBES during the normalization (default true)

-oFORMAT , --out=FORMAT

use output format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

--timings[=FILE]

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

Standard options

-q , --quiet

do not display warning messages

-v , --verbose

display short intermediate messages

-d , --debug

display detailed intermediate messages

--log-level=LEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink; Tom Boshoven and Tim Willemse