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.
Fix#505, Reported by Edmond Irani Liu.
* spot/twa/twagraph.cc (copy): Deal with kripke_graph in a better way.
* spot/twaalgos/hoa.cc: Do not force the use of named-states since
when the input is a kripke_graph.
* tests/python/kripke.py: Adjust test cases.
* NEWS: Mention the change.
* THANKS: Add Edmund.
* spot/twaalgos/hoa.hh (hoa_alias_formater): New class.
* spot/twaalgos/hoa.cc: Implement hoa_alias_formater using the code
that was previously in metadata::encode_label, and use it in place.
* bin/autfilt.cc: Here.
* spot/twaalgos/hoa.cc, spot/twaalgos/hoa.hh: Fix the prototype
of set_aliases so that it is usable.
* tests/core/dualize.test: Add a simple test case.
* NEWS: Mention the new option.
Part of issue #497.
* doc/org/concepts.org: Declare a new "aliases" named property.
* spot/parseaut/parseaut.yy: Fill the aliases named property.
* spot/twa/twa.cc (copy_named_properties_of): Copy it.
* spot/twaalgos/hoa.cc: Use "aliases" while encoding BDDs for
output.
* spot/twaalgos/hoa.hh: Add helper function to set/get aliases.
* python/spot/impl.i: Create a type for aliases.
* tests/core/parseaut.test: Adjust test case.
* tests/python/aliases.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention this change.
This replaces loops of the form
while (all != bddfalse) {
bdd one = bdd_satoneset(all, sup, bddfalse);
all -= one;
// ... use one ...
}
by the more efficient
for (bdd one: minterms_of(all, sub))
// ... use one ...
This patch only focues on loops where the third
argument of bdd_satoneset is bddfalse.
* spot/twaalgos/cobuchi.cc, spot/twaalgos/complement.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc,
spot/twaalgos/dtwasat.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/powerset.cc: Improve bdd_satoneset()-based loops.
*
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll,
spot/twaalgos/hoa.cc: Add input and output support.
* doc/org/hoa.org: Document the HOA extension.
* bin/ltlsynt.cc: Add a --print-game-hoa option to
produce such format.
* tests/core/gamehoa.test: New file to test this.
* tests/Makefile.am: Add it.
* NEWS: Mention this new feature.
Part of issue #376, reported by Hashim Ali.
* python/spot/impl.i: Add bindings for kripke_graph.
* python/spot/__init__.py (automaton): Add a want_kripke option.
* spot/kripke/kripkegraph.hh: Honnor the "state-names" property
when displaying states.
* spot/twaalgos/hoa.cc: Preserve names of Kripke states.
* tests/python/ltsmin-dve.ipynb: Illustrate all the above.
* NEWS: Mention those changes.
* THANKS: Add Hashim.
spot::acc_cond::mark_t is implemented as a bit vector using a single
unsigned, and implicit conversions between mark_t and unsigned may be
confusing. We try to use the proper interface.
* bin/autfilt.cc, bin/ltlsynt.cc, spot/kripke/kripke.cc,
spot/misc/game.hh, spot/parseaut/parseaut.yy, spot/priv/accmap.hh,
spot/ta/ta.cc, spot/ta/taexplicit.cc, spot/ta/taproduct.cc,
spot/taalgos/emptinessta.cc, spot/taalgos/tgba2ta.cc, spot/twa/acc.cc,
spot/twa/acc.hh, spot/twa/taatgba.cc, spot/twa/taatgba.hh,
spot/twa/twagraph.hh, spot/twaalgos/alternation.cc,
spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc,
spot/twaalgos/complete.cc, spot/twaalgos/couvreurnew.cc,
spot/twaalgos/degen.cc, spot/twaalgos/dot.cc,
spot/twaalgos/dtwasat.cc, spot/twaalgos/dualize.cc,
spot/twaalgos/emptiness.cc, spot/twaalgos/gtec/ce.cc,
spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gtec/sccstack.cc,
spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/lbtt.cc,
spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc,
spot/twaalgos/ndfs_result.hxx, spot/twaalgos/rabin2parity.cc,
spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh,
spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc,
spot/twaalgos/stripacc.cc, spot/twaalgos/stutter.cc,
spot/twaalgos/sum.cc, spot/twaalgos/tau03.cc,
spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc,
spot/twaalgos/toweak.cc, python/spot/impl.i, tests/core/acc.cc,
tests/core/twagraph.cc: do not confuse mark_t and unsigned
* tests/python/acc_cond.ipynb: warn about possible change of the API
For #212.
* spot/twa/twa.hh: Rename prop_deterministic() as prop_universal(),
and keep the old name as deprecated.
* spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh: Rename
is_deterministic() as is_universal(), and add a new function
for is_deterministic().
* doc/org/concepts.org, doc/org/hoa.org, doc/org/tut21.org,
spot/tl/hierarchy.cc, spot/twa/twagraph.cc,
spot/twaalgos/are_isomorphic.cc, spot/twaalgos/determinize.cc,
spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/hoa.cc, spot/twaalgos/minimize.cc,
spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/totgba.cc,
spot/twaalgos/word.cc, tests/python/product.ipynb,
tests/python/remfin.py: Adjust.
* NEWS: Mention the change.
* spot/twa/twa.hh: Implement the property.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input
and output for it.
* spot/twaalgos/strength.cc,
spot/twaalgos/strength.hh (is_very_weak_automaton): New function.
* tests/core/alternating.test: Add a test for --check=strength
on an alternating automaton.
* tests/core/strength.test, tests/core/parseaut.test: Adjust expected
output.
* NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it.
The only missing point is that the HOA parser cannot deal with multiple
universal initial states, as seen in parseaut.test.
* spot/graph/graph.hh (new_univ_dests): New function, extracted from...
(new_univ_edge): ... this one.
* spot/twa/twagraph.hh (set_univ_init_state): Implement using
new_univ_dests.
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, python/spot/impl.i:
Add support for universal initial states.
* spot/parseaut/parseaut.yy: Add preliminary support for
universal initial states. Multiple universal initial states
are still not supported.
* tests/core/alternating.test, tests/core/parseaut.test,
tests/python/alternating.py: Adjust tests and exercise this new feature.
* NEWS, spot/twa/twa.hh: Document the change.
* spot/twa/twagraph.hh, spot/kripke/kripkegraph.hh:
Add an exception in get_init_state_number().
get_init_state() now calls get_init_state_number().
* spot/twa/twagraph.cc, spot/twaalgos/simulation.cc,
spot/twaalgos/powerset.cc, spot/twaalgos/complete.cc,
spot/twaalgos/sccfilter.cc: Remove now useless tests.
* spot/twaalgos/hoa.cc: Remove now useless comment.
* spot/twaalgos/minimize.cc: Never return an automaton with no state.
* spot/twa/twa.cc, spot/twa/twa.hh: Add a way to
remove named properties.
* spot/twa/twagraph.cc: Clear highlight-edges on operations
that reorder the edge vector.
* spot/twaalgos/randomize.cc, spot/twaalgos/randomize.hh:
Preserve highlighted state, but not highlighted edges.
* spot/twaalgos/hoa.cc: Adjust output of highlight-edge
when the edges are not stored in order.
* tests/core/readsave.test, tests/core/tgbagraph.test,
tests/core/twagraph.cc: More test cases.
Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap()
so that the methods where this behavior is expected can be fixed.
And fix ltsmin::kripke() which did not register APs.
Part of #170.
* spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs.
Throw an exception when printing automata using unregistered APs.
* spot/ltsmin/ltsmin.cc: Call register_ap().
* spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc,
spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap):
New methods.
* spot/tl/exclusive.cc, spot/twaalgos/postproc.cc,
spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them.
* tests/core/maskacc.test, tests/core/maskkeep.test,
tests/core/strength.test: Adjust expected results.
* NEWS: Mention those changes.
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc: If a Kripke
structure is passed, automatically enable the "k" option.
* tests/core/parse_print_test.cc, tests/ltsmin/modelcheck.cc,
tests/python/ltsmin.ipynb: Remove the explicit use of "k".
* NEWS: Mention the change.
* NEWS: Mention the change.
* src/: Rename as ...
* spot/: ... this, adjust all headers to include <spot/...> instead of
"...", and adjust all Makefile.am to search headers from the top-level
directory.
* HACKING: Add conventions about #include.
* spot/sanity/style.test: Add a few more grep to catch cases
that do not follow these conventions.
* .gitignore, Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
debian/rules, doc/Doxyfile.in, doc/Makefile.am,
doc/org/.dir-locals.el.in, doc/org/g++wrap.in, doc/org/init.el.in,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut30.org, iface/ltsmin/Makefile.am,
iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc,
iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc,
wrap/python/Makefile.am, wrap/python/ajax/spotcgi.in,
wrap/python/spot_impl.i, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/randgen.py, wrap/python/tests/run.in: Adjust.
