* src/tgbaalgos/dotty.cc: Fix output of unreachable states.
* src/tgbatest/readsave.test: Add test.

ltl3ba 1.1.0 was released today

* wrap/python/ajax/spot.in: Use -T3 instead of -U.
* wrap/python/ajax/README: Adjust version.
* wrap/python/ajax/ltl2tgba.html: Turn on improved determinism
of ltl3ba by default.
* bench/ltl2tgba/tools, bench/spin13/run.sh: Adjust options.
* bench/spin13/README: Mention the update.

Fixes #52.

* src/ltltest/consterm.cc, src/ltltest/kind.cc: Rewrite to read a list
of input and expected output.
* src/ltltest/kind.test, src/ltltest/consterm.test: Adjust.

Otherwise autfilt will not start processing input automata before its
input buffer is full.

* src/hoaparse/hoascan.ll: Here.

* src/tgbaalgos/simulation.cc: Here.
* src/tgbatest/det.test: Test it.

* src/hoaparse/hoaparse.yy: If we have multiple initial states, but
one of them has no incoming edge, use this state instead of the fake
initial state we normally add.
* src/tgbatest/hoaparse.test: Add test case.

* src/tgbaalgos/dotty.cc: Do not output marked states if
an automaton has 0 acceptance set (like a monitor).
* src/tgbatest/monitor.test, src/tgbatest/dstar.test: Adjust.

and also set prop_state_based_acc() on input

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Add tests.

Report from Tomáš Babiak.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Add example from a development version
of ltl3ba.

Fixes #45.

* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Remove unused code.

Issue #45.

* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Take
a tgba_digraph is input.
* src/tgbatest/ltl2tgba.cc: Adjust.

Those where never really publicized because they were slow and we failed
to fix what we hopped to fix with them.  They where never used by
default.  Getting rid of them will make it easier to cleanup the
simulation code.

* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Remove
the simulation code.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
src/tgbatest/ltl2tgba.cc: Do not call it.
* src/bin/spot-x.cc: Update doc.
* src/tgbatest/sim.test: Delete this file.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/spotlbtt.test, bench/ltl2tgba/tools.sim:
Remove uses to don't care simulation.

For issue #51.

* wrap/python/ajax/ltl2tgba.html: Here.

and adjust it to detect siPSL formulas, as in the paper of Dax et
al. (ATVA'09).  For issue #51.

* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc: Rename
the property, and adjust its computation on siSERE.
* src/ltlvisit/remove_x.cc, src/ltlvisit/simplify.cc,
src/tgbaalgos/stutter.cc: Adjust to new names.
* src/bin/ltlfilt.cc: Add option --syntactic-sutter-invariant.
* src/ltltest/kind.test: Update tests and add some new.

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.

* doc/tl/tl.tex: Use "formulas" everywhere in this file.

* src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Here.
* src/tgbatest/ltl2tgba.cc: Remove option -k.
* src/tgbatest/sccsimpl.test: Move the only -k test...
* src/tgbatest/scc.test:... here.

Fixes #49.

* src/tgbatest/scc.test: Rewrite using ltl2tgba --stats.

Fixes #50.

* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh: Rewrite using
unsigned instead of state*, and std::vector instead of std::map.
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/powerset.cc: Adjust.

This fixes #44.

* src/bin/ltlfilt.cc: Implement -n/--max-count.
* doc/org/ltlfilt.org, src/tgbatest/randpsl.test: Use it
* NEWS: Document it.

* src/bin/ltlfilt.cc: Remove short option -n for --negate.

* src/tgbaalgos/neverclaim.cc: Make sure the any accepting initial state
is not output as an accept_all state.  This bug caused ltl2dstar.test to
fail.

Because -s can now take arguments.

* src/tgbatest/ltl2dstar2.test: Here.

* src/tgbaalgos/minimize.cc (minimize_monitor): Simplify the call to
tgba_powerset.

This helps issue #26 considerably, but I'm not closing it because there
are a few places here and there that can be cleaned up.  For instance
build_state_set in minimize.cc should be rewritten.

* src/misc/bitvect.hh (bitvector_array::clear_all): New method.
* src/tgbaalgos/powerset.cc (tgba_powerset): Rewrite it.
* src/tgbaalgos/powerset.hh (power_map): Simplify.

* src/tgbaalgos/powerset.cc: Replace std::deque by vector, and take
the return of aut->out(s) by reference.

* src/tgbaalgos/powerset.cc: Use bdd_implies.

* src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh: Rewrite
using the tgba_digraph interface.
* src/tgbatest/ltl2tgba.cc: Adjust call.

* src/ltltest/equals.cc: Delete.
* src/ltltest/Makefile.am: Adjust.
* src/ltltest/unabbrevwm.test: Rewrite using ltlfilt.

Fixes #46.

* src/tgbaalgos/neverclaim.cc: Add option '6'.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Make it
possible to use the option.
* NEWS, doc/org/oaut.org: Document it.
* src/tgbatest/ltlcross2.test: Test it.

* src/tgbaalgos/postproc.cc: Here.  Otherwise, reading
a neverclaim with autfilt would loose the SBA property
and degeneralize again.

* src/tgbaalgos/degen.cc: Here.

* src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh: Here.
Also take a string to supply options.
* src/tgbatest/ltl2tgba.cc: Adjust call.

Fixes #48.

* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh: Here.
* src/tgbaalgos/minimize.cc: Adjust usage.

* doc/org/oaut.org: Show another way to perform the last computation.

* src/sanity/style.test: Check for it.
* src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
src/tgbaalgos/randomize.cc, src/tgbaalgos/stutter.cc: Fix all those.

The namespace dstaryy was declared inline and then reopened as
non-inline.  Likewise for hoayy.  Let's use different names.

* src/dstarparse/dstarparse.yy, src/hoaparse/hoaparse.yy: Here.

* src/ltlvisit/randomltl.cc: Make sure generation of binary operator is
done in a deterministic order.

* src/ltlvisit/mutation.cc: Force order of evaluation of arguments of
binops.