1. 06 Jan, 2013 4 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Update with recent changes. · d02376aa
      Alexandre Duret-Lutz authored
      d02376aa
    • Alexandre Duret-Lutz's avatar
      Remove anything related to evtgba. · 254896d5
      Alexandre Duret-Lutz authored
      * src/evtgba/, src/evtgbaalgos/, src/evtgbaparse/, src/evtgbatest/:
      Delete.
      * src/Makefile.am (SUBDIRS): Adjust.
      * configure.ac, README: Adujst.
      254896d5
    • Alexandre Duret-Lutz's avatar
      bench: delete useless defs.in files. · 16c7bc19
      Alexandre Duret-Lutz authored
      * bench/wdba/defs.in, bench/ltlclasses/defs.in,
      bench/ltlcounter/defs.in: Delete.
      * bench/wdba/run, bench/ltlclasses/run, bench/ltlcounter/run: Adjust not
      to use them.
      * configure.ac: Do not output the associated defs files.
      16c7bc19
    • Alexandre Duret-Lutz's avatar
      Rewrite the ltl2tgba bench using ltlcross · 885a5351
      Alexandre Duret-Lutz authored
      * bench/ltl2tgba/sum.py: New file.
      * bench/ltl2tgba/.gitignore, bench/ltl2tgba/Makefile.am,
      bench/ltl2tgba/README, bench/ltl2tgba/algorithms, bench/ltl2tgba/big,
      bench/ltl2tgba/defs.in, bench/ltl2tgba/known, bench/ltl2tgba/small:
      Rewrite this benchmark completely.  Also drop support of Wring and
      Modella, as we cannot get them to work reliably.
      * bench/ltl2tgba/formulae.ltl: Rewrite in Spot's syntax.
      * bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
      bench/ltl2tgba/parseout.pl: Delete these scripts, no
      longer needed.
      * configure.ac: Do not output ltl2baw.pl anymore.
      885a5351
  2. 28 Dec, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Remove LBTT. · e2f17f65
      Alexandre Duret-Lutz authored
      * configure.ac: Detect lbtt using AC_CHECK_PROG.
      * m4/lbtt.m4: Delete.
      * lbtt/: Remove directory.
      * Makefile.am, README: Adjust.
      e2f17f65
  3. 24 Dec, 2012 4 commits
    • Alexandre Duret-Lutz's avatar
      Address several issues reported by cppcheck all over the place. · a577850e
      Alexandre Duret-Lutz authored
      * src/bin/common_finput.cc, src/tgbaalgos/lbtt.cc: Use !empty() instead
      of size() > 0.
      * src/bin/ltl2tgta.cc, src/kripke/kripkeexplicit.cc,
      src/tgbatest/complementation.cc: Avoid useless assignments.
      * src/bin/ltlcross.cc: Correct mistaken assignment inside assert().
      * src/evtgba/symbol.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh,
      src/tgba/tgbasafracomplement.cc (operator=): Do not return a const
      reference.
      * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/product.cc,
      src/evtgbatest/product.cc: Check indices before using them, not after.
      * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/tgbatest/randtgba.cc: Pass constant strings by reference.
      * src/kripke/kripkeprint.cc, src/tgbaalgos/simulation.cc:
      Remove a useless operation.
      * src/ltlvisit/simplify.cc: Remove a duplicate condition.
      * src/misc/formater.hh: Remove unused attribute.
      * src/misc/modgray.cc: Initialize done_ in the constructor.
      * src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh (operator=): Fix prototype.
      * src/saba/sabacomplementtgba.cc: Remove unused default constructor.
      * src/ta/taexplicit.cc, src/ta/taproduct.cc, src/ta/tgtaproduct.cc,
      src/ta/tgtaproduct.hh, src/taalgos/emptinessta.cc,
      src/taalgos/minimize.cc, src/taalgos/reachiter.cc,
      src/taalgos/tgba2ta.cc, src/tgbaalgos/cutscc.cc: Use C++ casts, and
      ++it instead of it++.
      * src/taalgos/dotty.cc, src/tgbatest/ltl2tgba.cc: Refine the scope of
      variables.
      * src/tgba/tgbakvcomplement.hh (bdd_order): Always initialize bdd_.
      * src/tgba/tgbasgba.cc, src/tgba/wdbacomp.cc: Use the initialization
      line to initialize all members.
      a577850e
    • Alexandre Duret-Lutz's avatar
      acccompl: Speed up. · a3b49f11
      Alexandre Duret-Lutz authored
      * src/misc/acccompl.cc: Simplify both directions of the conversion.
      * src/misc/acccompl.hh: Pass bdds by reference.
      a3b49f11
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      [buddy] · 15c9b72f
      Alexandre Duret-Lutz authored
      * src/bdd.h: Make all inplace operators return a reference.
      15c9b72f
  4. 19 Dec, 2012 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlast: use the return of insert() to avoid a double lookup · 13c41ee7
      Alexandre Duret-Lutz authored
      * src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
      src/ltlast/binop.cc, src/ltlast/bunop.cc,
      src/ltlast/multop.cc, src/ltlast/unop.cc: Do not look for a key
      and then insert the (key,value) on failure.  Simply insert
      (key,0), and replace 0 by value on failure.  This replaces two map
      lookups by one.
      13c41ee7
    • Alexandre Duret-Lutz's avatar
      More documentation. · 2776de87
      Alexandre Duret-Lutz authored
      * README: Introduce Spot, and point to the documentation.
      * wrap/python/ajax/README: Mention ltl3ba 1.0.2.
      2776de87
    • Alexandre Duret-Lutz's avatar
      Cosmetics. · aa2374c5
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Catch extra space around operator declarations.
      * src/ltlast/automatop.hh, src/ltlast/multop.hh,
      src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
      src/tgbaalgos/simulation.cc: Fix them.
      aa2374c5
  5. 14 Dec, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
      Remove useless variable. · cffbb7b4
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.hh (add_state): Remove useless variable.
      Reported by Étienne Renault.
      cffbb7b4
    • Alexandre Duret-Lutz's avatar
      x-to-1: Honor $PERL · b3d8b019
      Alexandre Duret-Lutz authored
      * tools/x-to-1.in: Run $HELP2MAN via $PERL so that the user gets a
      chance to use his preferred version of Perl.  This is typically
      required by Darwin users whose default /usr/bin/perl do not have all
      the libraries required by help2man, and who need to use their MacPorts
      installation of Perl instead.
      b3d8b019
  6. 28 Nov, 2012 3 commits
  7. 27 Nov, 2012 1 commit
  8. 14 Nov, 2012 2 commits
  9. 27 Oct, 2012 2 commits
  10. 26 Oct, 2012 3 commits
  11. 24 Oct, 2012 1 commit
  12. 23 Oct, 2012 2 commits
  13. 22 Oct, 2012 1 commit
  14. 21 Oct, 2012 3 commits
    • Alexandre Duret-Lutz's avatar
      rename ltlcheck as ltlcross · f3ef9de0
      Alexandre Duret-Lutz authored
      * src/bin/ltlcheck.cc, src/bin/man/ltlcheck.x,
      src/tgbatest/ltlcheck.test, src/tgbatest/ltlcheck2.test: Rename as ...
      * src/bin/ltlcross.cc, src/bin/man/ltlcross.x,
      src/tgbatest/ltlcross.test, src/tgbatest/ltlcross2.test: ... these.
      * NEWS, src/bin/Makefile.am, src/bin/man/Makefile.am,
      src/tgbatest/Makefile.am: Adjust.
      f3ef9de0
    • Alexandre Duret-Lutz's avatar
      tgbaexplicit: fix state_is_accepting() · fa4e6eff
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.hh (state_is_accepting): Use
      all_acceptance_conditions(), not all_acceptance_conditions_, so that
      it works even when all_acceptance_conditions_ is not ready.
      * src/tgbatest/explicit2.cc, src/tgbatest/explicit2.test: Adjust
      test case.
      fa4e6eff
    • Alexandre Duret-Lutz's avatar
      postproc: add the possibility to output a monitor · 76787b23
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a Monitor
      output option.
      * src/bin/ltl2tgba.cc: Add a --monitor/-M option.
      * NEWS: Mention monitors.
      * src/tgba/tgbaexplicit.hh (is_accepting_state): Fix for the
      case where the automaton has no acceptance set.
      76787b23
  15. 20 Oct, 2012 5 commits
  16. 19 Oct, 2012 3 commits
    • Alexandre Duret-Lutz's avatar
      bin: Adjust version display and help options. · b8ed85a3
      Alexandre Duret-Lutz authored
      In particular, this get rid of the ugly -? option that argp adds by
      default, and we also remove -V so that we can use it for something
      else later.
      
      * src/bin/common_setup.cc, src/bin/common_setup.hh (misc_argp):
      Provide support for --help/--version/--usage output, replacing argp's
      default builting version.
      * src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
      src/bin/ltlcheck.cc, src/bin/ltlfilt.cc, src/bin/randltl.cc:
      Call argp_parse() with ARGP_NO_HELP, and use misc_argp instead.
      b8ed85a3
    • Alexandre Duret-Lutz's avatar
      accconv: speed up acceptance_convertor::as_positive_product() · c6030df9
      Alexandre Duret-Lutz authored
      * src/misc/accconv.cc (as_positive_product): Use a small loop instead
      of calling bdd_satone().
      c6030df9
    • Alexandre Duret-Lutz's avatar
      tgbaexplicit: speed up merge_transitions() · 31fb3d9d
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.hh (merge_transitions): Use a hash table
      to merge compatible transitions.
      * src/tgbatest/readsave.test: Add a test case.
      31fb3d9d