User manual/formulacheck

From MCRL2

Check a boolean formula.

Contents 1 Synopsis 2 Short description 3 Example of use 4 Options 5 Author 6 Bug reporting

Synopsis

formulacheck [OPTION]... [INFILE]

Short description

The formulacheck tool checks the boolean formula (an mCRL2 data expression of sort Bool) in INFILE. If INFILE is not present, stdin is used.

The tool indicates whether or not the formula is a tautology or a contradiction.

In some cases, the tool is unable to determine whether a formula is a tautology or a contradiction. The option --verbose gives insight into what the prover used by the tool is doing and can be used to see if rewrite rules have to be added to the specification in order to enable the prover to determine that certain formulas are indeed tautologies or contradictions.

A BDD based prover is used to the check the formula. In some cases it may be useful to use an SMT solver to assist the prover. The SMT solver can further reduce BDDs by removing inconsistent paths. A specific SMT solver can be chosen using the option --smt-solver=SOLVER. Either the SMT solver Ario or CVC3 can be used. To use one of these solvers, the directory containing the corresponding executable must be in the path.

Example of use

The input file typically contains a single expression such as

 3+3<4

When formulacheck would be applied to this file it would respond with

'3 + 3 < 4': Contradiction

If the input formula holds, the following output would be

'#[4, 5, 6] > 2': Tautology

If the input contains an expression which cannot be rewritten to true or false the response is

'[1, 4, 7]': Undeterminable

It is not possible to use formulacheck for open terms. For this the interactive tool mcrl2i is more convenient.

Options

OPTION can be any of the following:

-c, --counter-example

display a valuation for which the formula does not hold, in case the current formula 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 a formula is a contradiction or a tautology; PREFIX will be used as prefix of the output files

-rNAME, --rewrite-strategy=NAME

use rewrite strategy NAME

-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 the formula

-w, --witness

display a valuation for which the formula holds, in case the current formula is neither a contradiction nor a tautology

-zSOLVER, --smt-solver=SOLVER

use SOLVER to remove inconsistent paths from the internally used BDDs:

• 'ario': the SMT solver Ario
• 'cvc': the SMT solver CVC3

by default, no path elimination is applied

Standard options:

-q, --quiet

do not display warning messages

-v, --verbose

display short intermediate messages

-d, --debug

display detailed intermediate messages

-h, --help

display help information

--version

display version information

Author

Written by Luc Engelen.

Bug reporting

Report bugs at our issue tracking system.