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.
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:
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES 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:
besBES in internal format
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES 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 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