1. 25 Sep, 2017 1 commit
    • Laurent XU's avatar
      misc: add spot::is_colored() · b7ef7c55
      Laurent XU authored
      This function checks whether an automaton is colored, an automaton
      is said to be colored iff all the transitions belong to exactly one
      acceptance set.
      
      * spot/twaalgos/iscolored.cc, spot/twaalgos/iscolored.hh: Here.
      * spot/twaalgos/Makefile.am: add spot/twaalgos/iscolored.{cc,hh}
      * python/spot/impl.i: add spot/twaalgos/iscolored.hh
      b7ef7c55
  2. 24 Sep, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      twa_graph: do not order BDDs by IDs in merge_edges() · 5e5a6948
      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/genltl.test: Adjust, and add an extra test
      for the behavior of #282.
      * 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.
      5e5a6948
    • Alexandre Duret-Lutz's avatar
      postproc: fix a comment · 2bca21f7
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc: Here.
      2bca21f7
  3. 22 Sep, 2017 1 commit
  4. 20 Sep, 2017 2 commits
  5. 19 Sep, 2017 13 commits
    • Alexandre GBAGUIDI AISSE's avatar
      hierarchy: Make is_recurrence() public · e59274b6
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Declare it.
      * spot/tl/hierarchy.cc: Remove static keyword and anonymous namespace.
      * spot/tl/hierarchy.hh: Declare function.
      e59274b6
    • Alexandre GBAGUIDI AISSE's avatar
      ltlfilt: Add %r and %R format options · 8cf54264
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Declare new options.
      * bin/common_output.cc: Add new options.
      * bin/common_output.hh: Add new options.
      * bin/genltl.cc: Update.
      * bin/ltlfilt.cc: Update.
      * bin/ltlgrind.cc: Update.
      * bin/randltl.cc: Update.
      8cf54264
    • 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.
      ad9bc644
    • Alexandre GBAGUIDI AISSE's avatar
      typos · 302095ff
      Alexandre GBAGUIDI AISSE authored
      * spot/twaalgos/alternation.hh: Typos.
      * spot/twa/twa.hh: Typos.
      302095ff
    • 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.
      8ae10f74
    • 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().
      5f6a71d2
    • 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.
      f2616069
    • 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.
      50e99cdc
    • 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
      automaton.
      * tests/python/dca.test: Add tests for Streett automata.
      * tests/Makefile.am: Add all tests.
      cf18c069
    • 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.
      37c1a19b
    • 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()
      wrappers.
      0957317a
    • 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.
      75d9e5f6
    • 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)
      scc_info::acc_sets_of().
      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.
      bd5c6920
  6. 15 Sep, 2017 1 commit
  7. 07 Sep, 2017 1 commit
  8. 06 Sep, 2017 3 commits
  9. 05 Sep, 2017 5 commits
  10. 04 Sep, 2017 3 commits
  11. 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.
      e7df182a
  12. 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.
      6cd6802a
    • 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.
      e8527d5a
    • 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.
      190d4cfa
    • 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.
      42abcf85
    • 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áš.
      646c5170
  13. 01 Sep, 2017 2 commits