NAME

       pbes2bool - Generate a BES from a PBES and solve it.

SYNOPSIS

       pbes2bool [OPTION]...[INFILE]

DESCRIPTION

       Solves (P)BES from INFILE. If INFILE is not present, stdin is used.

OPTIONS

       OPTION can be any of the following:

       -c, --counter
              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

       -eLEVEL, --erase=LEVEL
              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.

       -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 '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

       -oFORMAT, --output=FORMAT
              use output format  FORMAT  (this  option  is  deprecated.  Use  the  tool  pbes2bes
              instead).

       -QNUM, --qlimit=NUM
              limit  enumeration  of  quantifiers  to NUM variables. (Default NUM=1000, NUM=0 for
              unlimited).

       -rNAME, --rewriter=NAME
              use rewrite strategy NAME: 'jitty'  jitty  rewriting  (default)  'jittyc'  compiled
              jitty rewriting 'jittyp' jitty rewriting with prover

       -zSEARCH, --search=SEARCH
              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.

       -sSTRAT, --strategy=STRAT
              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.

       --timings[=FILE]
              append  timing  measurements to FILE. Measurements are written to standard error if
              no FILE is provided

       -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 © 2014 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/release/user_manual/tools/pbes2bool.html>.