1. 05 Feb, 2004 2 commits
  2. 02 Feb, 2004 6 commits
  3. 30 Jan, 2004 1 commit
  4. 29 Jan, 2004 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition): · 1d72cdc8
      Alexandre Duret-Lutz authored
      Do not treat true and false specially.  Otherwise it breaks
      translation of F(false).
      * src/tgbatest/explprod.test, src/tgbatest/tripprod.test: Do not
      use true as acceptance condition.
      
      * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Use Acc[b] as
      acceptance condition for Fb, not Acc[Fb].
      
      After this change, degeneralized automata are 40% smaller
      1d72cdc8
    • Alexandre Duret-Lutz's avatar
      After this changes, degeneralized automata are 40% smaller · 440029c1
      Alexandre Duret-Lutz authored
      in LBTT's statistics.
      
      * src/tgba/tgbatba.cc (state_tba_proxy): Store an iterator,
      pointing somewhere into the acceptance conditions list, instead of
      an acceptance condition.
      (state_tba_proxy::acceptance_iterator): New method.
      (tgba_tba_proxy_succ_iterator): Adjust to use iterators too.
      (tgba_tba_proxy_succ_iterator::current_state): If the current
      transition is in several consecutive acceptance steps after the
      expected one, advance many steps at once.
      (tgba_tba_proxy::tgba_tba_proxy): Build the acceptance cycle
      as a list, not a map.
      (tgba_tba_proxy::get_init_state, tgba_tba_proxy::succ_iter):
      Adjust.
      * src/tgba/tgbatba.hh (tgba_tba_proxy::acc_cycle_): Declare as
      a list, not a map.
      440029c1
  5. 26 Jan, 2004 3 commits
  6. 23 Jan, 2004 3 commits
  7. 13 Jan, 2004 1 commit
  8. 09 Jan, 2004 5 commits
  9. 08 Jan, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      Run valgrind in test cases. · 92cc5f9b
      Alexandre Duret-Lutz authored
      * src/tgbatest/defs.in (VALGRIND, run): Define.
      * src/tgbatest/bddprod.test, src/tgbatest/dupexp.test,
      src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
      src/tgbatest/explicit.test, src/tgbatest/explpro2.test,
      src/tgbatest/explpro3.test, src/tgbatest/explprod.test,
      src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.test,
      src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Use run().
      92cc5f9b
  10. 06 Jan, 2004 4 commits
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/eesrg.cc (format_state): Do not rewrite n's, · 9297d6dd
      Alexandre Duret-Lutz authored
      just strip the last one.  Escaping must be done at output.
      * iface/gspn/gspm.cc (format_state): Likewise.
      * src/misc/escape.hh, src/misc/escape.cc: New files.
      * src/misc/Makefile.am: Add them.
      * src/tgba/bddprint.cc (bdd_format_accset): New function.
      * src/tgba/bddprint.hh (bdd_format_accset): New function.
      * src/tgbaalgos/dotty.cc (dotty_bfs::process_state):
      Escape the state name using escape_str().
      (dotty_bfs::process_link): Escape conditions and acceptance
      conditions using escape_str().
      * src/tgbaalgos/save.cc (save_bfs::start): Call print_acc().
      (save_bfs::print_acc): New function extracted from save_bfs::start().
      Escape each acceptance condition.
      (save_bfs::process_state): Use escape_str() and print_acc()
      9297d6dd
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/tostring.cc · 8008deed
      Alexandre Duret-Lutz authored
      (to_string_visitor::visit(const atomic_prop*)): Quote propositions
      that start with F, G, or X.
      * src/ltltest/tostring.test: Test quoted propositions.
      * src/tgbaalgos/save.cc (save_bfs::process_state): Escape " and +	characters in formulae.
      * src/tgbatest/readsave.test: Test for this.
      8008deed
    • Alexandre Duret-Lutz's avatar
      a7ab42e4
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): · 24fec22e
      Alexandre Duret-Lutz authored
      Do not skip this computation if from == to but the period is empty.
      24fec22e
  11. 05 Jan, 2004 4 commits
  12. 30 Dec, 2003 1 commit
  13. 29 Dec, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/defs.in (run): New function, run valgrind. · 6f88e518
      Alexandre Duret-Lutz authored
      * src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/tostring.test,
      src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run().
      * Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files,
      Automake 1.8 find them automatically.
      * configure.ac: Require Automake 1.8, in gnits mode, and check
      for valgrind.
      * THANKS: New empty file.
      6f88e518
    • Alexandre Duret-Lutz's avatar
      * doc/Doxyfile.in: Upgrade to Doxygen 1.3.5. Build · c2892a82
      Alexandre Duret-Lutz authored
      documentation for iface/.
      * dox/mainpage.dox: Fix reference to ltl_to_tgba.
      * src/ltlenv/environment.hh: Typo.
      c2892a82
  14. 03 Dec, 2003 1 commit
  15. 28 Nov, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaparse/tgbaparse.yy (cond_list): Simplify into... · 18117865
      Alexandre Duret-Lutz authored
      (condition): ... this.  We now accept only one condition, which
      is a formula.
      * src/tgba/tgbaexplicit.hh (tgba_explicit::add_neg_condition,
      tgba_explicit::get_condition): Remove, unused.
      * src/tgba/tgbaexplicit.cc: Likewise.
      18117865
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/gspn.cc, · e341cc9a
      Alexandre Duret-Lutz authored
      iface/gspn/gspn.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/bddprint.hh, src/tgba/succiter.hh,
      src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
      src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
      src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh, src/tgba/tgbaexplicit.cc,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbaproduct.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/save.cc, src/tgbatest/explicit.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbaparse/tgbaparse.yy,
      wrap/python/tests/ltl2tgba.py:
      Rewrite `accepting condition' as `acceptance condition'.
      The symbols which have been renamed are:
      tgba::all_accepting_conditions
      tgba::neg_accepting_conditions
      succ_iterator::current_accepting_conditions
      bdd_dict::register_accepting_variable
      bdd_dict::register_accepting_variables
      bdd_dict::is_registered_accepting_variable
      tgba_bdd_concrete_factory::declare_accepting_condition
      tgba_bdd_core_data::accepting_conditions
      tgba_bdd_core_data::all_accepting_conditions
      tgba_explicit::declare_accepting_condition
      tgba_explicit::complement_all_accepting_conditions
      tgba_explicit::has_accepting_condition
      tgba_explicit::get_accepting_condition
      tgba_explicit::add_accepting_condition
      tgba_explicit::all_accepting_conditions
      tgba_explicit::neg_accepting_conditions
      state_tba_proxy::acceptance_cond
      accepting_cond_splitter
      e341cc9a
  16. 26 Nov, 2003 2 commits