1. 11 May, 2021 1 commit
  2. 03 May, 2021 1 commit
  3. 30 Apr, 2021 2 commits
    • Alexandre Duret-Lutz's avatar
      remove a useless test · 0744052b
      Alexandre Duret-Lutz authored
      We have enough outputs checked verbatim everywhere so that testing
      that three execution of a single command return the same output is now
      a waste of time.
      * tests/core/simdet.test: Remove.
      * tests/Makefile.am: Adjust.
    • Alexandre Duret-Lutz's avatar
      postproc: add support for -x dpa-simul and simul-trans-pruning · d32f19f5
      Alexandre Duret-Lutz authored
      Also have simul-max default to 4096 instead of 512, because it's
      really simul-trans-pruning that is very slow and need to be limited.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/simulation.cc, spot/twaalgos/simulation.hh,
      spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh:
      Implement the above options.
      * bin/spot-x.cc, NEWS: Document them.
      * tests/core/ltlsynt.test, tests/core/minusx.test,
      tests/core/sim3.test: Add some test cases.
  4. 19 Apr, 2021 2 commits
    • Alexandre Duret-Lutz's avatar
      simulation: fix merging transiant SCCs · fca65136
      Alexandre Duret-Lutz authored
      This fixes #452, and also fix a bug related to transiant SCCs
      incorrectly merged in cosimulation: the source of the edges was
      updated without fixing the chaining of the edges.
      * spot/twaalgos/simulation.cc: Fix all the above.
      * tests/python/simstate.py: Add test case from issue #452.
      * tests/core/det.test, tests/core/ltlsynt.test,
      tests/core/satmin.test: Lower expected sizes.
      * tests/python/decompose.ipynb: Adjust for changed order.
    • Alexandre Duret-Lutz's avatar
      improve documentation for -x sat-minimize · cfa34174
      Alexandre Duret-Lutz authored
      * bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based
      minimization.  It was still referring to TGBA although it works for
      * spot/twaalgos/postproc.cc: Typo.
  5. 17 Apr, 2021 2 commits
  6. 15 Apr, 2021 2 commits
  7. 14 Apr, 2021 1 commit
    • Alexandre Duret-Lutz's avatar
      replace bdd_satoneset(x,y,bddtrue) loops by minterms_of(x,y) · 2a38328a
      Alexandre Duret-Lutz authored
      Because the loops iterate in the opposite order, multiple
      test cases need to be adjusted.
      * spot/taalgos/tgba2ta.cc, spot/twaalgos/alternation.cc,
      spot/twaalgos/dualize.cc, spot/twaalgos/ltl2tgba_fm.cc,
      spot/twaalgos/simulation.cc, spot/twaalgos/stutter.cc,
      spot/twaalgos/toweak.cc: Replace loops based on
      bdd_satonest(x,y,bddtrue) by loops based on minterms_of(x,y).
      * tests/core/degenscc.test, tests/core/dualize.test,
      tests/core/genltl.test, tests/core/readsave.test,
      tests/python/alternation.ipynb, tests/python/automata.ipynb,
      tests/python/decompose.ipynb, tests/python/decompose_scc.py,
      tests/python/dualize.py, tests/python/sccinfo.py,
      tests/python/simstate.py, tests/python/testingaut.ipynb,
      tests/python/word.ipynb: Adjust expected test cases.  The
      only regression is in genltl.test, but the worsened case
      should eventually be fixed as discussed in issue #425 anyway.
  8. 12 Apr, 2021 4 commits
    • Alexandre Duret-Lutz's avatar
      replace bdd_satoneset(x,y,bddfalse) loops by minterms_of(x,y) · d54dca61
      Alexandre Duret-Lutz authored
      This replaces loops of the form
         while (all != bddfalse) {
            bdd one = bdd_satoneset(all, sup, bddfalse);
            all -= one;
            // ... use one ...
      by the more efficient
         for (bdd one: minterms_of(all, sub))
            // ... use one ...
      This patch only focues on loops where the third
      argument of bdd_satoneset is bddfalse.
      * spot/twaalgos/cobuchi.cc, spot/twaalgos/complement.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc,
      spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc,
      spot/twaalgos/powerset.cc: Improve bdd_satoneset()-based loops.
    • Alexandre Duret-Lutz's avatar
      split_edges: actually use the cache, and minterms_of() · f3c42596
      Alexandre Duret-Lutz authored
      * spot/twaalgos/split.cc (split_edges): Fix some typos, reported by
      Philipp, that were causing the cache not to be used.  Speed up using
    • Alexandre Duret-Lutz's avatar
      test minterms_of enumerator · c58aa678
      Alexandre Duret-Lutz authored
      * tests/core/minterm.cc, tests/core/minterm.test: New files.
      * tests/core/.gitignore, tests/Makefile.am: Add them.
    • Alexandre Duret-Lutz's avatar
      [buddy] introduce minterm enumeration support · d2fe4613
      Alexandre Duret-Lutz authored
      * src/bddop.c, src/bddx.h (bdd_ibuildcube2, bdd_first_minterm,
      bdd_next_minterm): New functions.
      * src/bddx.h (minterms_of): New class.
  9. 29 Mar, 2021 3 commits
  10. 24 Mar, 2021 1 commit
  11. 03 Mar, 2021 1 commit
  12. 19 Feb, 2021 3 commits
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 18 Jan, 2021 11 commits