1. 13 Feb, 2004 1 commit
  2. 12 Feb, 2004 1 commit
  3. 11 Feb, 2004 2 commits
  4. 10 Feb, 2004 2 commits
  5. 09 Feb, 2004 2 commits
  6. 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
  7. 05 Feb, 2004 2 commits
  8. 04 Feb, 2004 1 commit
  9. 03 Feb, 2004 3 commits
  10. 02 Feb, 2004 14 commits
  11. 30 Jan, 2004 1 commit
  12. 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
  13. 26 Jan, 2004 3 commits
  14. 23 Jan, 2004 3 commits
  15. 16 Jan, 2004 2 commits
    • Alexandre Duret-Lutz's avatar
      4b4b640e
    • Alexandre Duret-Lutz's avatar
      * src/Alloc.h: Rename as ... · 7c1ac7bb
      Alexandre Duret-Lutz authored
      * src/ObstackAlloc.h: ... this.  The problem is that alloc.h is a
      system header in g++ < 3.0, and Darwin has a case-insensitive
      filesystem.  System headers that include alloc.h pick the local
      Alloc.h version.
      * BuchiAutomaton.h, Configuration.h, DispUtil.cc,
      ExternalTranslator.h, FormulaRandomizer.h, Graph.h.in,
      LtlFormula.h, Makefile.am, NeverClaimAutomaton.h, PathEvaluator.h,
      ProductAutomaton.h, SccIterator.h, SharedTestData.h,
      StatDisplay.h, StateSpace.h, StateSpaceRandomizer.cc,
      StringUtil.h, TestOperations.h, TestRoundInfo.h, TestStatistics.h,
      UserCommandReader.h, UserCommands.h, main.cc: Adjust includes.
      7c1ac7bb