xenial (1) pbes2bool.1.gz

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