1. 20 Jun, 2018 3 commits
    • Alexandre Duret-Lutz's avatar
      org: fix lists of escape sequences · b7e77743
      Alexandre Duret-Lutz authored
      * doc/org/autfilt.org, doc/org/ltl2tgba.org, doc/org/ltlfilt.org: Here.
    • Alexandre Duret-Lutz's avatar
      translate: add ltl-split option · 4815a361
      Alexandre Duret-Lutz authored
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Build
      automata with generic acceptance by doing product of automata for
      smaller subformulas.
      * bin/spot-x.cc: Mention ltl-split.
      * NEWS: Mention the change, and show some results.
      * tests/core/genltl.test, tests/python/_product_susp.ipynb,
      tests/python/highlighting.ipynb: Adjust test cases.
      * doc/org/ltl2tgba.org: Update.
      * tests/core/gragsa.test: Add another formula to cover more
    • Alexandre Duret-Lutz's avatar
      product_susp: new function · 4f2e9512
      Alexandre Duret-Lutz authored
      * spot/twaalgos/product.cc, spot/twaalgos/product.hh: Implement it.
      * tests/python/_product_susp.ipynb: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention it.
  2. 15 Jun, 2018 3 commits
  3. 14 Jun, 2018 1 commit
  4. 13 Jun, 2018 1 commit
  5. 11 Jun, 2018 3 commits
    • Alexandre Duret-Lutz's avatar
      scc_filter: add quick test for very-weak · fbc372e2
      Alexandre Duret-Lutz authored
      Related to issue #351.
      * spot/twaalgos/sccfilter.cc: When handling weak automata, we know
      they are very-weak if the SCC count is equal to the number of states.
      * tests/core/dca2.test, tests/core/monitor.test,
      tests/core/parity2.test, tests/core/randomize.test,
      tests/core/readsave.test, tests/core/remfin.test,
      tests/core/sccsimpl.test, tests/core/wdba2.test,
      tests/python/dualize.py, tests/python/remfin.py: Adjust output.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba_fm: mark persistence formulas as weak automata · 729921c0
      Alexandre Duret-Lutz authored
      ... instead of inherently-weak.  The reason they were tagged
      as inherently-weak is historical: this property was introduced
      1.5 years before the weak propery.
      Fixes #351.
      * spot/twaalgos/ltl2tgba_fm.cc: Use prop_weak() instead of
      prop_inherently_weak().  Also be more conservative about the use of
      single_acc when unambiguous automata are generated.
    • Alexandre Duret-Lutz's avatar
      specialize scc_filter for inherently_weak automata · 95d732e3
      Alexandre Duret-Lutz authored
      Part of issue #351.
      * spot/twaalgos/sccfilter.cc, spot/twaalgos/sccfilter.hh: Specialize
      for inherently-weak automata.
      * spot/twaalgos/postproc.cc: Simplify.
      * tests/core/dca2.test, tests/core/parity2.test,
      tests/core/prodor.test, tests/core/randomize.test,
      tests/python/automata.ipynb, tests/python/highlighting.ipynb,
      tests/python/product.ipynb, tests/python/remfin.py,
      tests/python/stutter-inv.ipynb: Adjust.
      * NEWS: Mention it.
  6. 08 Jun, 2018 3 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Reorder and fix some typos. · 2fad1ff6
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      genltl: add --gf-equiv-xn, --gf-implies-xn · 1341c656
      Alexandre Duret-Lutz authored
      * spot/gen/formulas.cc, spot/gen/formulas.hh: Here.
      * bin/genltl.cc: Add options.
      * tests/core/genltl.test: Test them.
      * NEWS: Mention them.
    • Alexandre Duret-Lutz's avatar
      gf_guarantee_to_ba: save states using histories · 7e932586
      Alexandre Duret-Lutz authored
      This improves gf_guarantee_to_ba() on formulas GF(φ) where the
      automaton for F(φ) as several leading transiant SCCs.  E.g.,
      GF(a <-> XXXa) where we know get results that are as good as
      those of delag without loosing on the cases where delag's technique
      would actually produce two big automata.
      * spot/twaalgos/gfguarantee.cc: Implement this.
      * spot/twaalgos/gfguarantee.hh, NEWS: Document it.
      * tests/core/ltl2tgba2.test, tests/core/ltl3ba.test: Add test cases.
  7. 05 Jun, 2018 7 commits
  8. 03 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      genltl: three new families --sejk-{j,k,patterns} · c76df95c
      Alexandre Duret-Lutz authored
      These correspond to the first three blocks of table 1 in S. Sickert,
      J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic Büchi
      Automata for Linear Temporal Logic.  CAV'16.  LNCS 9780.
      For #353.
      * spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
      the new families.
      * tests/core/genltl.test: Test it.
      * bin/man/genltl.x, NEWS: Document it.
  9. 01 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      improve alternation removal to match G&O construction · e87d308e
      Alexandre Duret-Lutz authored
      When dealternating the VWAA for GFa, our result had two states that
      could not be fused by simulation because of unmatched acceptance mark.
      With this change, the result can be simplified.
      * spot/twaalgos/alternation.cc: Here.
      * tests/core/alternating.test, tests/python/alternation.ipynb: Update
      test case.
      * NEWS: Mention it.
  10. 26 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      acc: turn some assertions into exceptions · 6d9d35c9
      Alexandre Duret-Lutz authored
      * spot/misc/bitset.cc, spot/misc/bitset.hh (set, clear):
      Turn asserts into exceptions.
      * spot/twa/acc.hh (mark_t): As a consequence, the
      constructor is not noexcept anymore.
      * tests/core/acc.cc, tests/python/except.py: More tests.
  11. 25 May, 2018 7 commits
    • Alexandre Duret-Lutz's avatar
      fix a9293f32 · be0997c9
      Alexandre Duret-Lutz authored
      * spot/twaalgos/alternation.cc: Always call ensure_weak_scc().
    • Alexandre Duret-Lutz's avatar
      fix and check shifting issue · b12eb050
      Alexandre Duret-Lutz authored
      The exception raised by << and >> when shifting mark_t by too many
      bits are only enabled in SPOT_DEBUG, as those operations are quite
      low-level.  However we were always testing them, and although we
      wanted them to be active in Python, it was not always the case.
      * spot/twa/acc.hh: introduce max_accsets() as
      a static constexpr method, so we can see it in Python.
      * spot/misc/bitset.hh: Fix preprocessing directive
      so the check is actually enabled when compiling the Python
      * bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc: Use max_accsets().
      * tests/core/acc.cc: Comment out the shifting exception when
      SPOT_DEBUG is unset.
      * tests/python/except.py: Make sure the exception is always raised in
    • Alexandre Duret-Lutz's avatar
    • Maximilien Colange's avatar
      fix warnings when compiling without assertions · a9293f32
      Maximilien Colange authored
      * spot/twa/acc.hh, spot/twaalgos/alternation.cc,
        spot/twaalgos/determinize.cc, spot/twaalgos/ndfs_result.hxx,
        spot/twaalgos/tau03.cc, spot/ltsmin/ltsmin.cc, tests/core/parity.cc:
    • Maximilien Colange's avatar
      optimize split_2step · e8866092
      Maximilien Colange authored
      * spot/twaalgos/split.cc: split_2step relies less on bdd, which improves
        its performance
      * tests/python/split.py: update test
    • Maximilien Colange's avatar
      twa_graph: add a method to merge states with same outgoing edges · 5a819e0c
      Maximilien Colange authored
      * spot/twa/twagraph.hh, spot/twa/twagraph.cc: here
      * NEWS: document it
      * tests/core/twagraph.cc, tests/core/tgbagraph.test: test it
    • Maximilien Colange's avatar
      a few improvements to mark_t · 5b908800
      Maximilien Colange authored
      * spot/misc/bitset.hh: add methods set() and clear()
      * spot/twa/acc.hh: deprecate comparison of mark_t with unsigned, and
        rely more on biset for efficiency
  12. 24 May, 2018 6 commits
  13. 23 May, 2018 3 commits
    • Alexandre Duret-Lutz's avatar
      product: optimize product with weak automata · a738801e
      Alexandre Duret-Lutz authored
      Fixes #350.
      * spot/twaalgos/product.cc: Implement this change.
      * NEWS, spot/twaalgos/product.hh: Mention it.
      * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::sat_mark): New method.
      * tests/python/_product_weak.ipynb: New file.
      * tests/Makefile.am: Add it.
      * tests/python/automata.ipynb, tests/python/highlighting.ipynb,
      tests/python/product.ipynb, tests/core/prodor.test: Adjust test cases.
    • Maximilien Colange's avatar
      ltlsynt: improve coverage · b6550388
      Maximilien Colange authored
      * tests/core/ltlsynt.test: here
    • Maximilien Colange's avatar
      genltl: improve coverage · 61b2b9b1
      Maximilien Colange authored
      * tests/core/genltl.test: here
      * spot/gen/formulas.cc: typo