* bin/autfilt.cc, bin/dstar2tgba.cc, bin/common_hoaread.hh: The
filename is stored in the parsed automaton, so do not pass it another
time to the printer.

* bin/autfilt.cc, bin/dstar2tgba.cc: Move the common
hoa_processor class ...
* bin/common_hoaread.hh: ... here.

* bin/common_trans.cc, bin/common_trans.hh, bin/ltlcross.cc,
bin/ltldo.cc: Rename translator_spec and translators to tool_spec and
tools, so that we can reuse these structures for automata tools
in a future autcross.

* bin/common_color.cc, bin/common_color.hh: New files, with
code extracted from ltlcross.cc.
* bin/Makefile.am: Add them.
* bin/ltlcross.cc: Simplify.

* spot/parseaut/parseaut.yy: Here.

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.

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.

* spot/twaalgos/complete.cc: Here.
* tests/python/dualize.py, tests/core/complete.test: Adjust test cases.

Fixes #276.

* spot/twaalgos/sbacc.cc, spot/twaalgos/degen.cc: Detect accepting
sinks, and merge them.
* tests/python/dualize.py: Adjust.
* tests/python/sbacc.py: More test cases.

* spot/priv/bddalloc.cc: Add hooks on request.
* bin/man/spot-x.x, NEWS: Document the envvar.

* src/bddop.c, src/bddx.h, src/cache.c, src/cache.h, src/kernel.c,
src/kernel.h, src/prime.c, src/prime.h, src/reorder.c: Use power of
two for the sizes of all hash tables, in order to reduce the amount of
divisions performed.  Also allow bddhash to be smaller than bddnodes.

They were not updated since we moved binaries around in Spot 2.0.
Let them use ltl2tgba directly.

* bench/ltlclasses/plot.gnu, bench/ltlclasses/run,
bench/ltlcounter/plot.gnu, bench/ltlcounter/run: Adjust.

Fixes #273.

* NEWS: Mention this.
* spot/twaalgos/dualize.cc, tests/python/dualize.py: Adapt dualize.
* spot/twaalgos/sbacc.cc, tests/core/sbacc.test: sbacc support
  alternating automata

* 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.

Henrich Lauko authored Jul 13, 2017 and Alexandre Duret-Lutz committed Jul 17, 2017

* spot/twaalgos/remfin.cc: Create state-based result.

Henrich Lauko authored Jun 29, 2017 and Alexandre Duret-Lutz committed Jul 17, 2017

Move implementation of tra2tba to remfin.

* python/spot/impl.i: Remove tra2tba python bindings
* spot/twaalgos/Makefile.am: Remove tra2tba
* spot/twaalgos/remfin.cc: Update rabin_strategy
* spot/twaalgos/tra2tba.cc: Delete the file
* spot/twaalgos/tra2tba.hh: Delete the file
* tests/core/remfin.test: Update tests
* tests/python/tra2tba.py: Update tests

Henrich Lauko authored Jun 29, 2017 and Alexandre Duret-Lutz committed Jul 17, 2017

* spot/twa/acc.hh: Implement rs_pairs_view

Henrich Lauko authored Jun 13, 2017 and Alexandre Duret-Lutz committed Jul 17, 2017

* spot/twaalgos/tra2tba.cc: Call 'merge_edges'
* tests/python/tra2tba.py: Update tests

Henrich Lauko authored May 18, 2017 and Alexandre Duret-Lutz committed Jul 17, 2017

* spot/twaalgos/tra2tba.cc: Support Rabin like input
* tests/core/tra2tba.cc: Remove C tests
* tests/core/tra2tba.test: Remove C tests
* tests/python/tra2tba.py: Convert C tests to python
* tests/Makefile.am: Remove C tests and add python tests

Henrich Lauko authored May 09, 2017 and Alexandre Duret-Lutz committed Jul 17, 2017

* python/spot/impl.i: Add bindings for tra2tba
* spot/twaalgos/Makefile.am: Record tra2tba.cc, tra2tba.hh
* spot/twaalgos/tra2tba.cc: Implement transformation of TRA to TBA
* spot/twaalgos/tra2tba.hh: Introduce declaration of tra_to_tba
* tests/Makefile.am: Record tra2tba tests
* tests/core/tra2tba.cc: Add driver for tests
* tests/core/tra2tba.test: Add tests of tra2tba transformation

Fixes #274.

* python/spot/impl.i: Bind sbacc().
* tests/python/sbacc.py: New tesat.
* tests/Makefile.am: Add sbacc.py.

* spot/twaalgos/remfin.cc: 0x16 is not 16.

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.

* doc/org/hierarchy.org: When generating DBA from recurrence formulas,
actually use -B instead of --tgba.

* spot/twa/twa.cc (twa::accepting_run): Here.

* NEWS, configure.ac: Bump version to 2.3.5.dev.

* NEWS, configure.ac, doc/org/setup.org: Update version.

Fixes #271, reported by Henrich Lauko.

* spot/twa/acc.cc (maybe_accepting): Fix handling in case
of disjunction of Fin.
* tests/core/scc.test, tests/python/accparse2.py: Add more
tests.

When an acceptance condition is not Streett-like, is_streett_like
now clears the rs_pair vector parameter before returning. Fixes #270.

* spot/twa/acc.cc: Clear the pair vector.
* spot/twaalgos/totgba.cc: Stop calling streett_to_generalized_buchi()
  when the acceptance condition is not Streett-like.

* spot/ltsmin/ltsmin.cc, tests/ltsmin/modelcheck.cc: Here.

* spot/ltsmin/ltsmin.cc, tests/ltsmin/modelcheck.cc: Here.

* src/bddop.c: Fix shortcut.

* doc/org/install.org: Update.

Fixes #268, reported by Yann Thierry-Mieg.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Call
relabel_bse() + relabel_here().
* tests/core/format.test: Add a test case.
* bin/spot-x.cc, NEWS: Document the change.

* spot/twaalgos/relabel.cc: Deal with the cases where the substitution
value is a Boolean formula.
* spot/twaalgos/relabel.hh: Improve documentation.
* tests/python/relabel.py: Add more tests.
* python/spot/impl.i: Add bindings for are_isomorphic for the above
test.
* NEWS: Mention the news.

* src/bddop.c: Fix shortcut.

* doc/org/install.org: Update.

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.