1. 04 Aug, 2017 1 commit
  2. 03 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: extend the palette from 9 to 16 colors · e041db61
      Alexandre Duret-Lutz authored
      Let's close #212 even if this does not cover the 32 sets.
      
      * spot/twaalgos/dot.cc: Change the palette.
      * doc/org/autfilt.org, NEWS: Adjust documentation.
      * tests/core/alternating.test, tests/core/readsave.test,
      tests/core/tgbagraph.test, tests/python/_altscc.ipynb,
      tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
      tests/python/automata-io.ipynb, tests/python/automata.ipynb,
      tests/python/decompose.ipynb, tests/python/gen.ipynb,
      tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb,
      tests/python/piperead.ipynb, tests/python/product.ipynb,
      tests/python/randaut.ipynb, tests/python/word.ipynb: Adjust
      test cases.
      e041db61
  3. 01 Aug, 2017 1 commit
  4. 31 Jul, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      hoa: fix I/O of determinism · d3607a7c
      Alexandre Duret-Lutz authored
      Fixes #212.
      
      * spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Recognize
      exist-branch, and adjust printer to the 1.1 semantics.
      * tests/core/alternating.test, tests/core/complete.test,
      tests/core/det.test, tests/core/explsum.test,
      tests/core/parseaut.test, tests/core/readsave.test,
      tests/core/sbacc.test, tests/core/tgbagraph.test,
      tests/python/alternating.py, tests/python/dualize.py: Adjust test
      cases.
      * NEWS: Mention the change.
      d3607a7c
  5. 28 Jul, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: introduce autcross · 0cf250d8
      Alexandre Duret-Lutz authored
      Fixes #252.
      
      * NEWS: Mention it.
      * bin/autcross.cc, bin/man/autcross.x, doc/org/autcross.org: New
      files.
      * bin/Makefile.am, bin/man/Makefile.am, doc/org/tools.org,
      doc/Makefile.am: Add them.
      * bin/autfilt.cc: Use is_universal() instead of is_deterministic().
      * bin/common_hoaread.hh, bin/common_trans.cc, bin/common_trans.hh,
      bin/ltlcross.cc, bin/ltldo.cc: Factor some bits common between
      ltlcross, ltldo and autcross.
      * tests/core/autcross.test, tests/core/autcross2.test: New files.
      * tests/Makefile.am: Add them.
      * tests/core/dra2dba.test, tests/core/sbacc.test,
      tests/core/streett.test: Use autcross.
      0cf250d8
  6. 27 Jul, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      parseaut: make the scanner reentrant · b9fff6a4
      Alexandre Duret-Lutz authored
      * spot/parseaut/parseaut.yy, spot/parseaut/parsedecl.hh,
      spot/parseaut/public.hh, spot/parseaut/scanaut.ll: Use a reentrant
      scanner, so that we can now parse multiple automaton streams at the
      same time.  This is needed for the future autcross, which is going to
      read several individual automata produced by different tools, while
      reading the stream of automata to process.
      b9fff6a4
  7. 25 Jul, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      acc: make &= and |= symmetrical · abe2c08b
      Alexandre Duret-Lutz authored
      Operator &= used to always move Fin to the front, it does not anymore.
      The only thing it does now is to merge Inf(x)&Inf(y) as Inf({x,y}).
      Operator |= is now symmetrical and merges Fin()s.
      
      Fixes #253.
      
      * spot/twa/acc.cc, spot/twa/acc.hh: Simplify &= and make |= symmetrical.
      * spot/twaalgos/cleanacc.cc: Fix conjunction order.
      * tests/core/acc.test, tests/core/acc2.test, tests/core/parseaut.test,
      tests/core/readsave.test, tests/core/satmin2.test,
      tests/core/sccdot.test, tests/python/acc_cond.ipynb,
      tests/python/accparse.ipynb, tests/python/automata.ipynb,
      tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
      cases.
      abe2c08b
    • Alexandre Duret-Lutz's avatar
      deprecate copy() in favor of make_twa_graph() · 8e685e00
      Alexandre Duret-Lutz authored
      Fixes #258.
      
      * spot/twaalgos/copy.cc: Delete, and move the code...
      * spot/twa/twagraph.cc: ... in some anonymous namespace here.
      * spot/twa/twagraph.hh: Adjust the make_twa_graph() overload.
      * spot/twaalgos/copy.hh, NEWS: Mark copy() as deprecated and redirect
      to make_twa_graph().
      * doc/org/upgrade2.org, doc/org/tut51.org, python/spot/impl.i,
      spot/twaalgos/dot.cc, spot/twaalgos/langmap.cc, tests/core/ikwiad.cc:
      Adjust callers.
      * spot/twaalgos/Makefile.am: Remove copy.cc.
      8e685e00
  8. 24 Jul, 2017 2 commits
  9. 20 Jul, 2017 1 commit
  10. 19 Jul, 2017 1 commit
    • Thomas Medioni's avatar
      Implement to_weak_alternating() which weakifies tgbas · c8889e65
      Thomas Medioni authored
      * NEWS: mention the modification.
      * python/spot/impl.i: makes to_weak_alternating visible from python
      * spot/twaalgos/Makefile.am, spot/twaalgos/toweak.cc,
        spot/twaalgos/toweak.hh: Implements to_weak_alternating.
      * tests/Makefile.am, tests/python/toweak.py: Test the results of
        to_weak_alternating.
      c8889e65
  11. 30 Jun, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      decompose: merge decompose_strength() and decompose_scc() · 09e47d64
      Alexandre Duret-Lutz authored
      These two functions were doing almost identical work, the only
      difference was the way to select the SCC to keep.  Now we have a more
      uniform way to do that.  Closes #172.
      
      * bin/autfilt.cc: Offer a unique --decompose-scc option, but keep
      --decompose-strength as an alias for backward compatibility.
      * spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: Rename
      decompose_strength as decompose_scc, and handle a way to list
      all SCC numers in the string specifier.  This gets rid
      of the nearly identical
      * tests/core/scc.test, tests/core/strength.test,
      tests/python/decompose.ipynb, tests/python/decompose_scc.py: Adjust
      test cases.
      * NEWS: Adjust.
      09e47d64
  12. 22 Jun, 2017 2 commits
  13. 20 Jun, 2017 2 commits
  14. 19 Jun, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      stats: fix slow %s and inappropriate %S output · 413d2d6a
      Alexandre Duret-Lutz authored
      Fixes #269.
      
      * spot/twaalgos/stats.cc: Use twa_statistics instead of
      twa_sub_statistics when %t is not used.
      * bin/common_aoutput.cc: Likewise, also fix %S to use twa_statistics
      instead of num_states(), and document that %s,%t,%e all return
      statistics about the reachable part of the automaton.
      * tests/core/format.test: Add more tests.
      * NEWS: Document the issue.
      413d2d6a
    • Alexandre Duret-Lutz's avatar
      stats: fix slow %s and inappropriate %S output · 20a4959f
      Alexandre Duret-Lutz authored
      Fixes #269.
      
      * spot/twaalgos/stats.cc: Use twa_statistics instead of
      twa_sub_statistics when %t is not used.
      * bin/common_aoutput.cc: Likewise, also fix %S to use twa_statistics
      instead of num_states(), and document that %s,%t,%e all return
      statistics about the reachable part of the automaton.
      * tests/core/format.test: Add more tests.
      * NEWS: Document the issue.
      20a4959f
  15. 08 Jun, 2017 5 commits
  16. 02 Jun, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: fix printing of alternating automata · 7b6cfd44
      Alexandre Duret-Lutz authored
      Related to #208.
      
      * spot/twaalgos/dot.cc: Fix missing definitions of universal nodes,
      and inclusion of universal nodes inside of SCC when none of the
      destination comes back to the SCC.
      * tests/python/_altscc.ipynb: Adjust and add more test cases.
      * tests/core/alternating.test, tests/core/neverclaimread.test,
      tests/core/readsave.test, tests/core/sccdot.test,
      tests/python/decompose.ipynb: Adjust test cases.
      * NEWS: Mention the bug.
      7b6cfd44
  17. 31 May, 2017 4 commits
    • Alexandre Duret-Lutz's avatar
      dot: fix printing of alternating automata · 97f3efab
      Alexandre Duret-Lutz authored
      Related to #208.
      
      * spot/twaalgos/dot.cc: Fix missing definitions of universal nodes,
      and inclusion of universal nodes inside of SCC when none of the
      destination comes back to the SCC.
      * tests/python/_altscc.ipynb: Adjust and add more test cases.
      * tests/core/alternating.test, tests/core/neverclaimread.test,
      tests/core/readsave.test, tests/core/sccdot.test,
      tests/python/decompose.ipynb: Adjust test cases.
      * NEWS: Mention the bug.
      97f3efab
    • Alexandre Duret-Lutz's avatar
      scc_info: keep track of common acceptance sets · 617a7187
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Do it.
      * tests/core/sccdot.test: Add a test case.
      * NEWS: Mention it.
      617a7187
    • Maximilien Colange's avatar
      Degeneralization keeps track of levels. · f7d14ab5
      Maximilien Colange authored
      * NEWS: Document this.
      * spot/twa/twagraph.cc: `copy_state_names_from` handles this new info.
      * spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it.
      * tests/python/origstate.py, tests/python/simstate.py: Update tests to
        reflect the change.
      f7d14ab5
    • Maximilien Colange's avatar
      Simulation keeps track of simulated states in the input automaton. · 7b5ab545
      Maximilien Colange authored
      * NEWS: Document the change.
      * spot/twaalgos/simulation.cc: Implement the change.
      * spot/twa/twagraph.cc: `copy_state_names_from` uses simulated states
        info if present.
      * spot/twaalgos/determinize.cc: Pretty-print in determinization follows
        simulated states, avoiding possible confusion.
      * tests/Makefile.am, tests/python/simstate.py: Add a test.
      7b5ab545
  18. 30 May, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: make it possible to ignore or cut edges · 42562015
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Take
      a filter function as optional argument.
      * tests/core/sccif.cc, tests/core/sccif.test: New files.
      * tests/Makefile.am, tests/core/.gitignore: Adjust.
      * NEWS: Mention the new feature.
      42562015
  19. 18 May, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      bin: release all subformulas between runs · f6607f1a
      Alexandre Duret-Lutz authored
      Fixes #262, reported by Maximilien Colange.
      
      * bin/common_output.cc, bin/common_aoutput.cc, bin/common_aoutput.hh:
      Clear the set of atomic propositions if --stats=%[...]x was used.
      * spot/twa/bdddict.cc: Release any formula associated to a BDD when it
      is unregistered, do not wait for the dictionary's destruction.  This
      was the main culprit for #262.
      * tests/core/ltl2tgba.test: Add test cases.
      * NEWS: Mention the bug.
      f6607f1a
    • Alexandre Duret-Lutz's avatar
      bin: release all subformulas between runs · acdaaac4
      Alexandre Duret-Lutz authored
      Fixes #262, reported by Maximilien Colange.
      
      * bin/common_output.cc, bin/common_aoutput.cc, bin/common_aoutput.hh:
      Clear the set of atomic propositions if --stats=%[...]x was used.
      * spot/twa/bdddict.cc: Release any formula associated to a BDD when it
      is unregistered, do not wait for the dictionary's destruction.  This
      was the main culprit for #262.
      * tests/core/ltl2tgba.test: Add test cases.
      * NEWS: Mention the bug.
      acdaaac4
  20. 11 May, 2017 2 commits
  21. 10 May, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: clear simplification cache between translations · aa404823
      Alexandre Duret-Lutz authored
      The cache used in formula simplification will keep atomic propositions
      defined between several translations, and may impact variable order.
      Reported by Maximilien Colange.
      
      * spot/tl/simplify.hh, spot/tl/simplify.cc,
      spot/twaalgos/translate.cc, spot/twaalgos/translate.hh (clear_cache):
      New method.
      * bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call it.
      * spot/twaalgos/stats.cc: Do not keep a point to the formula after
      printing statistics.
      * tests/core/ltl2tgba.test: Add a test case.
      * tests/core/readsave.test: Adjust one formula.
      * NEWS: Mention the issue.
      aa404823
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: clear simplification cache between translations · f07fbbae
      Alexandre Duret-Lutz authored
      The cache used in formula simplification will keep atomic propositions
      defined between several translations, and may impact variable order.
      Reported by Maximilien Colange.
      
      * spot/tl/simplify.hh, spot/tl/simplify.cc,
      spot/twaalgos/translate.cc, spot/twaalgos/translate.hh (clear_cache):
      New method.
      * bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call it.
      * spot/twaalgos/stats.cc: Do not keep a point to the formula after
      printing statistics.
      * tests/core/ltl2tgba.test: Add a test case.
      * tests/core/readsave.test: Adjust one formula.
      * NEWS: Mention the issue.
      f07fbbae
  22. 09 May, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: introduce edges_of() and inner_edges_of() · 8e19d3f4
      Alexandre Duret-Lutz authored
      This is motivated by some upcoming patch by Heňo.
      
      * spot/twaalgos/sccinfo.hh (edges_of, inner_edges_of): New methods.
      * spot/twaalgos/sccinfo.cc, spot/twaalgos/strength.cc: Use them.
      * spot/twa/twagraph.hh (edge_number): Add an overload.
      * python/spot/impl.i: Bind the new methods.
      * tests/python/sccinfo.py: Add tests.
      * NEWS: Mention the changes.
      8e19d3f4
  23. 08 May, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      simplify: fix related to event_univ handling · 8968bf6c
      Alexandre Duret-Lutz authored
      Fixes #260.  Reported by František Blahoudek.
      
      The simplification F(f)|q = F(f|q), where q designates an event_univ
      formula, was not always applied because of a couple of issue: (1) the
      mospliter was ignoring event_univ unless favor_event_univ was set, (2)
      when processing formulas from res_EventUniv they were not put back
      into res_F or res_G to be subject to the F/G rules.
      
      * spot/tl/simplify.cc: Improve handling of the above points.
      * tests/core/reduccmp.test: Adjust and add test case.
      * tests/core/ltl2tgba2.test, tests/python/atva16-fig2a.ipynb: Adjust.
      8968bf6c
    • Alexandre Duret-Lutz's avatar
      simplify: fix related to event_univ handling · 84595883
      Alexandre Duret-Lutz authored
      Fixes #260.  Reported by František Blahoudek.
      
      The simplification F(f)|q = F(f|q), where q designates an event_univ
      formula, was not always applied because of a couple of issue: (1) the
      mospliter was ignoring event_univ unless favor_event_univ was set, (2)
      when processing formulas from res_EventUniv they were not put back
      into res_F or res_G to be subject to the F/G rules.
      
      * spot/tl/simplify.cc: Improve handling of the above points.
      * tests/core/reduccmp.test: Adjust and add test case.
      * tests/core/ltl2tgba2.test, tests/python/atva16-fig2a.ipynb: Adjust.
      84595883
  24. 05 May, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce spot::split_edges() · 19aae6f9
      Alexandre Duret-Lutz authored
      Fixes #255.
      
      * spot/twaalgos/split.cc, spot/twaalgos/split.hh,
      tests/core/split.test: New files.
      * spot/twaalgos/Makefile.am, tests/Makefile.am: Add them.
      * bin/autfilt.cc (--split-edges): New option.
      * python/spot/impl.i: Process split.hh.
      * tests/python/alternating.py: Test split_edges() on
      an alternating automaton.
      19aae6f9