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

pbes2bool mCRL2 toolset 201409.0 (Release)        November 2017                                     PBES2BOOL(1)