1. 29 Nov, 2018 1 commit
    • Etienne Renault's avatar
      noexcept: please gcc snapshot · c2c8d215
      Etienne Renault authored
      * bin/common_finput.hh,
      bin/common_trans.cc,
      bin/common_trans.hh,
      spot/misc/minato.hh,
      spot/ta/ta.cc,
      spot/ta/ta.hh,
      spot/twa/acc.hh,
      spot/twaalgos/cycles.hh,
      spot/twaalgos/emptiness.hh,
      spot/twaalgos/gtec/gtec.hh,
      spot/twaalgos/ndfs_result.hxx,
      spot/twaalgos/sccinfo.hh,
      spot/twaalgos/word.cc,
      spot/twaalgos/word.hh: Here.
      c2c8d215
  2. 08 Nov, 2018 1 commit
  3. 15 Oct, 2018 3 commits
  4. 12 Oct, 2018 2 commits
  5. 26 Sep, 2018 2 commits
    • Alexandre Duret-Lutz's avatar
      print_dot: add xlabel to colored states if too many colors in use · 87ef2822
      Alexandre Duret-Lutz authored
      Based on a report from Andreas Tollkötter.
      
      * spot/twaalgos/dot.cc (highlight_states_show_num_): New option,
      turned on implicitly when more than 8 colors are used.
      * tests/core/highlightstate.test: Test it.
      * NEWS: Mention it.
      * THANKS: Add Andreas.
      87ef2822
    • Alexandre Duret-Lutz's avatar
      gcc-snapshot warnings · 10d94d9f
      Alexandre Duret-Lutz authored
      * spot/kripke/kripkegraph.hh, spot/priv/bddalloc.hh,
      spot/priv/freelist.hh, spot/priv/satcommon.hh, spot/ta/taexplicit.cc
      spot/twa/bdddict.cc, spot/twa/twagraph.hh,
      spot/twaalgos/alternation.hh, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/ltl2taa.cc, spot/twaalgos/stutter.cc,
      tests/core/ngraph.cc: Add default constructors, copy constructors, or
      remove useless destructors.
      10d94d9f
  6. 25 Sep, 2018 1 commit
  7. 11 Aug, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      gcc-snapshot warnings · 389ef16b
      Alexandre Duret-Lutz authored
      * spot/kripke/kripkegraph.hh, spot/priv/bddalloc.hh,
      spot/priv/freelist.hh, spot/priv/satcommon.hh, spot/ta/taexplicit.cc
      spot/twa/bdddict.cc, spot/twa/twagraph.hh,
      spot/twaalgos/alternation.hh, spot/twaalgos/dtwasat.cc,
      spot/twaalgos/ltl2taa.cc, spot/twaalgos/stutter.cc,
      tests/core/ngraph.cc: Add default constructors, copy constructors, or
      remove useless destructors.
      389ef16b
  8. 02 Aug, 2018 5 commits
  9. 01 Aug, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      contains: fix the semantics · 23722c03
      Alexandre Duret-Lutz authored
      spot::contains(a, b) should test a⊇b.  It was testing a⊆b instead.
      
      * NEWS: Mention the bug.
      * spot/twaalgos/contains.cc, spot/twaalgos/contains.hh: Fix the
      code and documentation.
      * tests/python/contains.ipynb: Adjust description and expected
      results.
      * python/spot/__init__.py: Also swap the argument of
      language_containment_checker.contains()
      * bin/autfilt.cc: Adjust usage.
      23722c03
  10. 27 Jul, 2018 1 commit
  11. 26 Jul, 2018 4 commits
  12. 24 Jul, 2018 3 commits
    • Maximilien Colange's avatar
      translate any automaton to a parity automaton · 465536d1
      Maximilien Colange authored
      * spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: implement it,
        based on last-appearance record (LAR)
      * spot/twaalgos/Makefile.am: build it
      * NEWS: document it
      * python/spot/impl.i: add to python bindings
      * tests/Makefile.am, tests/python/toparity.py: test it
      465536d1
    • Alexandre Duret-Lutz's avatar
      use the generic emptiness check · da996ecb
      Alexandre Duret-Lutz authored
      * spot/twa/twa.cc (is_empty, intersects): Here.
      * spot/twaalgos/sccinfo.cc (check_scc_emptiness): Here.
      * spot/twaalgos/genem.cc: Report error if the input is alternating.
      * spot/twaalgos/isunamb.cc, spot/twaalgos/sccinfo.hh: Adjust.
      * NEWS: Mention the change.
      da996ecb
    • Alexandre Duret-Lutz's avatar
      genem: implement a generic emptiness check for twa_graph_ptr · d708174c
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh (fin_unit, one_fin): New function.
      * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: New files.
      * spot/twaalgos/Makefile.am: Add it.
      * tests/python/genem.py: New file.
      * tests/Makefile.am: Add it.
      * python/spot/impl.i: Add bindings for genem.hh.
      * NEWS: Mention the new function.
      d708174c
  13. 23 Jul, 2018 2 commits
    • Etienne Renault's avatar
      remove duplicated includes · 8aeadb59
      Etienne Renault authored
      * spot/graph/graph.hh,
      spot/taalgos/tgba2ta.cc,
      spot/tl/formula.hh,
      spot/twaalgos/dot.cc,
      spot/twaalgos/ltl2tgba_fm.cc,
      spot/twaalgos/ndfs_result.hxx,
      spot/twaalgos/powerset.cc,
      spot/twaalgos/stutter.cc: Here.
      8aeadb59
    • Etienne Renault's avatar
      remove useless forward declaration · a1877ab4
      Etienne Renault authored
      * spot/ta/taexplicit.hh,
      spot/twaalgos/compsusp.hh,
      spot/twaalgos/isunamb.hh,
      spot/twaalgos/word.hh: Here.
      a1877ab4
  14. 19 Jul, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      modernize std::string("foo") into "foo"s · d0819350
      Alexandre Duret-Lutz authored
      * spot/ltsmin/ltsmin.cc, spot/misc/tmpfile.cc,
      spot/parseaut/parseaut.yy, spot/taalgos/dot.cc, spot/tl/hierarchy.cc,
      spot/tl/unabbrev.cc, spot/twa/acc.cc, spot/twa/twagraph.cc,
      spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, spot/twaalgos/lbtt.cc,
      spot/twaalgos/neverclaim.cc, spot/twaalgos/strength.cc,
      spot/twaalgos/word.cc: Replace std::string("foo") by "foo"s, and
      include namespace std::string_literals.
      d0819350
  15. 02 Jul, 2018 4 commits
  16. 30 Jun, 2018 2 commits
  17. 28 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      translate: enable a restricted form of ltl-split for TGBA/BA · f5f5daec
      Alexandre Duret-Lutz authored
      Fixes #267
      
      * spot/twaalgos/gfguarantee.cc: Fix a typo when comparing automata
      sizes.
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Use
      ltl-split even for BA/TGBA, but only of conjunctions with GF(..)
      in those cases.
      * tests/core/ltl2tgba2.test: Adjust and add the example of #267.
      * tests/core/degenid.test, tests/core/parity2.test,
      tests/core/stutter-tgba.test, tests/python/automata.ipynb,
      tests/python/highlighting.ipynb, tests/python/stutter-inv.ipynb,
      bin/spot-x.cc: Adjust.
      f5f5daec
  18. 25 Jun, 2018 1 commit
  19. 22 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: simplify the acceptance condition · a325de86
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc: Here.
      * spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Fix some bug
      uncovered by the new simplified automata.
      * tests/core/satmin2.test, tests/core/sccdot.test,
      tests/core/sim3.test, tests/python/decompose.ipynb,
      tests/python/satmin.ipynb: Update expected results.
      * NEWS: Mention the simplification and the bug.
      a325de86
  20. 21 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      improve translation of ms-phi-h=2..3 · 621fb818
      Alexandre Duret-Lutz authored
      * spot/twaalgos/gfguarantee.cc: Rework the history computation to keep
      an overapproximation of the history, and a longer one.  Also replay
      the history even if there is no initial trivial SCC.  This helps with
      translating FG(!a|XXXb) where we need to keep the history of a, but we
      were previously unable to do so because some state had both "a" and
      "ab" as input.
      * spot/twaalgos/translate.cc: Optimize the product of suspendable
      automata by removing useless trivial SCCs.
      * tests/core/genltl.test, tests/core/satmin.test, NEWS: Adjust
      expected results.
      621fb818
  21. 20 Jun, 2018 2 commits
    • 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
      code.
      4815a361
    • 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.
      4f2e9512