1. 17 Nov, 2017 2 commits
  2. 16 Nov, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce is_obligation(f) · 50fe34a5
      Alexandre Duret-Lutz authored
      This is not optimal yet because it still construct a minimal WDBA
      internally, but it's better than the previous way to call
      minimize_obligation() since it can avoid constructing the minimized
      automaton in a few more cases.
      
      * spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce
      is_obligation().
      * bin/ltlfilt.cc: Wire it to --obligation.
      * spot/twaalgos/minimize.cc: Implement is_wdba_realizable(),
      needed by the above.
      * tests/core/obligation.test: Test it.
      * bin/man/spot-x.x, NEWS: Document it.
      50fe34a5
  3. 15 Nov, 2017 1 commit
  4. 07 Nov, 2017 2 commits
  5. 06 Nov, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      symplify_acceptance: More rules · e5a37ff9
      Alexandre Duret-Lutz authored
      Fixes #297. Implement the following rules.
      
      Fin(i) & Fin(j) by f if i and j are complementary
      Fin(i) & Inf(i) by f
      Inf(i) | Inf(j) by t if i and j are complementary
      Fin(i) | Inf(i) by t.
      
      * spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Here.
      * tests/python/merge.py: Add more test cases.
      * NEWS: Mention the change.
      e5a37ff9
  6. 05 Nov, 2017 1 commit
  7. 04 Nov, 2017 3 commits
    • Alexandre Duret-Lutz's avatar
      autfilt: introduce --acceptance-is · 62302b60
      Alexandre Duret-Lutz authored
      Fixes #288.
      
      * bin/autfilt.cc: Implement it.
      * spot/twa/acc.cc, spot/twa/acc.hh: Add
      acc_cond::is_generalized_streett, acc_cond::operator==, and
      acc_cond::operator!=.
      * tests/core/randaut.test: Add some tests.
      * NEWS: Mention it.
      62302b60
    • Alexandre Duret-Lutz's avatar
      bin: add %g options to print acceptance name · 75a1d6ac
      Alexandre Duret-Lutz authored
      Fixes #289.
      
      * spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
      bin/common_aoutput.cc, bin/common_aoutput.hh: plug %g and %G into
      acc_cond::name() when arguments are given as %[arg]g.  or %[arg]G.
      * tests/core/acc2.test: Add test case.
      * doc/org/randaut.org, NEWS: Document it.
      75a1d6ac
    • Alexandre Duret-Lutz's avatar
      acc: introduce acc_cond::name() · bd39edde
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::name): New method.
      * spot/twaalgos/dot.cc: Use it.
      * tests/python/acc_cond.ipynb: Add a small test.
      * NEWS: Mention it.
      bd39edde
  8. 03 Nov, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce stutter_invariant_letters() · 4711dcd7
      Alexandre Duret-Lutz authored
      * spot/twaalgos/stutter.cc,
      spot/twaalgos/stutter.hh (stutter_invariant_letters)
      (stutter_invariant_states): Get rid of the broken local variant.
      * tests/python/stutter-inv.ipynb, NEWS: Document.
      * python/spot/impl.i: Bind vector<bdd>.
      4711dcd7
  9. 02 Nov, 2017 1 commit
  10. 01 Nov, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      overhaul the stutter-invariance checks · 6459877a
      Alexandre Duret-Lutz authored
      * spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Cleanup and
      document the api.
      * spot/twa/twa.hh, doc/mainpage.dox: Add a stutter-invariant section.
      * tests/python/stutter-inv-states.ipynb: Rename as ...
      * tests/python/stutter-inv.ipynb: ... this, and add more comments.
      * tests/Makefile.am, doc/org/tut.org: Adjust renaming.
      * bench/stutter/stutter_invariance_randomgraph.cc,
      bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/Makefile.am: Make it compile again.
      * bin/autfilt.cc: Call inplace variants.
      * NEWS: Mention the overhaul.
      6459877a
  11. 19 Oct, 2017 1 commit
  12. 18 Oct, 2017 3 commits
  13. 15 Oct, 2017 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlcross: add support for --reference translators · fcccd5f4
      Alexandre Duret-Lutz authored
      Suggested by Tobias Meggendorfer.  Fixes #295.
      
      * bin/ltlcross.cc, bin/common_trans.hh, bin/common_trans.cc: Implement
      this --reference option.
      * NEWS, doc/org/ltlcross.org: Document it.
      * tests/core/ltlcross3.test: Test it.
      fcccd5f4
    • Alexandre Duret-Lutz's avatar
      ltlcross, autcross, ltldo: support --fail-on-timeout · 183ec1fb
      Alexandre Duret-Lutz authored
      Suggested by Tobias Meggendorfer.  Fixes #294.
      
      * bin/autcross.cc, bin/ltlcross.cc, bin/ltldo.cc: Add the option.
      * tests/core/autcross3.test, tests/core/ltlcross3.test,
      tests/core/ltldo.test: Test it.
      * tests/Makefile.am: Add autcross3.test.
      * NEWS, doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
      Mention the option.
      * THANKS: Add Tobias.
      183ec1fb
    • Alexandre Duret-Lutz's avatar
      simplify: improve the logic of some implication checks · 0a2bca13
      Alexandre Duret-Lutz authored
      Fixes #293.
      
      * spot/tl/simplify.cc: Test implications that would yield tt or ff
      first.  In rules of the form "if a => b, a op b = b" also check
      if b => a, and in this case return smallest(a,b).
      * tests/core/reduccmp.test: Add a test.
      * NEWS: Mention it.
      0a2bca13
  14. 13 Oct, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      translate: add support for -x tls-impl=N · 689aa7fd
      Alexandre Duret-Lutz authored
      This is long overdue, and we probably want to use tls-impl=1 in
      ltlsynt.
      
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh:
      Add support for tls-impl=N.
      * tests/core/ltl2tgba.test: Test it.
      * bin/spot-x.cc, NEWS: Document it.
      689aa7fd
  15. 11 Oct, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      stutter: detect stutter-invariance at the state level · 9b187297
      Alexandre Duret-Lutz authored
      * spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Implement
      stutter-invariance detection at the state level.
      * python/spot/impl.i: Instantiate std::vector<bool>
      * tests/python/stutter-inv-states.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      9b187297
    • Alexandre Duret-Lutz's avatar
      genaut: fix ks_nca · b4963a7a
      Alexandre Duret-Lutz authored
      * spot/gen/automata.cc (ks_nca): The output is complete.
      * tests/core/genaut.test: Add test.
      * NEWS: Mention the bug.
      b4963a7a
  16. 07 Oct, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: add ways to speedup scc_info · 9ca5b8c2
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Add an optional
      argument to abort on accepting SCC, to not keep track of SCC states,
      and some one_accepting_scc() method.
      * NEWS: Mention it.
      * bin/ltlcross.cc, spot/twaalgos/alternation.cc,
      spot/twaalgos/cobuchi.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc,
      spot/twaalgos/dtwasat.cc, spot/twaalgos/isunamb.cc,
      spot/twaalgos/powerset.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
      spot/twaalgos/totgba.cc: Adjust arguments passed to scc_info.
      9ca5b8c2
  17. 05 Oct, 2017 2 commits
  18. 03 Oct, 2017 1 commit
  19. 02 Oct, 2017 1 commit
  20. 29 Sep, 2017 6 commits
    • Alexandre Duret-Lutz's avatar
      simulation: incorrect setting of non-deterministic property · 7e394506
      Alexandre Duret-Lutz authored
      Fixes #286.
      
      * spot/twaalgos/simulation.cc: Only set the deterministic
      property, not the non-deterministic one.
      * tests/core/ltl2tgba.test: Add test case.
      * NEWS: Mention the issue.
      7e394506
    • Alexandre Duret-Lutz's avatar
      formula: fix building of {a->c[*]} · bef58b41
      Alexandre Duret-Lutz authored
      Fixes #285, reported by Florian Perlié-Long.
      
      * NEWS: Mention the issue.
      * spot/tl/formula.cc: Fix it.
      * tests/core/kind.test: Document it.
      * THANKS: Add Florian.
      bef58b41
    • Alexandre Duret-Lutz's avatar
      streett_to_generalized_buchi: fix incorrect algorithm · 32087f29
      Alexandre Duret-Lutz authored
      Fixes #284, reported by Juraj Major.
      
      * spot/twaalgos/totgba.cc: Fix the algorithm.
      * spot/twa/acc.hh: More doc for future generations.
      * tests/core/scc.test: More test cases.
      * NEWS: Mention the issues.
      32087f29
    • Maximilien Colange's avatar
      Fix a bug in scc_info, and clarify documentation · f45112a2
      Maximilien Colange authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Implement it
      * tests/python/sccinfo.py: Test it
      * NEWS: Document the fix
      f45112a2
    • Alexandre Duret-Lutz's avatar
      twa_graph: do not order BDDs by IDs in merge_edges() · cdfe78f1
      Alexandre Duret-Lutz authored
      Fixes #282.
      
      * spot/misc/bddlt.hh (bdd_less_than_stable): New function.
      * spot/twa/twagraph.cc (merge_edges): Use it.
      * tests/core/complement.test, tests/core/degenid.test,
      tests/core/ltldo.test, tests/core/prodor.test,
      tests/core/readsave.test, tests/core/sbacc.test,
      tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
      tests/python/decompose.ipynb, tests/python/dualize.py,
      tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
      tests/python/product.ipynb, tests/python/simstate.py,
      tests/python/tra2tba.py: Adjust all expected outputs.
      * NEWS: Mention the bug.
      cdfe78f1
    • Alexandre Duret-Lutz's avatar
      degen: detect superfluous SCCs and remove them · 900b344c
      Alexandre Duret-Lutz authored
      Suggested by Maximilien Colange.
      
      * spot/twaalgos/degen.cc: If the output has more SCC than the input,
      detect useless SCCs and remove them.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/degen.hh: Add support for a degen-remscc option.
      * bin/spot-x.cc, NEWS: Document it.
      * tests/core/degenscc.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/det.test: Lower some expected size (yay!).
      900b344c
  21. 28 Sep, 2017 1 commit
  22. 27 Sep, 2017 2 commits
  23. 26 Sep, 2017 2 commits