This fixes#552, reported by Rüdiger and Ayrat.
* tests/sanity/style.test: Warn aginst iterations on edge_vector.
* spot/parseaut/parseaut.yy, spot/twaalgos/complete.cc,
spot/twaalgos/parity.cc: Iterate over edges(), not edge_vector().
* tests/core/ltlcross.test: Add a test case for #552.
* NEWS: Mention the bug.
Reported by Yann Thierry-Mieg.
* spot/twaalgos/translate.cc: Run scc_filter if relabel_here reduced
the number of edges, because maybe we have more to remove.
* tests/core/ltl2tgba2.test: Add test case.
* spot/twaalgos/sccfilter.cc: If an inherently-weak automaton has
no rejecting cycle, reduce its acceptance to t instead of Büchi.
* spot/twa/acc.hh (operator==, operator<): Fix comparisons of
true acceptances.
* NEWS: Mention these two changes.
* spot/twaalgos/sccfilter.hh: Update documentation.
* spot/twaalgos/determinize.cc (tgba_determinize): The call
to scc_filter assume that the input BA is never reduced to t
acceptance. Call scc_filter with an extra option to ensure that.
* spot/twaalgos/postproc.cc (do_scc_filter): Adjust to add the
extra option when we want to build Büchi or coBuchi.
(ensure_ba): Don't mark trivial SCCs as accepting.
* tests/core/complement.test, tests/core/dstar.test,
tests/core/ltlsynt.test, tests/core/readsave.test,
tests/core/wdba2.test, tests/python/_product_susp.ipynb,
tests/python/automata-io.ipynb, tests/python/dualize.py,
tests/python/highlighting.ipynb, tests/python/intrun.py,
tests/python/setacc.py, tests/python/simstate.py,
tests/python/stutter-inv.ipynb, tests/python/zlktree.py: Adjust test
cases.
This is a followup to issue #548, which was caused by edges being
dropped. In that context dropping edge was not really desirable, so
let's make this behavior configurable.
* spot/parseaut/public.hh: Add a new option.
* python/spot/__init__.py: Likewise.
* spot/parseaut/parseaut.yy: Honor that option.
* tests/python/parsetgba.py: Add a short test for it.
* NEWS: Mention it.
This fixes#548, reported by Dávid Smolka.
* spot/parseaut/parseaut.yy: Update the edge numbers in the
highlight-edges property.
* tests/core/highlightstate.test: Add test case.
* NEWS: Mention the bug.
Fixes#546 (again).
* spot/twaalgos/gfguarantee.cc (g_f_terminal_inplace): Detect
true/false languages early, so that we do not tag them as
non-inherently-weak.
* tests/core/ltlcross.test: Improve test case.
This massive set of changes was triggered by issue #546.
In addition to the better handling of !weak, this also adds some
weak properties in a few places.
* spot/twaalgos/product.cc (product_aux): Throw some exception
if an automaton with t or f acceptance has the !weak property. This
is a cheap sanity check to help detect algorithms that incorrectly
assumed !weak input would necessarily become !weak output.
* spot/twaalgos/hoa.cc (print_hoa): Likewise, also do not assume
that terminal implies very-weak.
* spot/parseaut/parseaut.yy: Add several diagnostics for similar
cases. E.g., a one-state automaton cannot be declared as !very-weak.
* tests/core/parseaut.test: Check those new diagnostics.
* spot/twa/twa.cc (twa::intersecting_run): Temporary remove the weak
property by setting it to maybe, not to false.
* spot/twaalgos/minimize.cc, spot/twaalgos/parity.cc,
spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc: Account for
the fact that these algorithm may in fact improve the weakness.
* spot/twaalgos/strength.cc: Only look at colors used by the
acceptance condition when deciding weakness.
* spot/twaalgos/synthesis.cc: Declare the strategy as weak.
* bin/randaut.cc: Add weak to automata with t/f acceptance.
* spot/kripke/kripke.hh: Make kripke structures as weak.
* tests/core/acc_word.test, tests/core/alternating.test,
tests/core/complement.test, tests/core/complete.test,
tests/core/ltlsynt.test, tests/core/randomize.test,
tests/core/readsave.test, tests/core/remfin.test,
tests/core/sccsimpl.test, tests/core/strength.test,
tests/core/wdba2.test, tests/ltsmin/kripke.test,
tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/dbranch.py, tests/python/highlighting.ipynb,
tests/python/kripke.py, tests/python/ltsmin-dve.ipynb,
tests/python/mealy.py, tests/python/simstate.py: Adjust all these test
cases.
* NEWS: Mention the fixes.
Part of issue #546 reported by Rüdiger Ehlers
* spot/twaalgos/product.cc (product_susp): Fix detection and handling
of unsatisfiable/universal acceptances.
* tests/python/_product_susp.ipynb: Add test cases.
* spot/twa/twagraph.cc: Mark two variables as unused.
* spot/twaalgos/aiger.cc: Avoid spurious nullptr dereference warning,
and mark more variable as unused.
* spot/twaalgos/forq_contains.cc (word::operator==): Mark as
maybe_unused.
* bin/ltlsynt.cc, spot/twaalgos/relabel.cc,
spot/twaalgos/mealy_machine.cc, spot/twaalgos/synthesis.cc,
spot/twaalgos/zlktree.cc: Avoid unused variables warnings.
* spot/twaalgos/toparity.cc: Remove uses of std::optional, they were
not necessary, and they trigger spurious warnings in GCC 7. Also
work around a spurious "potential nullptr deref".
* tests/core/twacube.cc: Fix another potential nullptr warning.
* spot/twaalgos/simulation.cc: Work a around GCC 6/7 bug.
This is actually used by next patch.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Here.
* tests/python/sccinfo.py: Add a small test case.
* NEWS: Mention it.
This corner case was simply causing segfaults.
* tests/python/mergedge.py: Add a test case.
* spot/twa/twagraph.cc (merge_states): Add special handling for
the case where the automaton has no edges.
This implements the first point of issue #529.
* spot/tl/apcollect.cc, spot/tl/apcollect.hh (collect_litterals): New
function.
* bin/ltlsynt.cc: Implement the --polarity option, use
collect_litterals() to simplify the specification, finally patch the
game, Mealy, or Aiger output.
* spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Take a
relabeling_map has argument to specify extra APs.
* tests/core/ltlsynt.test, tests/core/ltlsynt2.test: Adjust test
cases.
* spot/twaalgos/contains.hh, spot/twaalgos/contains.cc
(containment_select_version): New function.
(contains): Use it.
* spot/twa/twa.cc (exclusive_word): Likewise.
* bin/autfilt.cc (--included-in): Adjust to use forq depending
on containement_select_version.
* bin/man/spot-x.x: Adjust documentation of
CONTAINMENT_SELECT_VERSION.
* tests/core/included.test, tests/python/forq_contains.py: Add more
tests.
* NEWS: Mention the new feature.
* spot/twaalgos/forq_contains.hh,
spot/twaalgos/forq_contains.cc (contains_forq): Swap arguments so
they follow the same order as contains().
* tests/python/forq_contains.py: Adjust.
Rework the way we compute and use cut-points to catch more patterns we
can rewrite. Also Use BDDs to check if a Boolean sub-expression is
false or true. Fixes issue #540.
* spot/tl/relabel.hh: Update documentation
* spot/tl/relabel.cc (relabel_bse): Rework.
* tests/core/ltlfilt.test: Add more test cases.
* tests/python/_mealy.ipynb: Update.
* NEWS: Mention the change.
Requested by Marek Jankola.
* python/spot/impl.i: Add bindings for std::set<unsigned>.
* tests/python/powerset.py: New file.
* tests/Makefile.am: Add it.
* THANKS: Add Marek.
Fixes issue #536. Also a part of issue #500.
* spot/twaalgos/translate.hh, spot/twaalgos/translate.cc: Implement
this new option.
* bin/spot-x.cc, NEWS: Mention it.
* tests/core/ltl2tgba2.test: Add the test case from issue #536.
Related to issue #500 and issue #536.
* spot/tl/relabel.hh (relabel_overlapping_bse): New function.
* spot/tl/relabel.cc: Implement it.
* bin/ltlfilt.cc: Add a --relabel-overlapping-bool option.
* tests/core/ltlfilt.test: Test it.
* NEWS: Mention it.
* bin/common_output.cc, bin/common_output.hh,
bin/randltl.cc: Adjust so that running "randltl -S" use
the SERE flavor of the spot/latex/utf8 formula printers.
* tests/core/latex.test, tests/core/utf8.test,
tests/python/ltlparse.py: Add more test cases.
* bin/common_output.cc: Set the output stream for LTL formats.
* tests/core/serial.test: Add a test case about this issue that also
improve the covering of the previous patch about saving file
descriptors.
* spot/graph/graph.hh (new_univ_dests): Add an overload taking
a temporary vector.
* spot/twa/twagraph.cc (defrag_states): Use it.
* tests/core/parity.cc: Remove some temporary variables.
Fixes#534.
* bin/common_file.hh, bin/common_file.cc: Make it possible
to reopen a closed file.
* bin/common_output.cc, bin/common_aoutput.cc: Add a heuristic
to decide when to close files.
* tests/core/serial.test: Add a test case.
* NEWS: Mention the issue.
Reported by Yuri Victorovich.
* tests/core/ltlcross4.test: Drop the 'formula' column before
computing aggregates. It causes warnings in some Pandas versions, and
errors in others.
* spot/twa/acc.hh, spot/twa/acc.cc (fin_unit_one_split_improved): New
function.
* python/spot/impl.i: Add bindings for fin_unit_one_split_improved.
* spot/twaalgos/genem.cc: Add the spot212 version.
* tests/python/genem.py: Test it.
Reported by Raven Beutner.
* spot/twaalgos/minimize.cc: Improve comment.
* spot/twaalgos/powerset.cc: Fix handling of an initial state that
is also a sink.
* tests/core/wdba2.test: Add test case.
* NEWS: Mention the bug.
Reported by Philipp Schlehuber-Caissier.
* spot/twaalgos/emptiness.cc (as_twa): Simplify considerably. Don't
try to replay the run, and don't merge identical states.
* spot/twaalgos/word.hh, spot/twaalgos/emptiness.hh: Improve
documentation.
* tests/python/intrun.py: Add a test case.
* NEWS: Mention the bug.
Validity of strategies was tested relying on
num_edges() which might be smaller than the edge_number
* spot/twaalgos/game.cc: Fix here
* tests/python/game.py: Test here
Parity games have been solved semi-locally so far.
We deduced a strategy for the reachable part of the arena
This lead to some inconsistencies when not all state were
rachable.
Now you can chose to solve parity games truely globally.
* spot/twaalgos/game.cc, spot/twaalgos/game.hh: Here
* tests/python/games.ipynb: Test
* spot/twa/formula2bdd.hh,
spot/twa/formula2bdd.cc (bdd_to_cnf_formula): New function.
* python/spot/__init__.py: Add a default dictionary for convenience.
* tests/python/bdditer.py: Add test cases.
* NEWS: Mention it.
Fixes issue #525.
* spot/twaalgos/dbranch.hh, NEWS: Document.
* spot/twaalgos/dbranch.cc: Detect cases where the acceptance should
be changed from state-based to transition-based.
* tests/python/dbranch.py: Add a test case.
