1. 19 Jun, 2012 4 commits
  2. 18 Jun, 2012 1 commit
  3. 07 Jun, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix computation of support_conditions in tgba_wdba_comp_proxy. · d7ff0665
      Alexandre Duret-Lutz authored
      * src/tgba/wdbacomp.cc
      (tgba_wdba_comp_proxy::compute_support_conditions): Fix.
      * src/tgbatest/wdba2.test: Test a formula that used to be wrongly
      minimized if translated by LaCIM, because the product of a
      tgbabddconcrete automaton with another automaton (done during
      WDBA-minimization) use the support conditions to speed things up.
      d7ff0665
  4. 06 Jun, 2012 3 commits
  5. 05 Jun, 2012 1 commit
  6. 04 Jun, 2012 4 commits
  7. 23 May, 2012 3 commits
  8. 22 May, 2012 2 commits
  9. 21 May, 2012 5 commits
    • Alexandre Duret-Lutz's avatar
      Clear the contaiment cache after -r7. · 72f36c50
      Alexandre Duret-Lutz authored
      Doing so will release all BDD variables used by automata created for
      syntactic implication.  This way the main translation will create
      acceptance variables again in a more natural order, which will help
      the degeneralization (until we get a better degeneralization).
      
      * src/ltlvisit/contain.cc, src/ltlvisit/contain.hh
      (language_containment_checker::clear): New method to clear the
      containment cache.
      * src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
      (clear_as_bdd_cache): Also call language_containment_checker::clear.
      72f36c50
    • Alexandre Duret-Lutz's avatar
      Use the distributed LBTT is the installed one is not 1.2.1a. · 1c1c95f6
      Alexandre Duret-Lutz authored
      * m4/lbtt.m4: Check version number.
      1c1c95f6
    • Alexandre Duret-Lutz's avatar
      [lbtt] Make it clearer this is not LBTT 1.2.1. · a8fd9e8b
      Alexandre Duret-Lutz authored
      * configure.ac: Bump the version number to 1.2.1a.
      * NEWS: Summarize all changes since 1.2.1.
      * README: Warn this is not 1.2.1, and add pointers to NEWS and
      ChangeLog.
      a8fd9e8b
    • Alexandre Duret-Lutz's avatar
      Adjust parseout.pl to the new LBTT output. · faed4e8b
      Alexandre Duret-Lutz authored
      * bench/ltl2tgba/parseout.pl: Adjust to output nondeterministic
      indices and number of nondeterministic automata.
      * bench/ltl2tgba/README: Update explanations.
      faed4e8b
    • Tomáš Babiak's avatar
      [lbtt] Count deterministic automata and deterministic states. · f2b188d9
      Tomáš Babiak authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/BuchiAutomaton.h, src/BuchiAutomaton.cc
      (BuchiState::isDeterministic, BuchiAutomaton::isDeterministic,
      BuchiAutomaton::nondeterminismIndex): New methods.
      * src/TestOperations.cc (generateBuchiAutomaton): Collect
      nondeterminism indices, and count deterministic automata.
      * src/TestStatistics.cc, src/TestStatistics.h: Add storage
      for these statistics.
      * src/StatDisplay.cc (printBuchiAutomatonStats,
      printCollectiveStats): Display these statistics.
      f2b188d9
  10. 20 May, 2012 8 commits
  11. 14 May, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
      FM: collect implied formulae in & arguments; do not to translate them · c5b294c7
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc (implied_subforfmulae): New function.
      (ltl_trad_visitor::visit(const binop*)): Use it.  This is an attempt
      to correct the unoptimal translation of 'Fa & GFa' left by previous
      patch.  It still fails to optimize 'Fa & GF(a&b)', but this is not a
      regression compared to previous version.
      c5b294c7
    • Alexandre Duret-Lutz's avatar
      Faster translation of GFa. · 1b143067
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc: Add a "recurring" mode for the
      translation of the child of G.  This generalizes Couvreur's original
      trick to translate GFa as (a|Prom(a))&X(GFa) without generating an
      intermediate GF(a)&F(a) state that would have to be merged with GF(a)
      latter.  This implementation will also speedup formulas such a G((a U
      b) & (c M d)).  With this patch, translating GF(p1) & GF(p2) &
      ... GF(p20) into a TGBA takes 57s instead of 128s on my computer.
      However it alsos causes some formulas to be translated into larger
      automata that are not immediately reduced (the simulation-reduction is
      needed).  For instance Fa & GFa now has a different signature than
      GFa, so translating 'Fa & GFa' generates two states where is used to
      generate only one.
      1b143067
  12. 12 May, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix translation of !{r}. · e2f70e72
      Alexandre Duret-Lutz authored
      We need a marked version of !{r} to perform breakpoint unroling.
      
      * src/ltlast/unop.cc, src/ltlast/unop.hh: Declare a NegClosureMarked
      operator.
      * src/ltlvisit/mark.hh, src/ltlvisit/mark.cc,
      src/tgbaalgos/ltl2tgba_fm.cc: Adjust to deal with NegClosureMarked
      and NegClosure as apropriate.
      * src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
      src/ltlvisit/tunabbrev.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgba/formula2bdd.cc: Deal with NegClosureMarked in the same way as
      we deal with NegClosure.
      * src/tgbatest/ltl2tgba.test: More tests.
      * src/ltltest/kind.test: Adjust.
      * doc/tl/tl.tex: Mention the marked negated closure.
      e2f70e72
  13. 11 May, 2012 2 commits
  14. 10 May, 2012 3 commits