.\" Manual page for pbes2bool version 201202.0 (Release). .\"
.\" Generated from pbes2bool --generate-man-page. .\"
.TH PBES2BOOL "1" "April 2012" "pbes2bool mCRL2 toolset 201202.0 (Release)" "User Commands"
.SH NAME
pbes2bool \- Generate a BES from a PBES and solve it. 
.SH SYNOPSIS
.B pbes2bool
[\fIOPTION\fR]...[\fIINFILE\fR]
.SH DESCRIPTION
Solves (P)BES from INFILE. If INFILE is not present, stdin is used. 
.SH OPTIONS
.TP
\fIOPTION\fR can be any of the following:
.TP
\fB-c\fR, \fB--counter\fR
print at the end a tree labelled with instantiations of the left hand side of 
equations; this tree is an indication of how pbes2bool came to the validity or 
invalidity of the PBES
.TP
\fB-H\fR, \fB--hashtables\fR
use hashtables when substituting in bes equations, and translate internal 
expressions to binary decision diagrams (discouraged, due to performance)
.TP
\fB-i\fR\fIFORMAT\fR, \fB--in\fR=\fIFORMAT\fR
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
.TP
\fB-o\fR\fIFORMAT\fR, \fB--output\fR=\fIFORMAT\fR
use output format FORMAT (this option is deprecated\&. Use the tool pbes2bes 
instead)\&.

.TP
\fB-p\fR[\fINAME\fR], \fB--pbes-rewriter\fR[=\fINAME\fR]
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
.TP
\fB-r\fR\fINAME\fR, \fB--rewriter\fR=\fINAME\fR
use rewrite strategy NAME:
  \&'jitty\&' for jitty rewriting (default),
  \&'jittyc\&' for compiled jitty rewriting,
  \&'jittyp\&' for jitty rewriting with prover

.TP
\fB-s\fR\fISTRAT\fR, \fB--strategy\fR=\fISTRAT\fR
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
.TP
\fB--timings\fR[=\fIFILE\fR]
append timing measurements to FILE\&. Measurements are written to standard error 
if no FILE is provided
.TP
\fB-t\fR, \fB--tree\fR
store state in a tree (for memory efficiency)
.TP
\fB-u\fR, \fB--unused_data\fR
do not remove unused parts of the data specification
.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 Jan Friso Groote.
.SH "REPORTING BUGS"
Report bugs at <http://www.mcrl2.org/issuetracker>.
.SH COPYRIGHT
Copyright \(co 2012 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/mcrl2/wiki/index.php/User_manual/pbes2bool>.