.\" Manual page for pbespgsolve version 201409.0 (Release). .\"
.\" Generated from pbespgsolve --generate-man-page. .\"
.TH PBESPGSOLVE "1" "September 2017" "pbespgsolve mCRL2 toolset 201409.0 (Release)" "User Commands"
.SH NAME
pbespgsolve \- Solve a (P)BES or parity game using a parity game solver
.SH SYNOPSIS
.B pbespgsolve
[\fIOPTION\fR]... [\fIINFILE\fR]
.SH DESCRIPTION
Reads a file containing a (P)BES or a max parity game in PGSolver 
format,instantiates it into a BES, and applies a
parity game solver to it. If INFILE is not present, standard input is used.
.SH OPTIONS
.TP
\fIOPTION\fR can be any of the following:
.TP
\fB-C\fR, \fB--cycle\fR
Eliminate cycles
.TP
\fB-i\fR\fIFORMAT\fR, \fB--in\fR=\fIFORMAT\fR
use input format FORMAT:
\&'pbes\&' PBES in internal format
\&'pbes_text\&' PBES in internal textual format
\&'text\&' PBES in textual (mCRL2) format
\&'bes\&' BES in internal format
\&'bes_text\&' BES in internal textual format
\&'cwi\&' BES in CWI format
\&'pgsolver\&' BES in PGSolver format
.TP
\fB-L\fR, \fB--loop\fR
Eliminate self-loops
.TP
\fB-g\fR, \fB--onlygenerate\fR
Only generate the BES without solving
.TP
\fB-Q\fR\fINUM\fR, \fB--qlimit\fR=\fINUM\fR
limit enumeration of quantifiers to NUM variables\&. (Default NUM=1000, NUM=0 for 
unlimited)\&.
.TP
\fB-r\fR\fINAME\fR, \fB--rewriter\fR=\fINAME\fR
use rewrite strategy NAME:
\&'jitty\&' jitty rewriting (default)
\&'jittyc\&' compiled jitty rewriting
\&'jittyp\&' jitty rewriting with prover
.TP
\fB-c\fR, \fB--scc\fR
Use scc decomposition
.TP
\fB-s\fR\fINAME\fR, \fB--solver-type\fR=\fINAME\fR
Use the solver type NAME:
\&'spm\&' Small progress measures (default)
\&'altspm\&' Alternative implementation of small progress measures
\&'recursive\&' Recursive algorithm
.TP
\fB--timings\fR[=\fIFILE\fR]
append timing measurements to FILE\&. Measurements are written to standard error 
if no FILE is provided
.TP
\fB-e\fR, \fB--verify\fR
Verify the solution
.TP
Standard options:
.TP
\fB-q\fR, \fB--quiet\fR
do not display warning messages
.TP
\fB-v\fR, \fB--verbose\fR
display short intermediate messages
.TP
\fB-d\fR, \fB--debug\fR
display detailed intermediate messages
.TP
\fB--log-level\fR=\fILEVEL\fR
display intermediate messages up to and including level
.TP
\fB-h\fR, \fB--help\fR
display help information
.TP
\fB--version\fR
display version information

.SH AUTHOR
Written by Maks Verver and Wieger Wesselink; Michael Weber.
.SH "REPORTING BUGS"
Report bugs at <http://www.mcrl2.org/issuetracker>.
.SH COPYRIGHT
Copyright \(co 2014 Technische Universiteit Eindhoven.
.br
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.
.SH "SEE ALSO"
See also the manual at <http://www.mcrl2.org/release/user_manual/tools/pbespgsolve.html>.