NAME

       formulacheck - check a boolean formula

SYNOPSIS

       formulacheck [OPTION]... [INFILE]

DESCRIPTION

       Checks  whether  the  boolean  formula  (an  mCRL2 data expression of sort Bool) in INFILE
       holds. If INFILE is not present, stdin is used.

OPTIONS

       OPTION can be any of the following:

       -c, --counter-example
              display a valuation for which the formula does not hold, in case it  is  neither  a
              contradiction nor a tautology

       -o, --induction
              apply induction on lists

       -pPREFIX, --print-dot=PREFIX
              save  a .dot file of the resulting BDD if it is impossible to determine whether the
              formula is a contradiction or a tautology; PREFIX will be used  as  prefix  of  the
              output files

       -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

       -zSOLVER, --smt-solver=SOLVER
              use  SOLVER to remove inconsistent paths from the internally used BDDs (by default,
              no path elimination is applied): 'cvc' the SMT solver CVC3

       -sSPECFILE, --spec=SPECFILE
              check the formula against the data types from the LPS or PBES in SPECFILE

       -tLIMIT, --time-limit=LIMIT
              spend at most LIMIT seconds on proving a single formula

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

       -w, --witness
              display  a  valuation  for  which  the  formula  holds,  in  case  it  is neither a
              contradiction nor a tautology

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

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

formulacheck mCRL2 toolset 201210.1 (ReleaNovember 2012                           FORMULACHECK(1)