1. 14 Nov, 2014 1 commit
  2. 13 Nov, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      futurecondcol: avoid gcc-snapshot bug · 6e2151dc
      Alexandre Duret-Lutz authored
      * src/tgba/futurecondcol.cc: Use swap instead of assignement.  It is
      more efficient, and it avoid the bug of gcc-snapshot mentionned two
      commits below.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba_fm: fix non-deterministic output · 4ea63f84
      Alexandre Duret-Lutz authored
      The ltl_to_tgba_fm() translation function was using a hash_map of
      maps (ugh!) to merge transitions on output.  However recent libstd++
      changed the implementation of hash_map (a.k.a. unordered_map) causing
      transitions to be output in a different order.  This
      implementation-dependent order caused the ltl2ta.test to fail because
      the BA->TA transformation can produce TA of different sizes if you
      simply change the order of transitions in the input BA! This does not
      sound like a nice property for the BA->TA transformation, but Ala Eddine
      isn't sure how to fix it yet.  In the meantime, this patch makes sure
      ltl_to_tgba_fm() will return the same output regardless of the
      implementation of hash_map.
      The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux,
      and with gcc-snapshot (5.0.0 20141016) on Debian.
      * src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging
      using a std::vector and std::sort instead of nested maps tables.
      * NEWS: Mention the fix.
  3. 10 Nov, 2014 1 commit
  4. 24 Oct, 2014 1 commit
  5. 06 Sep, 2014 1 commit
  6. 31 Aug, 2014 4 commits
  7. 22 Aug, 2014 2 commits
  8. 21 Aug, 2014 10 commits
  9. 20 Aug, 2014 4 commits
  10. 19 Aug, 2014 2 commits
  11. 11 Aug, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] Fix a harmless uninitialized read. · d4e3a952
      Alexandre Duret-Lutz authored
      This can only cause failure when running under valgrind (i.e., in the
      test suite), but is not a problem in practice as the test is certain
      to fail the entry->c check whenever entry->b is uninitialized.
      * src/bddop.c (bdd_implies): Here.
  12. 09 Jul, 2014 1 commit
  13. 29 May, 2014 2 commits
  14. 17 May, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Mention recent fix. · a4934c4f
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/equals.cc: Fix style. · 8315cad6
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      snf: Fix the handling of bounded repetition. · 139f7b49
      Alexandre Duret-Lutz authored
      star_normal_form() used to be called under bounded
      repetitions like [*0..4], but some of these rewritings
      are only correct for [*0..].  For instance
           (a*|1)[*]      can be rewritten to    1[*]
      but  (a*|1)[*0..1]  cannot be rewritten to 1[*0..1]
      it would be correct to rewrite the latter as (a[+]|1)[*0..1],
      canceling the empty word in a*.
      Also (a*;b*)[*]     can be rewritten to    (a|b)[*]
      but  (a*;b*)[*0..1]  cannot be rewritten to (a|b)[*0..1]
      and it cannot either be rewritten to (a[+]|b[+])[*0..1].
      This patch introduces a new function to implement
      rewritings under bounded repetition.
      * src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded):
      New function.
      * src/ltlvisit/simplify.cc: Use it.
      * src/ltltest/reduccmp.test: Add tests.
      * doc/tl/tl.tex: Document the rewritings implemented.
  15. 15 May, 2014 2 commits
  16. 14 May, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      doc: update bibliographic references · 97617037
      Alexandre Duret-Lutz authored
      * doc/org/satmin.org, src/bin/man/dstar2tgba.x, src/bin/man/ltl2tgba.x:
      Cite the FORTE'14 paper.
      * doc/org/tools.org, src/bin/man/ltl2tgba.x: Replace the VECOS'11
      citation by IJCCBS'14.
      * src/bin/man/ltl2tgba.x: Cite SPIN'13.
  17. 13 May, 2014 2 commits