This way we can easily parse a stream of HOAs intermixed with
neverclaims.
* src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll: Add rules
for neverclaims, adjusted from src/neverparse/neverclaimparse.yy
and src/neverparse/neverclaimparse.ll.
* src/hoaparse/public.hh, NEWS: Update documentation.
* src/neverparse/: Remove this directory.
* README, configure.ac, src/Makefile.am: Adjust accordingly.
* src/tgbatest/ltl2tgba.cc, src/bin/ltlcross.cc: Use HOA
parser to read neverclaims.
* src/tgbatest/hoaparse.test, src/tgbatest/neverclaimread.test: Adjust.
* src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh:
Add closure function.
* src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh:
Add two implementations of "self-loopize" function.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgba/tgbasl.cc, src/tgba/tgbasl.hh: On-the-fly implementation of
self-loopize.
* src/tgba/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/stutter_invariant.test: Test
closure and sl.
* src/tgbatest/Makefile.am: Adjust.
* src/bin/ltlfilt.cc: Modify stutter-invariant option to use
automaton-based checking rather than syntactic-based checking.
* src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh:
Remove is_stutter_insensitive function.
* src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh: Check if a formula is
stutter-invariant using closure and sl.
* wrap/python/spot.i: Add closure and sl bindings.
* bench/stutter/stutter_invariance_formulas.cc: Generate benchmarks from
given formulas.
* bench/stutter/stutter_invariance_randomgraph.cc: Generate benchmarks
from random automata.
* bench/stutter/Makefile.am: Add them.
* configure.ac: Add bench/stutter/Makefile.
* bench/Makefile.am: Add stutter subdirectory.
* README: Document bench/stutter directory.
This was never actually used and we have a new implementation of
alternating automata coming.
* src/saba/, src/sabaalgos/, src/sabatest/: Remove.
* src/Makefile.am, configure.ac, README: Adjust.
* NEWS: Mention it.
These were used in old experiments, but have not turned useful in
practice. Not worth keeping and maintaining.
* src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Delete.
* bench/scc-stats/, bench/split-product/: Delete.
* configure.ac, src/tgbaalgos/Makefile.am, README, bench/Makefile.am:
Adjust.
It hasn't been tested for several year, may not even compile, has
to be linked with source code that isn't even publicly available,
and its presence was the only reason to keep some inefficient
code in gtec.cc and friends.
* iface/gspn/: Delete this directory.
* iface/Makefile.am, configure.ac, README: Adjust.
* m4/gspnlib.m4: Delete.
* src/sanity/Makefile.am: Do not use LIBGSPN_CPPFLAGS.
* src/misc/random.cc, src/misc/random.hh (srand, drand, mrand, rrand,
barand): Simplify using <random> from C++11.
(nrand, bmrand, prand): Remove these unused functions.
* src/tgbaalgos/randomgraph.cc: Adjust the use of barand.
* configure.ac: Do not check for srand48 and drand48.
We still want to remain compatible with Bison 2.7 so instead of fixing
all the new errors reported by 3.0 we silence some warning. We should
fix these for good once Bison 3.0 is more widespread.
* m4/bison.m4: New file. Test if bison support -Wno-empty-rule and
-Wno-deprecated. Define BISON and BISON_EXTRA_FLAGS.
* configure.ac: Do not test for yacc, use the above test instead.
* src/dstarparse/Makefile.am, src/eltlparse/Makefile.am,
src/kripkeparse/Makefile.am, src/ltlparse/Makefile.am,
src/neverparse/Makefile.am, src/tgbaparse/Makefile.am: Use BISON
and BISON_EXTRA_FLAGS.
* src/ltlparse/ltlparse.yy: Fix or and remove useless %right/%nonassoc
settings.
* src/eltlparse/eltlparse.yy: Likewise, and remove "%pure-parser".
* configure.ac: Check for flags and fill CXXFLAGS and CFLAGS.
* iface/dve2/dve2.hh: Mark load_dve2 for export.
* src/eltlparse/Makefile.am, src/kripke/Makefile.am,
src/kripkeparse/Makefile.am, src/ltlast/Makefile.am,
src/ltlenv/Makefile.am, src/ltlparse/Makefile.am,
src/ltlvisit/Makefile.am, src/misc/Makefile.am,
src/neverparse/Makefile.am, src/priv/Makefile.am, src/saba/Makefile.am,
src/sabaalgos/Makefile.am, src/ta/Makefile.am, src/taalgos/Makefile.am,
src/tgba/Makefile.am, src/tgbaalgos/Makefile.am,
src/tgbaalgos/gtec/Makefile.am, src/tgbaparse/Makefile.am:
Remove $(VISIBILITY_CXXFLAGS) now that it is set globally.
* configure.ac: Check for -fvisibility support.
* m4/ax_check_compile_flag.m4: New file.
* src/misc/common.hh: New file.
* src/misc/Makefile.am: Add common.hh, and adjust to use -fvisibility.
* src/misc/bareword.hh, src/misc/escape.hh, src/misc/formater.hh,
src/misc/intvcmp2.hh, src/misc/intvcomp.hh, src/misc/memusage.hh,
src/misc/minato.hh, src/misc/optionmap.hh, src/misc/random.hh,
src/misc/timer.hh, src/misc/version.hh, src/misc/bddop.hh: Include
common.hh and add SPOT_API tags.
* src/misc/acccompl.hh, src/misc/accconv.hh: Prepare for upcoming
move.
* src/sanity/style.test: Ignore SPOT_API tags.
* wrap/python/Makefile.am: Ignore SPOT_API.
* wrap/python/spot.i: Do not emit binding for bddalloc.hh.
* wrap/python/tests/minato.py: Do not use bdd_allocator.
