NAME

       pbes2bes - Generate a BES from a PBES.

SYNOPSIS

       pbes2bes [OPTION]... [INFILE [OUTFILE]]

DESCRIPTION

       Reads  the  PBES  from  INFILE  and  writes an equivalent BES to OUTFILE. If INFILE is not
       present, stdin is used. If OUTFILE is not present, stdout is used.

OPTIONS

       OPTION can be any of the following:

       -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, --out=FORMAT
              use  output  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

       -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/pbes2bes.html>.