1. 29 Mar, 2021 3 commits
    • Jérôme Dubois's avatar
      split: Improve performance of split_edges() · ec4deb32
      Jérôme Dubois authored
      * spot/twaalgos/split.cc: Add cache to avoid
        computing multiple split on the same condition.
    • Jérôme Dubois's avatar
      postproc: Add the new simulation in do_simul() · b082df20
      Jérôme Dubois authored
      * spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add the new simulation
        in do_simul().
      * bin/man/spot-x.x, bin/spot-x.cc: Add documentation for
        SPOT_SIMULATION_REDUCTION environnement variable and the simul-method
        fine tunning option.
      * NEWS: Mention the changes.
    • Jérôme Dubois's avatar
      simulation: Add simulation based reduction · fb066ada
      Jérôme Dubois authored
      * spot/twaalgos/simulation.hh, spot/twaalgos/simulation.cc: Add
        reduce_direct_sim(), reduce_direct_cosim() and
        reduce_direct_iterated() wich reduce an automaton using simulation.
        This functions wrap the class direct_sim wich compute simulation
        with a new method.
      * doc/spot.bib: Add ref.
      * tests/python/simstate.py: Add tests for the new simulation.
  2. 24 Mar, 2021 1 commit
  3. 03 Mar, 2021 1 commit
  4. 19 Feb, 2021 3 commits
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 18 Jan, 2021 26 commits