1. 05 Nov, 2004 1 commit
  2. 04 Nov, 2004 3 commits
  3. 03 Nov, 2004 3 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh, · 76884314
      Alexandre Duret-Lutz authored
      src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
      * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
      libtgbaalgos_la_SOURCES): Add them.
      * src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
      as third parameter.
      * src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
      dotty_bfs::process_link): Use the decorator.
      * src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
      is given.
      * src/tgbatest/emptchk.test: Exercize -g.
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      * tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc · 42b05c7a
      Alexandre Duret-Lutz authored
      (tgba_reachable_iterator::process_link): Take the state* as arguments
      in addition to the state numbers.
      * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
      (tgba_explicit::copy_acceptance_conditions_of): New method.
      * tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
      (dupexp_iter::process_state, duplex_iter::declare_state,
      dupexp_iter::name_): Remove.
      (dupexp_iter::process_link): Adjust prototype, and format
      the state here rather than in process_state.
      * tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
      of process_link.
  4. 02 Nov, 2004 4 commits
  5. 29 Oct, 2004 11 commits
  6. 28 Oct, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files. · 7819f14d
      Alexandre Duret-Lutz authored
      Cannot test them because the run returned by the emptiness checks
      are currently incomplete (they lack the acceptance conditions, and
      sometimes even the labels in the prefix).
      * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
      libtgbaalgos_la_SOURCES): Add them.
      * src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run
      when the emptiness checks are fixed.
  7. 27 Oct, 2004 3 commits
    • Alexandre Duret-Lutz's avatar
      Introduce an emptiness-check interface, and modify the existing · 6c815004
      Alexandre Duret-Lutz authored
      algorithms to conform to it, uniformly.  This will unfortunately
      break third-party code that were using these algorithms.
      * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
      * src/tgbaalgos/Makefile.am: New files.
      * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
      conform to the new emptiness-check interface.
      * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
      src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
      Likewise.  The classes have been renamed are as following
        emptiness_check -> couvreur99_check
        emptiness_check_shy -> couvreur99_check_shy
        counter_example -> couvreur99_check_result
      * src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
      iface/gspn/ssp.cc: Adjust to renaming and new interface.
    • Alexandre Duret-Lutz's avatar
      * src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh: · 7010a02c
      Alexandre Duret-Lutz authored
      New files.
      * src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS,
      libevtgbaalgos_la_SOURCES): Add them.
      * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test:
      New files.
      * src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them.
      (ltl2evtgba_SOURCES): New variable.
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert · b89f1e25
      Alexandre Duret-Lutz authored
      that the true state has only one link when unobs is used.
  8. 23 Oct, 2004 1 commit
  9. 22 Oct, 2004 3 commits
    • Alexandre Duret-Lutz's avatar
      Preliminary support for Event-based GBA. · 73ff928b
      Alexandre Duret-Lutz authored
      * src/evtgba/Makefile.am, src/evtgba/evtgba.cc,
      src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh,
      src/evtgba/explicit.cc, src/evtgba/explicit.hh,
      src/evtgba/product.cc, src/evtgba/product.hh,
      src/evtgba/symbol.cc, src/evtgba/symbol.hh,
      src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc,
      src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc,
      src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc,
      src/evtgbaalgos/save.hh, src/evtgbaparse/Makefile.am,
      src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
      src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
      src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am,
      src/evtgbatest/defs.in, src/evtgbatest/explicit.cc,
      src/evtgbatest/explicit.test, src/evtgbatest/product.cc,
      src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
      src/evtgbatest/readsave.test: New files.
      * configure.ac: Create the Makefiles in these new subdirectories.
      * src/Makefile.am: Recurse them.
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/tostring.cc (to_spin_string_visitor): Move to · 38f7cac8
      Alexandre Duret-Lutz authored
      anonymous namespace.
  10. 20 Oct, 2004 3 commits
  11. 18 Oct, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc, · 7d27fd37
      Alexandre Duret-Lutz authored
      src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc,
      src/ltlvisit/dump.cc, src/ltlvisit/length.cc,
      src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
      src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc,
      src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc,
      src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh:
      Declare private classes and helper function in anonymous namespaces.
      * HACKING, src/sanity/style.test: Document and check this.
      Also check for trailing { after namespace or class.
      * src/ltlast/predecl.hh, src/ltlast/visitor.hh,
      src/tgba/tgbareduc.hh: Fix trailing {.
  12. 15 Oct, 2004 2 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Back out all Thomas's changes on emptiness checks since · ed6db926
      Alexandre Duret-Lutz authored
      2004-08-23.  Some of these will need to be reintegrated more
      slowly and cleanly.
      * src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc,
      src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am,
      src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert.
      * src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh,
      src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh,
      src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh,
      src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh,
      src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh:
  13. 14 Oct, 2004 2 commits
  14. 13 Oct, 2004 2 commits