GitLab

Fixes #262, reported by Maximilien Colange.

* bin/common_output.cc, bin/common_aoutput.cc, bin/common_aoutput.hh:
Clear the set of atomic propositions if --stats=%[...]x was used.
* spot/twa/bdddict.cc: Release any formula associated to a BDD when it
is unregistered, do not wait for the dictionary's destruction.  This
was the main culprit for #262.
* tests/core/ltl2tgba.test: Add test cases.
* NEWS: Mention the bug.

The cache used in formula simplification will keep atomic propositions
defined between several translations, and may impact variable order.
Reported by Maximilien Colange.

* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc, spot/twaalgos/translate.hh (clear_cache):
New method.
* bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call it.
* spot/twaalgos/stats.cc: Do not keep a point to the formula after
printing statistics.
* tests/core/ltl2tgba.test: Add a test case.
* tests/core/readsave.test: Adjust one formula.
* NEWS: Mention the issue.

* tests/core/ltl2tgba.test: Add new test-case,
reported by Tomáš Babiak.
* NEWS: Mention the bug fixed by previous patch.

Fixing this bug alone revealed another bug: parsing never claim or LBTT
automata did not register APs.  So this fixes both bugs.

This is the first part of #170.

* spot/twa/twa.hh (register_aps_from_dict): New method.
* spot/parseaut/parseaut.yy: Call it for never claim and LBTT files.
* spot/twaalgos/stats.cc: Simplify using ap_vars().
* tests/core/ltl2tgba.test: Add a test case.
* NEWS: Mention the bugs.

Fixing this bug alone revealed another bug: parsing never claim or LBTT
automata did not register APs.  So this fixes both bugs.

This is the first part of #170.

* spot/twa/twa.hh (register_aps_from_dict): New method.
* spot/parseaut/parseaut.yy: Call it for never claim and LBTT files.
* spot/twaalgos/stats.cc: Simplify using ap_vars().
* tests/core/ltl2tgba.test: Add a test case.
* NEWS: Mention the bugs.

* bin/common_aoutput.hh, bin/common_aoutput.cc,
bin/ltl2tgba.cc, bin/ltldo.cc: Add support for %< and %>.
* tests/core/ltl2tgba.test, tests/core/ltldo.test: Test it.
* NEWS: Mention it.

* tests/: Rename as...
* tests/core/: ... this.
* python/tests/: Rename as...
* tests/python/: ... this.
* python/tests/run.in: Move as...
* tests/run.in: This, and adjust.
* tests/Makefile.am: Adjust to run both core and python tests.
* configure.ac, README, debian/python3-spot.examples, debian/rules,
doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.

* spot/bin/: Move...
* bin/: ... here.
* spot/tests/: Move...
* tests/: ... here.
* Makefile.am, README, bench/stutter/Makefile.am,
bench/stutter/stutter_invariance_formulas.cc, doc/Makefile.am,
configure.ac, debian/rules, spot/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/style.test, python/tests/run.in:
Adjust.

* 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.

* src/taalgos/stats.cc, src/taalgos/stats.hh
(tgba_statistics::transitions, tgba_sub_statistics::sub_transitions):
Rename ...
(twa_statistics::edges, twa_sub_statistics::transitions): ... to
these.
* NEWS: Mention it.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/checkta.cc, src/tests/complementation.cc,
src/tests/ikwiad.cc, src/tests/ltl2tgba.test,
src/tests/neverclaimread.test, src/tests/randtgba.cc,
src/tests/renault.test, src/tests/wdba2.test, src/twaalgos/dtbasat.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/stats.cc,
src/twaalgos/stats.hh, wrap/python/ajax/spotcgi.in: Adjust.

Fixes #23.

* src/tests/ltl2tgba.cc: Rename as ...
* src/tests/ikwiad.cc: ... this.
* src/tests/Makefile.am, src/tests/babiak.test, src/tests/checkta.cc,
src/tests/complementation.test, src/tests/cycles.test,
src/tests/dbacomp.test, src/tests/degendet.test,
src/tests/degenid.test, src/tests/det.test, src/tests/dfs.test,
src/tests/dstar.test, src/tests/dupexp.test, src/tests/emptchke.test,
src/tests/kv.test, src/tests/ltl2neverclaim-lbtt.test,
src/tests/ltl2neverclaim.test, src/tests/ltl2tgba.test,
src/tests/ltlcounter.test, src/tests/ltlcross.test,
src/tests/neverclaimread.test, src/tests/obligation.test,
src/tests/parseaut.test, src/tests/randaut.test,
src/tests/randpsl.test, src/tests/renault.test,
src/tests/satmin2.test, src/tests/sccsimpl.test, src/tests/sim2.test,
src/tests/simdet.test, src/tests/spotlbtt.test, src/tests/wdba.test,
src/tests/wdba2.test, bench/emptchk/README, bench/emptchk/defs.in,
bench/ltlclasses/run, bench/ltlcounter/run, bench/wdba/run: Adjust.

* src/Makefile.am, README, configure.ac: update references.
* src/tgbatest/: rename as...
* src/tests/: ...this!

* src/tgbaalgos/postproc.cc: Here.
* src/tgbatest/ltl2tgba.test: Make sure ltl2tgba -B 0 has one
acceptance set.

This is progress for #1.

* src/tgbatest/ltl2tgba.cc: Remove options -b and -X.  Change
-P to read HOA files instead.
* src/tgbatest/complementation.cc: Replace option -b by -H for
HOA output, and read files in HOA.
* src/tgbatest/complementation.test, src/tgbatest/cycles.test,
src/tgbatest/dbacomp.test, src/tgbatest/degenid.test,
src/tgbatest/dfs.test, src/tgbatest/emptchke.test,
src/tgbatest/ltl2tgba.test, src/tgbatest/renault.test,
src/tgbatest/satmin2.test, src/tgbatest/sccsimpl.test,
src/tgbatest/sim2.test: Adjust.

This operator is to ':' what [*i..j] is to ';'.

Part of issue #51.

* doc/tl/tl.tex: Document syntax, semantic, and trivial
simplifications.
* doc/tl/spotltl.sty: Add macros for new operators.
* src/ltlast/bunop.cc, src/ltlast/bunop.hh: Implement it.
* src/ltlast/multop.cc: Add some trivial simplifications.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse it.
* src/ltltest/equals.test, src/ltltest/latex.test,
src/tgbatest/ltl2tgba.test: Add more tests.
* src/ltlvisit/randomltl.cc: Output this operator in
random PSL formulas.
* src/ltltest/rand.test: Adjust.
* src/tgbaalgos/ltl2tgba_fm.cc: Add translation rules.
* src/ltlvisit/tostring.cc: Add pretty printing code.
* src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc: Adjust
switches.
* NEWS: Mention the new operator.

* src/bin/ltl2tgba.cc, src/bin/randaut.cc: Catch exceptions
in main loop.
* src/tgbatest/ltl2tgba.test, src/tgbatest/randaut.test: Test
errors with unknown --dot argument.

* src/tgbaalgos/dotty.cc: Specialize for tgba_digraph_ptr.
* src/tgba/tgbagraph.hh, src/tgbaalgos/dupexp.cc: Copy properties by
default when cloning an automaton.
* src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/ltl2tgba.test, src/tgbatest/monitor.test,
src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test: Adjust
tests.

This is a huge patch, that took over a month to complete.  The bit sets
are currently restricted to what 'unsigned can store', but it should be
easy to extend it to 'uint64_t' should we need it.

* NEWS: Update.
* src/tgba/acc.hh: New file.
* src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
* src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: Delete.  The KV
complementation is too slow to be used in practice, and I somehow broke
it during the conversion to bitsets.  The tgba->sgba conversion was only
used for the KV complementation, and should be better redone on
tgba_digraph_ptr should it be needed again.
* src/bin/ltlcross.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/nsa2tgba.cc, src/graphtest/tgbagraph.cc,
src/graphtest/tgbagraph.test, src/kripke/fairkripke.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.cc, src/kripke/kripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/misc/hash.hh, src/neverparse/neverclaimparse.yy, src/priv/accmap.hh,
src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgta.cc,
src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
src/taalgos/tgba2ta.cc, src/tgba/Makefile.am, src/tgba/fwd.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh,
src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/complete.cc,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/hoaf.cc,
src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/postproc.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reducerun.cc, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc,
src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
src/tgbaalgos/stripacc.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc,
src/tgbaalgos/weight.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/Makefile.am, src/tgbatest/complementation.cc,
src/tgbatest/complementation.test, src/tgbatest/degenlskip.test,
src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/emptchk.cc,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test,
src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test,
src/tgbatest/neverclaimread.test, src/tgbatest/randtgba.cc,
src/tgbatest/readsave.test, src/tgbatest/sim.test,
src/tgbatest/sim2.test, src/tgbatest/spotlbtt.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
iface/dve2/dve2.cc: Adjust or use to the new acceptance interface.

So that running valgrind is a lot more efficient.  Running
ltl2tgba.test using to take more than 15min.  We are now down to
25sec.

* src/tgbatest/checkpsl.cc: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.test: Adjust.

Replace it by a new degeneralize_tba(), that use the same tricks as
degeneralize().

* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: Delete.
* src/tgba/Makefile.am: Adjust.
* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: Implement
a degeneralize_tba() function sharing its code
with degeneralize().
* src/tgbatest/ltl2tgba.cc: Rename -D to -DT so that we can pass it the
same option as -DS.
* src/tgbatest/degenid.test, src/tgbatest/emptchk.test,
src/tgbatest/emptchke.test, src/tgbatest/ltlcounter.test,
src/tgbatest/ltlcross.test, src/tgbatest/spotlbtt.test,
src/tgbatest/ltl2tgba.test: Adjust.
* src/tgbatest/det.test, src/tgbatest/emptchk.test: Adjust numbers to
the smaller output.
* src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
src/tgbatest/randtgba.cc, src/tgbatest/complementation.cc,
wrap/python/spot.i, wrap/python/tests/ltl2tgba.py,
src/sabatest/sabacomplementtgba.cc: Adjust to the removal
of tgba_tba_proxy, using degeneralize_tba() if needed.

This translator algorithm is seldom used in practice because we work
with explicit automata everywhere, and this is only useful to build
symbolic automata.  Furthermore, the symbolic automata produced by this
algorithm are larger (when looked at explicitly) than those produced by
ltl2tgba_fm or other explicit translators.

The nice side effect of this removal is that we can also remove a lot of
supporting classes, that were relying a lot on BDDs.

* src/tgba/public.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbabddconcreteproduct.hh,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbabddfactory.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbatest/bddprod.test,
src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: Delete all these
files.
* bench/ltlcounter/Makefile.am, bench/ltlcounter/README,
bench/ltlcounter/plot.gnu, bench/ltlcounter/run, src/tgba/Makefile.am,
src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am,
src/tgbatest/cycles.test, src/tgbatest/dupexp.test,
src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltl2tgba.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlprod.cc, src/tgbatest/spotlbtt.test,
src/tgbatest/wdba.test, src/tgbatest/wdba2.test,
src/tgba/tgbaexplicit.hh, wrap/python/ajax/ltl2tgba.html,
wrap/python/ajax/spot.in, wrap/python/spot.i,
wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/ltl2tgba.test: Adjust.

* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case that is improved
by this.
* src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.test: Adjust.

This follows from a discussion with Ernesto Posse.

The semantics for the {...} operator we use in Spot comes from the
cl(...) operator defined by Dax et al. (ATVA'09).  This is slightly
different from the the way the PSL spec interprets a SERE used in the
context of a temporal formula (appendix B.3.1.1.2, item 7).

cl({a;b}[*]) would match any infinite word that starts with a;b, while
in PSL {a;b}[*] would match any infinite word that alternates a and b.

Spot documents that {SERE} in a temporal formula is interpreted like
cl(SERE) however it failed to ignore the empty prefix of SERE.  So
{{a;b}[*]} would match anything, because the empty word is a prefix of
any word, and is also accepted by {a;b}[*].  Some trivial identities
and basic rewritings were also wrongly considering these empty
prefixes as well.

This patch therefore fixes the translation and syntactic
simplification rules, to really ignore these empty prefixes.

In some future version it should probably be wise to rename this {...}
operator as cl(...), and use {...} for the semantics given in appendix
B.3.1.1.2 (item 7) of the PSL specs.

* src/ltlast/unop.cc: Fix trivial identities.  We have
{[*0]} = 0 and !{[*0]} = 1.
* src/ltlvisit/simplify.cc: Fix basic rewriting rules.
{e[*]} = {e} and !{e[*]} = !{e}.
* doc/tl/tl.tex: Adjust documentation.
* doc/tl/tl.bib (dax.09.atva): New entry.
* src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
infinite word for {e[*]} just because the empty
prefix is matched by e[*].
* src/tgbatest/ltl2tgba.test: Add a test case.
* NEWS: Mention it.
* THANKS: Add Ernesto.

* src/tgbaalgos/ltl2tgba_fm.cc: Typo.
* src/tgbatest/ltl2tgba.test: Add a test case.

* NEWS: Mention this.
* COPYING: Replace by GPL v3.
* src/sanity/style.test: Check files with the wrong license,
in case we forgot to update it during a merge.
* Makefile.am, bench/Makefile.am, bench/emptchk/Makefile.am,
bench/emptchk/defs.in, bench/emptchk/ltl-human.sh,
bench/emptchk/ltl-random.sh, bench/emptchk/pml-clserv.sh,
bench/emptchk/pml-eeaean.sh, bench/emptchk/pml2tgba.pl,
bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/known,
bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small,
bench/ltlclasses/Makefile.am, bench/ltlclasses/defs.in,
bench/ltlclasses/run, bench/ltlcounter/Makefile.am,
bench/ltlcounter/defs.in, bench/ltlcounter/run,
bench/scc-stats/Makefile.am, bench/scc-stats/stats.cc,
bench/split-product/Makefile.am, bench/split-product/cutscc.cc,
bench/split-product/pml2tgba.pl, bench/wdba/Makefile.am,
bench/wdba/defs.in, bench/wdba/run, configure.ac, doc/Makefile.am,
doc/dot.in, doc/tl/Makefile.am, ifac...

This helps reducing (p&XF!p)|(!p&XFp)|X(Fp&F!p) to (p&XF!p)|(!p&XFp).

* src/tgbaalgos/ltl2tgba_fm.cc: Adjust rewriting rules of X.
* src/tgbatest/ltl2tgba.test: Add a test case.

We need a marked version of !{r} to perform breakpoint unroling.

* src/ltlast/unop.cc, src/ltlast/unop.hh: Declare a NegClosureMarked
operator.
* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc,
src/tgbaalgos/ltl2tgba_fm.cc: Adjust to deal with NegClosureMarked
and NegClosure as apropriate.
* src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgba/formula2bdd.cc: Deal with NegClosureMarked in the same way as
we deal with NegClosure.
* src/tgbatest/ltl2tgba.test: More tests.
* src/ltltest/kind.test: Adjust.
* doc/tl/tl.tex: Mention the marked negated closure.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not
translate a subformula if we have already proved it useless in
a previous rational expression.
* src/tgbatest/ltl2tgba.test: Add an example, although that
test does not ensure the subformula is ignored early in the
translation.  I.e., it would still work without the patch.

This fixes a bug where {(a&!a)[=2]} was translated either into an
universal automaton (with simplification turned off) or in an
empty automaton (with simplification turned on).

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Trim
the automaton.
(ratexp_to_dfa::succ, ratexp_to_dfa::get_label): Deal with trimed
states.
(ltl_trad_visitor::visit(unop::Closure)): Likewise.
* src/tgbatest/ltl2tgba.test, src/ltltest/reduccmp.test: New test
cases.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit):
Use a different translating rule for E* if E accepts [*0].
* src/tgbatest/ltl2tgba.test: Add test case.

* src/ltlast/bunop.hh: Declare bunop::Goto
* src/ltlast/bunop.cc: Handle it.
* src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll: Add rules for [->min..max].
* src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Goto in
the translation.
* src/ltltest/equals.test: Test trivial identities.
* src/tgbatest/ltl2tgba.test: Test two more formulae using [->].

* src/ltlast/bunop.hh: Declare bunop::Equal
* src/ltlast/bunop.cc: Handle it.
* src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll: Add rules for [=min..max].
* src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Equal in
the translation.
* src/ltltest/equals.test: Test trivial identities
for [=min..max].
* src/tgbatest/ltl2tgba.test: Add new formulae to test.

* src/ltlast/bunop.cc (bunop::format): Output [*1..] as [+].
* src/ltlvisit/tostring.cc: Output "a*" as "a[*]" for consistency.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Recognize [+].
* src/ltltest/tostring.test, src/ltltest/equals.test,
src/tgbatest/ltl2tgba.test: More tests.

* src/ltlast/bunop.hh, src/ltlast/bunop.cc: New files for
bounded unary operators.
* src/ltlast/Makefile.am, src/ltlast/allnodes.hh: Add them.
* src/ltlast/predecl.hh (bunop): Declare.
* src/ltlast/unop.hh, src/ltlast/unop.cc (Star): Remove
declaration of Star and associated code.
* src/ltlast/visitor.hh: Add visit(bunop* node) methods.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Add parse
rules for LTL.  This required passing the parse_error list
to the lexer, so it can report scanning errors when it reads
a number that does not fit in an unsigned int.
* src/ltlparse/parsedecl.hh (YY_DECL): Take error_list
as third argument.
* src/ltltest/consterm.test, src/ltltest/tostring.test,
src/ltltest/equals.test, src/tgbatest/ltl2tgba.test: More tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/consterm.cc,
src/ltlvisit/dotty.cc, src/ltlvisit/mark.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/postfix.cc,
src/ltlvisit/postfix.hh, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Adjust syntax to use
"bunop::Star" instead of "unop::Star".
* src/tgbaalgos/ltl2tgba_fm.cc: Likewise, but also adjust
the code to handle the bounds of the operator.

* src/ltlparse/ltlparse.yy: Recognize "*" as "1*".
* src/ltlvisit/tostring.cc: Abbreviate "1*" as "*".
* src/tgbatest/ltl2tgba.test: Use the new syntax.

* src/ltlparse/ltlscan.ll: Recognize "[]=>" (a.k.a "|=>") and "<>=>".
* src/ltlparse/ltlparse.yy: Support them by rewriting them using
"[]->" and "<>->".
* src/tgbatest/ltl2tgba.test: More tests.

* src/ltlparse/ltlparse.yy (rationalexp): Recognize "OP_NOT
booleanatom".
* src/ltlvisit/consterm.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust.
* src/tgbatest/ltl2tgba.test: Add one test.

* src/ltlast/multop.cc, src/ltlast/multop.hh: Declare AndNML
operator.
* src/ltlparse/ltlscan.ll: Distinguish "&" and "&&".
* src/ltlparse/ltlparse.yy: Handle them both as "And" for LTL
formula, use AndNML or And for rational expressions.
* src/ltlvisit/tostring.cc: Adjust to distinguish "&" and "&&" in
rational expressions. Also use {braces} to group rational
expressions.
* src/tgbaalgos/ltl2tgba_fm.cc
(ratexp_trad_visitor::ratexp_trad_visitor): Remove the possibility
to select the empty_word should act like true, and fix the rules
for Closure and NegClosure to rely on constant_term instead.
(ratexp_trad_visitor::visit) Adjust the And translation to also
support AndNML.
(ratexp_trad_visitor::recurse_and_concat): Introduce this new
method to simplify some calls to recurse(f, to_concat_).
* src/tgbatest/ltl2tgba.test: Add more test cases.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/contain.cc, src/ltlvisit/mark.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/syntimpl.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Add
missing cases in switches.

* src/ltlparse/ltlscan.ll: Recognize [*] as *, and use
[*0] instead of #e for the empty word.
* src/ltlast/binop.cc, src/ltlast/constant.cc,
src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc,
src/ltlast/unop.hh, src/ltltest/consterm.test,
src/ltltest/equals.test: Adjust all occurrences of #e to [*0].
* src/tgbatest/ltl2tgba.test: Also use [*].

* src/ltlparse/ltlparse.yy (rationalexp): Allow bracedrationalexp.
* src/ltltest/consterm.test, src/tgbatest/ltl2tgba.test: Add more
tests.