1. 09 Apr, 2013 29 commits
  2. 04 Apr, 2013 5 commits
    • Alexandre Duret-Lutz's avatar
      * src/ltlast/formula.cc: Typo. · 2e7711a3
      Alexandre Duret-Lutz authored
      2e7711a3
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: fix translation of !{xxx} when xxx reduces to false · c083c0df
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba_fm.cc: Typo.
      * src/tgbatest/ltl2tgba.test: Add a test case.
      c083c0df
    • Alexandre Duret-Lutz's avatar
      fix a memory leak in basic LTL simplifications · a9fc213a
      Alexandre Duret-Lutz authored
      When something like XFa & FXa is reduced, the subformulae XFa and FXa
      are both rewritten separately to XFa, and then the vector of arguments
      of the And operators, [XFa,XFa], is passed through a specialized loop
      that searches of the form X(...) that can potentially be simplified with
      some other terms.  This loop converts the vector [XFa,XFa] into the set
      {XFa,XFa}={XFa} and forgot to deal with the case where the insertion
      would actually not add an existing subformula.
      
      * src/ltlvisit/simplify.cc: Fix the code for Or, and And.
      * src/ltltest/reduc0.test: New file, to test it.
      * src/ltltest/Makefile.am (TESTS): Add it.
      * src/ltltest/reduccmp.test: Add an extra test that does not
      trigger the bug (because reduccmp.test uses more than basic
      optimizations, and the implication-based simplifications are
      already able to detect that XFa and FXa are equivalent).
      a9fc213a
    • Alexandre Duret-Lutz's avatar
      * HACKING: Typo · 4b70453d
      Alexandre Duret-Lutz authored
      4b70453d
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbascc.cc: 80 columns. · 6835973a
      Alexandre Duret-Lutz authored
      6835973a
  3. 06 Mar, 2013 2 commits
  4. 05 Mar, 2013 4 commits