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
- -rNAME, --rewriter=NAME
- use rewrite strategy NAME:
'jitty' for jitty rewriting (default),
'jittyc' for compiled jitty rewriting,
'jittyp' for 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' for 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/mcrl2/wiki/index.php/User_manual/formulacheck>.