xenial (1) lpsconfcheck.1.gz

Provided by: mcrl2_201409.0-1ubuntu1_amd64 bug

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 © 2014 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>.