* spot/tl/Makefile.am: New sonf files
* spot/tl/sonf.cc,spot/tl/sonf.hh: Here.
* python/spot/impl.i: include sonf.hh header
* doc/spot.bib: add entry for the SONF paper
* tests/python/formulas.ipynb: show sample usage
* tests/python/spot.py: test automata equivalence before/after SONF
* NEWS: mention the change
do them using C++17's __has_include instead
* configure.ac: Do not check for sys/times.h,
valgrind/memcheck.h, and spawn.h.
* bin/common_trans.cc, spot/misc/fixpool.hh, spot/misc/mspool.hh,
spot/misc/timer.hh: Adjust to use __has_include instead.
The fallback definition of SIZE_MAX supplied by flex was not
preprocessor friendly and prevented robin_hood.hh from doing "#if
SIZE_MAX == UINT64_MAX", as observed by Marc Espie on OpenBSD.
* spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Define
__STDC_VERSION__ just so that the code generated by Flex
include <inttypes.h>.
* NEWS: Mention the bug.
* THANKS: Add Marc.
* spot/twaalgos/parity.cc (reduce_parity): Use the
size of the edge vector to initialize piprime1 and piprime2,
not the number of edges.
* tests/python/parity.py: Add test case, based on a report
by Yann Thierry-Mieg.
These were deprecated in C++11, and are supposed to be removed from
C++17, however gcc-snapshot just started warning about those.
* spot/misc/bddlt.hh, spot/misc/hash.hh, spot/misc/ltstr.hh,
spot/twa/taatgba.hh, spot/twaalgos/ltl2tgba_fm.cc: Here.
* spot/twaalgos/remprop.cc, spot/twaalgos/remprop.hh (to_finite): New
function.
* bin/autfilt.cc (--to-finite): Add it.
* doc/org/tut12.org: Update to use it.
* spot/twa/twagraph.cc (purge_dead_states): Also remove false edges.
* spot/parseaut/parseaut.yy: Do not ignore false self-loops, and
add false self-loop on accepting states without successors.
* NEWS: List the above changes.
* tests/core/ltlf.test: New file.
* tests/Makefile.am: Add it.
* tests/core/complete.test: Adjust expected output.
Fixes#497.
* spot/twaalgos/dot.cc: Implement this option.
* tests/core/ltl2tgba.test, tests/core/randaut.test: @ is
now a valid option for --dot, use something else.
* tests/python/aliases.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* doc/org/hoa.org: Mention aliases.
* NEWS: Mention this new feature.
* 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.
The current building issue is a docker issue unrelated to Spot,
so it should not prevent us from doing a release.
* .gitlab-ci.yml (rpm-pkg): Allow failure.
* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Ignore edges
whose colors are not part of the colors gathered in the SCC up to
deciding acceptance.
* tests/python/genem.py: New test case, reported by Clément Tamines.
* THANKS: Add him.
* NEWS: Mention the bug.
The related GraphViz issue is
https://gitlab.com/graphviz/graphviz/-/issues/2179
* spot/twaalgos/dot.cc: Avoid initial newline in title.
* NEWS: Mention the bug.
* tests/core/det.test, tests/core/dstar.test,
tests/core/neverclaimread.test, tests/python/automata-io.ipynb: Adjust
test cases.
Monitors can now be split AND completed at the same time.
Split can be called on games without providing
"synthesis-outputs" - relying on named prop.
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Here
Reported by Reuben Rowe.
* spot/twaalgos/complement.cc (complement): Remove the hard-coded
simul=0 option on automata with >32 states. In 2.10 simul=0 now
implies det-simul=0, causing the regression, and most importantly it
is not needed anymore, because we have other threashold like simul-max
and simul-trans-pruning in place.
* tests/core/complement.test: Add Reuben's automaton as test case.
* NEWS: Mention the fix.
This fixes#492, based on a report from Jérôme Dubois.
* spot/twaalgos/sbacc.cc: If the initial state is in a rejecting
component, start with an initial state whose colors are unsat_mark.
* tests/core/sbacc.test: Add test case.
* tests/python/pdegen.py: Adjust it.
The current building issue is a docker issue unrelated to Spot,
so it should not prevent us from doing a release.
* .gitlab-ci.yml (rpm-pkg): Allow failure.
* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Ignore edges
whose colors are not part of the colors gathered in the SCC up to
deciding acceptance.
* tests/python/genem.py: New test case, reported by Clément Tamines.
* THANKS: Add him.
* NEWS: Mention the bug.
The related GraphViz issue is
https://gitlab.com/graphviz/graphviz/-/issues/2179
* spot/twaalgos/dot.cc: Avoid initial newline in title.
* NEWS: Mention the bug.
* tests/core/det.test, tests/core/dstar.test,
tests/core/neverclaimread.test, tests/python/automata-io.ipynb: Adjust
test cases.
Monitors can now be split AND completed at the same time.
Split can be called on games without providing
"synthesis-outputs" - relying on named prop.
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Here
* tests/python/_synthesis.ipynb: Testing
* doc/org/concepts.org, NEWS: Document it.
* spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/sbacc.cc, spot/twaalgos/sbacc.hh: Use it.
* spot/twa/twagraph.cc: Update it on defrag.
* spot/twa/twa.cc (copy_named_properties_of): Copy it.
* tests/python/det.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i (get_original_states, get_original_classes): New
methods, to help with the tests.
Reported by Reuben Rowe.
* spot/twaalgos/complement.cc (complement): Remove the hard-coded
simul=0 option on automata with >32 states. In 2.10 simul=0 now
implies det-simul=0, causing the regression, and most importantly it
is not needed anymore, because we have other threashold like simul-max
and simul-trans-pruning in place.
* tests/core/complement.test: Add Reuben's automaton as test case.
* NEWS: Mention the fix.
This fixes#492, based on a report from Jérôme Dubois.
* spot/twaalgos/sbacc.cc: If the initial state is in a rejecting
component, start with an initial state whose colors are unsat_mark.
* tests/core/sbacc.test: Add test case.
* tests/python/pdegen.py: Adjust it.
