|
|
Changing default 'FORMAT' variables.
|
|
PBES2BES(1) User Commands PBES2BES(1) NAME
pbes2bes - Generate a BES from a PBES. SYNOPSIS
pbes2bes [OPTION]... [INFILE [OUTFILE]] DESCRIPTION
Reads the PBES from INFILE and writes an equivalent BES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used. OPTIONS
OPTION can be any of the following: -H, --hashtables use hashtables when substituting in bes equations, and translate internal expressions to binary decision diagrams (discouraged, due to performance) -iFORMAT, --in=FORMAT use input format FORMAT: 'pbes' PBES in internal format 'bes' BES in internal format 'cwi' BES in CWI format 'pgsolver' max-parity game in PGSolver format -oFORMAT, --out=FORMAT use output format FORMAT: 'pbes' PBES in internal format 'bes' BES in internal format (default) 'cwi' BES in CWI format 'pgsolver' max-parity game in PGSolver format -p[NAME], --pbes-rewriter[=NAME] use pbes rewrite strategy NAME: 'simplify' for simplification 'quantifier-all' for eliminating all quantifiers 'quantifier-finite' for eliminating finite quantifier variables 'pfnf' for rewriting into PFNF normal form -rNAME, --rewriter=NAME use rewrite strategy NAME: 'jitty' for jitty rewriting (default), 'jittyc' for compiled jitty rewriting, 'jittyp' for jitty rewriting with prover -sSTRAT, --strategy=STRAT use strategy STRAT (default '0'); 0) Compute all boolean equations which can be reached from the initial state, without optimization (default). This is is the most data efficient option per generated equation. 1) Optimize by immediately substituting the right hand sides for already investigated variables that are true or false when generating an expression. This is as memory efficient as 0. 2) In addition to 1, also substitute variables that are true or false into an already generated right hand side. This can mean that certain variables become unreachable (e.g. X0 in X0 and X1, when X1 becomes false, assuming X0 does not occur elsewhere. It will be maintained which variables have become unreachable as these do not have to be investigated. Depending on the PBES, this can reduce the size of the generated BES substantially but requires a larger memory footprint. 3) In addition to 2, investigate for generated variables whether they occur on a loop, such that they can be set to true or false, depending on the fixed point symbol. This can increase the time needed to generate an equation substantially --timings[=FILE] append timing measurements to FILE. Measurements are written to standard error if no FILE is provided -t, --tree store state in a tree (for memory efficiency) -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-level=LEVEL display intermediate messages up to and including level -h, --help display help information --version display version information AUTHOR
Written by Jan Friso Groote. REPORTING BUGS
Report bugs at <http://www.mcrl2.org/issuetracker>. COPYRIGHT
Copyright (C) 2012 Technische Universiteit Eindhoven. This is free software. You may redistribute copies of it under the terms of the Boost Software License <http://www.boost.org/LICENSE_1_0.txt>. There is NO WARRANTY, to the extent permitted by law. SEE ALSO
See also the manual at <http://www.mcrl2.org/mcrl2/wiki/index.php/User_manual/pbes2bes>. pbes2bes mCRL2 toolset 201202.0 (Release) April 2012 PBES2BES(1)
