.\" Manual page for pbes2bool version 201409.0 (Release). .\" .\" Generated from pbes2bool --generate-man-page. .\" .TH PBES2BOOL "1" "September 2017" "pbes2bool mCRL2 toolset 201409.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-e\fR\fILEVEL\fR, \fB--erase\fR=\fILEVEL\fR use remove level LEVEL to remove bes variables \&'none\&' do not remove generated bes variables\&. This can lead to excessive usage of memory\&. (default) \&'some\&' remove generated bes variables that are not used, except if the right hand side of its equation is true or false\&. The rhss of variables must have to be recalculated, if encountered again, which is quite normal\&. \&'all\&' remove every bes variable that is not used anymore in any equation\&. This is quite memory efficient, but it can be very time consuming as the rhss of removed bes variables may have to be recalculated quite often\&. .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 \&'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-o\fR\fIFORMAT\fR, \fB--output\fR=\fIFORMAT\fR use output format FORMAT (this option is deprecated\&. Use the tool pbes2bes instead)\&. .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-z\fR\fISEARCH\fR, \fB--search\fR=\fISEARCH\fR use search strategy SEARCH: \&'breadth-first\&' Compute the right hand side of the boolean variables in a first come first served basis\&. This is comparable with a breadth-first search\&. This is good for generating counter examples\&. (default) \&'depth-first\&' Compute the right hand side of a boolean variables where the last generated variable is investigated first\&. This corresponds to a depth-first search\&. This can substantially outperform breadth-first search when the validity of a formula is determined after a larger depths\&. \&'b\&' Short hand for breadth-first\&. \&'d\&' Short hand for depth-first\&. .TP \fB-s\fR\fISTRAT\fR, \fB--strategy\fR=\fISTRAT\fR use substitution strategy STRAT: \&'0\&' Compute all boolean equations which can be reached from the initial state, without optimization\&. This is is the most data efficient option per generated equation\&. (default) \&'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-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 . .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 . There is NO WARRANTY, to the extent permitted by law. .SH "SEE ALSO" See also the manual at .