1. 10 Feb, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Take an exprop · 07ba321e
      Alexandre Duret-Lutz authored
      argument.  Consider all possible combinations of propositions when
      generating arcs.  Suggested by Jean-Michel Couvreur.
      * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Adjust.
      * src/tgbatest/ltl2tgba.cc: Honor -fx.
      * src/tgbatest/spotlbtt.test: Exercise -fx.
      * wrap/python/cgi/ltl2tgba.in: Support Couvreur/FM with exploded
      properties.
      07ba321e
  2. 09 Feb, 2004 1 commit
  3. 08 Feb, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      This should help getting accurate statistics (on both the · 7069d540
      Alexandre Duret-Lutz authored
      formula automaton and the synchronized product) from LBTT.
      Idea from Jean-Michel Couvreur.
      
      * src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class.
      (nonacceptant_lbtt_reachable): New function.
      * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New
      function.
      * src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable
      if the -T option is used.
      * src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by
      default.
      7069d540
  4. 05 Feb, 2004 2 commits
  5. 02 Feb, 2004 6 commits
  6. 30 Jan, 2004 1 commit
  7. 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
  8. 26 Jan, 2004 3 commits
  9. 23 Jan, 2004 3 commits
  10. 13 Jan, 2004 1 commit
  11. 09 Jan, 2004 5 commits
  12. 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
  13. 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
  14. 05 Jan, 2004 4 commits
  15. 30 Dec, 2003 1 commit
  16. 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
  17. 03 Dec, 2003 1 commit
  18. 28 Nov, 2003 1 commit