NAME

       lpsconfcheck - mark confluent tau-summands of an LPS

SYNOPSIS

       lpsconfcheck [OPTION]... [INFILE [OUTFILE]]

DESCRIPTION

       Checks which tau-summands of the mCRL2 LPS in INFILE are confluent, marks them by renaming
       them to ctau, and write the result to OUTFILE. If INFILE is not present stdin is used.  If
       OUTFILE is not present, stdout is used.

OPTIONS

       OPTION can be any of the following:

       -a, --check-all
              check  the  confluence  of  tau-summands  regarding  all other summands, instead of
              continuing with the next tau-summand as soon as a summand is  encountered  that  is
              not confluent with the current tau-summand

       -c, --counter-example
              display  a  valuation for which the confluence condition does not hold, in case the
              encountered condition is neither a contradiction nor a tautolgy

       -g, --generate-invariants
              try to prove that the reduced confluence condition is an invariant of the  LPS,  in
              case the confluence condition is not a tautology

       -o, --induction
              apply induction on lists

       -iINVFILE, --invariant=INVFILE
              use  the  boolean  formula  (an  mCRL2  data expression of sort Bool) in INVFILE as
              invariant

       -n, --no-check
              do not check if the invariant holds before checking for for confluence

       -m, --no-marking
              do not mark the confluent tau-summands; since there are no changes made to the LPS,
              nothing is written to OUTFILE

       -pPREFIX, --print-dot=PREFIX
              save  a  .dot  file  of  the  resulting  BDD  in case two summands cannot be proven
              confluent; 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

       -sNUM, --summand=NUM
              eliminate or simplify the summand with number NUM only

       -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

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

lpsconfcheck mCRL2 toolset 201210.1 (ReleaNovember 2012                           LPSCONFCHECK(1)