1. 15 Jun, 2021 4 commits
  2. 11 Jun, 2021 5 commits
  3. 31 May, 2021 1 commit
  4. 18 May, 2021 1 commit
  5. 17 May, 2021 1 commit
  6. 12 May, 2021 13 commits
  7. 11 May, 2021 1 commit
  8. 03 May, 2021 1 commit
  9. 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.
  10. 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.
  11. 17 Apr, 2021 2 commits
  12. 15 Apr, 2021 2 commits
  13. 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.
  14. 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.