Man Linux: Main Page and Category List


       lpsconfcheck - mark confluent tau-summands of an LPS


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


       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.


       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

       -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

       -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

       -rNAME, --rewriter=NAME
              use rewrite strategy NAME:
                ’jitty’ for jitty rewriting (default),
                ’jittyp’ for jitty rewriting with prover,
                ’jittyc’ for compiled jitty rewriting,
                ’inner’ for innermost rewriting,
                ’innerp’ for innermost rewriting with prover, or
                ’innerc’ for compiled innermost rewriting

       -zSOLVER, --smt-solver=SOLVER
              use SOLVER to remove inconsistent paths from the internally used
              BDDs (by default, no path elimination is applied):
                ’ario’ for the SMT solver Ario, or
                ’cvc’ for 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

       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

              display version information


       Written by Luc Engelen.


       Report bugs at <>.


       Copyright © 2010 Technische Universiteit Eindhoven.
       This  is  free  software.   You may redistribute copies of it under the
       terms        of        the        Boost        Software         License
       <>.   There  is NO WARRANTY, to the
       extent permitted by law.


       See             also             the             manual              at

lpsconfcheck mCRL2 toolset July 201Mayd2010opment)