1. 19 Feb, 2021 3 commits
  2. 18 Feb, 2021 1 commit
    • Alexandre Duret-Lutz's avatar
      twagraph: improve doc · 0b048e1c
      Alexandre Duret-Lutz authored
      Based on report by Michaël Cadilhac.
      * spot/graph/graph.hh, spot/twa/twagraph.hh (defrag_state): Clarify
      that only unreachable states are meant to be removed.
      * spot/twa/twagraph.hh (merge_edges): Typo in comment.  Fixes #454.
      * THANKS: Add Michaël.
  3. 03 Feb, 2021 2 commits
    • Alexandre Duret-Lutz's avatar
      work around a GraphViz 2.60.0 bug · 57b508c7
      Alexandre Duret-Lutz authored
      * spot/twa/twagraph.cc (dump_storage_as_dot): Prefer \n over a plain
      new line to work around GraphViz issue 1931, which was causing
      twagraph-internals.ipynb to fail in our test suite.
    • Alexandre Duret-Lutz's avatar
      fix eventual/universal properties for ->/<->/xor · c06e15e0
      Alexandre Duret-Lutz authored
      * spot/tl/formula.cc: Correctly set eventual and universal properties
      for ->, <->, and xor.  This wasn't really relevant before, but there
      are now situation where those are not rewritten.
      * tests/core/kind.test: Adjust expected output.
      * tests/core/ltl2tgba2.test: New test case, reported by Florian
      * NEWS: Mention the bug.
  4. 27 Jan, 2021 2 commits
    • Alexandre Duret-Lutz's avatar
      translate: speed up some -G -D cases · 93d8f432
      Alexandre Duret-Lutz authored
      When gf-guarentee works and produce a deterministic automaton, use it
      right away without comparing it with the automaton produced by the
      regular translation.  This used to be the case for all -D scenarios
      except -G -D.
      Reported by Florian Renkin.
      * spot/twaalgos/translate.cc: Use the result of
      gf_guarantee_to_ba_maybe() or fg_safety_to_dca_maybe() whenever -D is
      * spot/twaalgos/postproc.cc: Call remove_unused_ap() in finalize(), to
      iron out some slight output differences.
      * tests/core/ltl2tgba2.test, tests/python/toparity.py: Lower expected
      results in the test cases.
      * tests/python/automata.ipynb, tests/core/prodor.test: Adjust to new
    • Alexandre Duret-Lutz's avatar
      merge_edge: clarify documentation · 238a9ffc
      Alexandre Duret-Lutz authored
      Reported by Florian Renkin.
      * spot/graph/graph.hh, spot/twa/twagraph.hh (merge_edge): Document
      that it is expected that state i can only be renamed as j if j≤i.
  5. 20 Jan, 2021 1 commit
    • Alexandre Duret-Lutz's avatar
      twa_graph: swap the two passes of merge_edges() · 20721514
      Alexandre Duret-Lutz authored
      This improves the determinism in a few cases.
      * spot/twa/twagraph.cc (merge_edges): Encapsulate the two
      passes into lambdas so that they are very easy to swap.
      * spot/twa/twagraph.hh (merge_edges): Adjust documentation.
      * tests/python/mergedge.py: Add test case.
      * tests/core/alternating.test, tests/python/alternation.ipynb:
      Determinism was improved.
      * tests/core/parity2.test, tests/core/readsave.test,
      tests/core/sbacc.test, tests/python/_product_susp.ipynb,
      tests/python/atva16-fig2a.ipynb, tests/python/decompose.ipynb,
      tests/python/highlighting.ipynb, tests/python/satmin.ipynb,
      tests/python/simstate.py: Adjust expected order of edges.
      * NEWS: Mention the change.
  6. 18 Jan, 2021 27 commits
  7. 17 Jan, 2021 4 commits