Fixes#39, reported by Joachim Klein.
* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Take an option
to specify which of xor/equiv/implies should be rewritten.
* src/ltlvisit/print.cc (print_spin): Rewrite only xor.
* src/tests/ltlfilt.test: Add a test case.
* NEWS: Mention this.
* src/twa/twagraph.hh (namer): Use a template alias instead
of a trait.
* src/twa/twagraph.cc, src/parseaut/parseaut.yy,
src/twaalgos/ltl2tgba_fm.cc: Adjust.
We do not remove them in rejecting SCCs (as it might make the SCC
accepting), but we can remove them between SCCs.
Fixes#101.
* src/twaalgos/sccfilter.cc: Here.
* src/tests/sccsimpl.test: Add test case.
* NEWS: Mention this.
* src/ltlvisit/print.cc: Property output the double
quotes in latex mode, not only sclatex.
* src/misc/escape.cc: Fix LaTeX escape to work in math mode.
* src/tests/latex.test: Add a test.
* wrap/python/tests/formulas.ipynb: Adjust expected output
* NEWS: Mention the fix.
Fixes#100.
* doc/org/tut.org: Link to the notebook.
* src/sanity/ipynb.test: New test, to make sure we do not forget
to document ipython notebook when we add some.
* src/sanity/Makefile.am: Add it and run it.
* NEWS: Mention it.
* src/bin/man/autfilt.x, src/bin/man/dstar2tgba.x,
src/bin/man/ltl2tgba.x, src/bin/man/ltlcross.x,
src/bin/man/ltlgrind.x, src/bin/man/randltl.x, src/bin/man/spot-x.x:
Improve typesetting and cross-references.
* tools/help2man: Adjust to better detect the optional arguments.
Detect options that are not separated from their description by two
spaces. Argp output some of those.
* tools/man2html.pl: New file.
* Makefile.am: Distribute it.
* src/bin/ltlfilt.cc: Fix description of --define.
* src/bin/ltlgrind.cc: Fix duplicate description for --help and
--version. Reorder --help output slightly.
* NEWS: Mention the few fixes.
* src/twaalgos/hoa.cc: Here.
* src/tests/readsave.test: Test it.
* NEWS: Mention it.
* src/twaalgos/dot.cc, src/twaalgos/neverclaim.cc: Fix the
error message.
Fixes#99.
* src/tests/parseaut.test: New test case.
* src/twa/acc.cc (is_generalized_rabin): Fix detection
of Fin(0)|Fin(1)|Fin(2)&Inf(3).
* NEWS: Mention it.
Also change http:// to https:// for url that would automatically
redirect to the later.
* doc/mainpage.dox, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org,
doc/org/ltlcross.org, doc/org/satmin.org, doc/org/tools.org,
src/ltlvisit/dot.hh, src/misc/hashfunc.hh, wrap/python/ajax/trans.html:
Here.
* src/twaalgos/totgba.hh, src/twaalgos/totgba.cc: Implement
the new function.
* NEWS: Mention this new function.
* src/bin/man/spot-x.x: Document SPOT_STREETT_CONV_MIN.
* src/tests/ltl2dstar4.test: Add tests.
* src/tests/Makefile.am: Add it.
* src/bin/autfilt.cc: Do do call remove_fin explicitely
when --tgba is used, let the postprocessor do it.
* src/twa/acc.hh: Add shift operators for acceptance marks.
* src/twaalgos/remfin.cc: Use the new algorithm.
* src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Add
a new method to supply the acceptance sets visited by an SCC.
The command in #96 now takes 1min 16s.
* src/twaalgos/sccinfo.cc: Only gather successor SCCs when popping an
SCC.
* wrap/python/tests/automata.ipynb: Adjust.
They are unused.
* src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Do
not keep track of conditions between two SCCs.
* src/twaalgos/minimize.cc, src/twaalgos/ltl2tgba_fm.cc:
Adjust.
* src/twaalgos/sccfilter.cc (acc_filter_some, acc_filter_all): Merge
into...
(acc_filter_mask): ... this single parametrized class, and only
remove sets that are only used as Inf.
* src/twa/acc.hh: Add missing operator~.
* src/tests/sccsimpl.test: Add test case.
* src/tests/sccdot.test: Adjust.
* NEWS: Mention the bug.
* src/misc/bareword.hh, src/misc/bitvect.hh, src/misc/escape.hh,
src/misc/hashfunc.hh, src/misc/intvcmp2.hh, src/misc/intvcomp.hh,
src/misc/random.hh, src/misc/timer.hh, src/misc/tmpfile.hh: Use ingroup
rather than addtogroup.
Because this parser is not specific to HOA anymore.
* src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
src/hoaparse/hoaparse.yy, src/hoaparse/parsedecl.hh,
src/parseaut/public.hh, src/hoaparse/hoascan.ll,
src/tests/hoaparse.test: Rename to...
* src/parseaut/Makefile.am, src/parseaut/fmterror.cc,
src/parseaut/parseaut.yy, src/parseaut/parsedecl.hh,
src/hoaparse/public.hh, src/parseaut/scanaut.ll,
src/tests/parseaut.test: ... these, and also adjust the name internally.
For instance hoa_aut_ptr is now parsed_aut_ptr; hoa_stream_parser is now
automaton_stream_parser, and hoa_parse() has become parse_aut().
* NEWS, README, configure.ac, doc/org/tut20.org, src/Makefile.am,
src/bin/autfilt.cc, src/bin/common_aoutput.cc,
src/bin/common_aoutput.hh, src/bin/common_conv.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/Makefile.am,
src/tests/complementation.cc, src/tests/ltl2tgba.cc,
src/tests/readsave.test, wrap/python/ajax/spot.in,
wrap/python/spot.py, wrap/python/spot_impl.i,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/parsetgba.py:
Adjust.
* src/twaalgos/lbtt.hh (print_lbtt): Take a const char* opt argument.
* src/twaalgos/lbtt.cc: Use it, select state-based
vs. transition-based using automaton property, and implement output
for generalized state-based acceptance.
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/dstar2tgba.cc: Adjust usage. We do not need to handle
--lbtt=t as a special case anymore.
* src/tests/lbttparse.test, wrap/python/spot.py,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb:
Adjust.
This addresses one item in #14.
* doc/org/tut10.org: New file.
* doc/Makefile.am: Add it.
* src/twaalgos/translate.hh: Fix inclusion of types from
postprocessor.
* wrap/python/spot.py (translate): Fix typo in doc string.
This fixes#61, and addresses one item of #14.
* src/ltlvisit/relabel.hh: Use a map rather than a unordered_map,
because the Swig binding for unordered_map do not seem functional.
* wrap/python/spot_impl.i: Adjust.
* wrap/python/tests/relabel.py: New file.
* wrap/python/tests/Makefile.am: Add it.
* doc/org/tut02.org: New file.
* doc/Makefile.am: Add it.
