1. 19 Sep, 2017 11 commits
    • Alexandre GBAGUIDI AISSE's avatar
      misc/timer: Gather handling of %r and %R options · ad9bc644
      Alexandre GBAGUIDI AISSE authored
      * bin/autcross.cc: Update.
      * bin/autfilt.cc: Update.
      * bin/common_aoutput.cc: Gather them. Move process_timer struct.
      * bin/common_aoutput.hh: Gather them.
      * bin/common_output.hh: Update.
      * bin/dstar2tgba.cc: Update.
      * bin/ltl2tgba.cc: Update.
      * bin/ltlcross.cc: Update.
      * bin/ltldo.cc: Update.
      * bin/ltlfilt.cc: Update.
      * bin/randaut.cc: Update.
      * spot/misc/formater.hh: Remove an useless function.
      * spot/misc/timer.hh: Add process_timer struct definition.
      * spot/misc/timer.cc: Remove old dead code.
      * spot/twaalgos/stats.cc: Update.
      * spot/twaalgos/stats.hh: Update.
    • Alexandre GBAGUIDI AISSE's avatar
      typos · 302095ff
      Alexandre GBAGUIDI AISSE authored
      * spot/twaalgos/alternation.hh: Typos.
      * spot/twa/twa.hh: Typos.
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/cobuchi: Add dnf_to_dca() · 8ae10f74
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Update news with all co-Büching functions.
      * spot/twaalgos/cobuchi.hh: Declare it.
      * spot/twaalgos/cobuchi.cc: Implement it.
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/cobuchi: Add breakpoint construction and nsa_to_dca() · 5f6a71d2
      Alexandre GBAGUIDI AISSE authored
      * spot/twaalgos/cobuchi.hh: Declare nsa_to_dca().
      * spot/twaalgos/cobuchi.cc: Implement nsa_to_dca().
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/cobuchi: Add dnf_to_nca() method · f2616069
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Update.
      * spot/twaalgos/cobuchi.hh: Declare dnf_to_nca().
      * spot/twaalgos/cobuchi.cc: Implement it.
      * tests/core/dca.test: Add tests.
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/totgba: Add dnf_to_streett() method · 50e99cdc
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Update.
      * spot/twaalgos/totgba.hh: Declare dnf_to_streett().
      * spot/twaalgos/totgba.cc: Implement dnf_to_streett().
      * bin/autfilt.cc: Add --dnf-to-streett cmd line option.
      * tests/core/dnfstreett.test: Add test.
      * tests/Makefile.am: Add test file.
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/cobuchi: Add nsa_to_nca() · cf18c069
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Update.
      * spot/twaalgos/cobuchi.hh: Declare to_dca() and nsa_to_nca().
      * spot/twaalgos/cobuchi.cc: Implement them.
      * python/spot/impl.i: Include new file for python bindings.
      * spot/twaalgos/Makefile.am: Add new file.
      * bin/autfilt.cc: Add --dca command line option. This option does not
      return a deterministic automaton yet, but it will.
      * tests/core/dca.test: Add tests for Büchi automata.
      * tests/python/dca.py: Add a python script that builds a nondet. Streett
      * tests/python/dca.test: Add tests for Streett automata.
      * tests/Makefile.am: Add all tests.
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/scc_info: Add states_on_acc_cycle_of() method · 37c1a19b
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Update.
      * spot/twaalgos/sccinfo.hh: Declare states_on_acc_cycle_of().
      * spot/twaalgos/sccinfo.cc: Implement it.
    • Alexandre GBAGUIDI AISSE's avatar
      spot/twa: Add methods to set co-Büchi acceptance · 0957317a
      Alexandre GBAGUIDI AISSE authored
      * spot/twa/acc.hh: Add set_generalized_co_buchi() method.
      * spot/twa/twa.hh: Add set_generalized_co_buchi() and set_co_buchi()
    • Alexandre GBAGUIDI AISSE's avatar
      Fix: Remove SBAcc option in bin/ltlfilt · 75d9e5f6
      Alexandre GBAGUIDI AISSE authored
      * bin/ltlfilt.cc: Remove SBAcc option as rabin_to_buchi_maybe() works
      with transition-based acceptance as well.
    • Maximilien Colange's avatar
      Use clearer names for three methods of spot::scc_info · bd5c6920
      Maximilien Colange authored
      scc_info::used_acc() and spot::info::used_acc_of() have been renamed to
      scc_info::marks() and scc_info::marks_of().
      scc_info::acc() has been renamed to (the already existing and redundant)
      Old names have been deprecated.
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: implement it.
      * spot/twaalgos/dtwasat.cc, spot/twaalgos/isweakscc.cc,
        spot/twaalgos/remfin.cc, spot/twaalgos/sccfilter.cc: update names.
      * NEWS: documentate it.
  2. 15 Sep, 2017 1 commit
  3. 07 Sep, 2017 1 commit
  4. 06 Sep, 2017 3 commits
  5. 05 Sep, 2017 5 commits
  6. 04 Sep, 2017 3 commits
  7. 03 Sep, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      gen: rename KS_COBUCHI to KS_NCA for consistency · e7df182a
      Alexandre Duret-Lutz authored
      * spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Rename
      the enum, function, and command-line option.
      * tests/core/genaut.test, tests/python/gen.ipynb, tests/python/gen.py:
      Adjust test cases.
      * doc/org/genaut.org: Adjust doc.
  8. 02 Sep, 2017 5 commits
    • Alexandre Duret-Lutz's avatar
      simplify: rewrite GF(a & Fb) as G(Fa & Fb) · 6cd6802a
      Alexandre Duret-Lutz authored
      This addresses part of #35, and is just a generalization of the rules
      from 646c5170 for #263 (hence, no new documentation).
      * spot/tl/simplify.cc: Implement this.
      * tests/core/reduccmp.test: Add test cases.
      * tests/core/stutter-tgba.test: Adjust to expect smaller automata.
    • Alexandre Duret-Lutz's avatar
      Improve simplification of expr[*0..1] · e8527d5a
      Alexandre Duret-Lutz authored
      Fixes #108.
      * spot/tl/simplify.cc: Implement the reduction.
      * doc/tl/tl.tex, NEWS: Document it.
      * tests/core/reduccmp.test: Test it.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba_fm: implement a small optimization · 190d4cfa
      Alexandre Duret-Lutz authored
      Fixes #277.
      * spot/twaalgos/ltl2tgba_fm.cc: Improve the translation of f U g
      when f is universal.  Suggested by Maximilien Colange.
      * tests/core/ltl2tgba.test: Test it.
    • Alexandre Duret-Lutz's avatar
      genltl: add --gxf-and and --fxg-or · 42abcf85
      Alexandre Duret-Lutz authored
      As suggested in #263.
      * spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
      these options.
      * tests/core/genltl.test: Use them.
      * NEWS: Mention them.
    • Alexandre Duret-Lutz's avatar
      simplify: some new simplification rules · 646c5170
      Alexandre Duret-Lutz authored
      For #263, reported by Mikuláš Klokočka.
      G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
      F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)
      * spot/tl/simplify.cc: Implement the rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
      * tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
      smaller automata.
      * THANKS: Add Mikuláš.
  9. 01 Sep, 2017 4 commits
  10. 31 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: add x option for dot2tex · fbb9e437
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh: Add a LaTeX output for acceptance
      * spot/twaalgos/dot.cc: Implement the 'x' option and refactor the code
      a bit to limit duplication.
      * tests/core/dot2tex.test: New test case (requires dot2tex).
      * tests/Makefile.am: Add dot2tex.test.
      * tests/core/alternating.test, tests/core/readsave.test,
      tests/python/automata-io.ipynb: Adjust expected output.
      * NEWS, doc/org/oaut.org: Mention the new option.
  11. 30 Aug, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      dot: add option 'A' to disable 'a' · b242122c
      Alexandre Duret-Lutz authored
      This way in 2.5 we can make 'a' the default, and tell people to use
      SPOT_DOTDEFAULT=A if they want the old behavior in both 2.4 and 2.5.
      * spot/twaalgos/dot.cc: Implement the option.
      * NEWS, bin/common_aoutput.cc: Mention it.
      * tests/core/readsave.test: Test it.
    • Alexandre Duret-Lutz's avatar
      dot: display Rabin-like and Streett-like acceptances · 205294c2
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc (print_acceptance_for_human): Add Rabin-like
      and Streett-like checks.
      * tests/core/sccdot.test, tests/python/decompose.ipynb,
      tests/python/randaut.ipynb, tests/core/alternating.test: Adjust.
  12. 29 Aug, 2017 2 commits
  13. 28 Aug, 2017 1 commit
    • Maximilien Colange's avatar
      Fix a bug in spot.complete() · 1b2f2a79
      Maximilien Colange authored
      spot.complete() could complete an empty co-Büchi automaton into an
      automaton accepting everything.
      * NEWS: Document it
      * spot/twaalgos/complete.cc: Fix it
      * tests/core/complete.test, tests/core/prodor.test: Test it