NAME

       pbesconstelm - remove constant parameters from a PBES

SYNOPSIS

       pbesconstelm [OPTION]... [INFILE [OUTFILE]]

DESCRIPTION

       Reads  a  file  containing  a  PBES,  and applies constant parameter elimination to it. If
       OUTFILE is not present, standard output is used. If INFILE is not present, standard  input
       is used.

OPTIONS

       OPTION can be any of the following:

       -c, --compute-conditions
              compute propagation conditions

       -pNAME, --pbes-rewriter=NAME
              use   pbes   rewrite   strategy   NAME:  'simplify'  for  simplification  (default)
              'quantifier-all'  for   eliminating   all   quantifiers   'quantifier-finite'   for
              eliminating  finite quantifier variables 'pfnf' for rewriting into PFNF normal form
              'ppg' for rewriting into  Parameterised  Parity  Game  form  'bqnf-quantifier'  for
              rewriting quantifiers over conjuncts to conjuncts of quantifiers (experimental)

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

       -e, --remove-equations
              remove redundant equations

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

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

       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 Wieger Wesselink; Simon Janssen and Tim Willemse.

REPORTING BUGS

       Report bugs at <http://www.mcrl2.org/issuetracker>.

COPYRIGHT

       Copyright © 2012 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/pbesconstelm.html>.

pbesconstelm mCRL2 toolset 201210.1 (ReleaNovember 2012                           PBESCONSTELM(1)