1. 12 May, 2021 13 commits
  2. 11 May, 2021 1 commit
  3. 03 May, 2021 1 commit
  4. 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.
      0744052b
    • 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.
      d32f19f5
  5. 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.
      fca65136
    • 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
      TwA.
      * spot/twaalgos/postproc.cc: Typo.
      cfa34174
  6. 17 Apr, 2021 2 commits
  7. 15 Apr, 2021 2 commits
  8. 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.
      2a38328a
  9. 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.
      *
      d54dca61
    • 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
      minterms_of().
      f3c42596
    • 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.
      c58aa678
    • 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.
      d2fe4613
  10. 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.
      ec4deb32
    • 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.
      b082df20
    • 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.
      fb066ada
  11. 24 Mar, 2021 1 commit
  12. 03 Mar, 2021 1 commit
  13. 19 Feb, 2021 3 commits
  14. 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.
      0b048e1c
  15. 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.
      57b508c7
    • 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
      Renkin.
      * NEWS: Mention the bug.
      c06e15e0
  16. 27 Jan, 2021 1 commit
    • 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
      used.
      * 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
      order.
      93d8f432