* spot/twaalgos/determinize.cc: Here.

* spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
tests/core/safra.cc (tgba_determinisation): Rename as...
(twa_determinisation): ... this.

* spot/twaalgos/determinize.hh: Add documentaion and rename options.
* spot/twaalgos/determinize.cc: Rename options as well.

bisimulation and complete just trigger extra algorithms to be called at
the end of this one, so they need not be part of this algorithm.

* spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh: Reduce
the number of options.
* tests/core/safra.cc: Implement those options here.

* spot/twaalgos/determinize.hh: Move class definitions...
* spot/twaalgos/determinize.cc: ... here.

* spot/twaalgos/safra.cc, spot/twaalgos/safra.hh: Rename as...
* spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh: ... these.
* spot/twaalgos/Makefile.am, tests/core/safra.cc: Adjust.

Alexandre Lewkowicz authored Feb 05, 2016 and Alexandre Duret-Lutz committed Feb 12, 2016

* spot/twaalgos/safra.cc, spot/twaalgos/safra.hh: Here.
* tests/core/safra.cc: Add option.

Alexandre Lewkowicz authored Feb 04, 2016 and Alexandre Duret-Lutz committed Feb 12, 2016

* spot/twaalgos/safra.cc, spot/twaalgos/safra.hh:  Enables use to
compute successor safra state for any edge.

Alexandre Lewkowicz authored Feb 04, 2016 and Alexandre Duret-Lutz committed Feb 12, 2016

* spot/twaalgos/safra.cc: Here.

Alexandre Lewkowicz authored Feb 04, 2016 and Alexandre Duret-Lutz committed Feb 12, 2016

* spot/twaalgos/safra.cc, spot/twaalgos/safra.hh: Here.

Alexandre Lewkowicz authored Jan 14, 2016 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/twaalgos/safra.cc,
src/twaalgos/safra.hh, src/tests/safra.test: Rename as...
* spot/twaalgos/safra.cc, spot/twaalgos/safra.hh, tests/core/safra.cc
tests/core/safra.test: ... these.
* tests/Makefile.am: Update.

Alexandre Lewkowicz authored Nov 11, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/twaalgos/safra.cc,
src/twaalgos/safra.hh, spot/twaalgos/simulation.cc,
spot/twaalgos/simulation.hh: Here.

Alexandre Lewkowicz authored Nov 09, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/twaalgos/safra.cc: Here.

Alexandre Lewkowicz authored Sep 24, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/tests/safra.test: Update it.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: all nodes in a safra
state are grouped by SCC. This is done by putting them in different
braces.  The same SCC can have different ids depending on the safra
state.

Alexandre Lewkowicz authored Sep 24, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.

Alexandre Lewkowicz authored Sep 23, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.test: Update it.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Acceptance is now MIN
ODD.  We only track runs within an SCC and only consider accepting SCC.

Alexandre Lewkowicz authored Sep 23, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/twaalgos/safra.cc: Here.

Alexandre Lewkowicz authored Sep 22, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc:  Add option.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh:  When a node leaves an
SCC, all the subpaths of that node are removed.

Alexandre Lewkowicz authored Sep 22, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

*  src/twaalgos/safra.cc, src/twaalgos/safra.hh: Implement optimisation.
Update function calls with new API.
* src/tests/safra.cc, src/tests/safra.test: Use new API.

Alexandre Lewkowicz authored Jun 06, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/twaalgos/safra.cc,
src/twaalgos/safra.hh: Here.

Alexandre Lewkowicz authored May 30, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/tests/safra.test: Add options and test.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.

Alexandre Lewkowicz authored May 28, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.

Alexandre Lewkowicz authored May 28, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc:  Output error message for wrong ltl formula.
* src/twaalgos/safra.cc:  Default comparision of vector does not
correspond to the desired comparision.

Alexandre Lewkowicz authored May 27, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/tests/safra.test:  Use HOA format in tests.
* src/twaalgos/safra.cc:  Make sure the number of sets are always odd so
that cycles without any acceptance set are rejected.

Alexandre Lewkowicz authored May 25, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/tests/safra.test:  Update results.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: The use of transitions
resulted in non deterministic automata.  By using sub-transitions the
problem is solved.

Alexandre Lewkowicz authored May 25, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/tests/safra.test:  Update it.
* src/twaalgos/safra.cc: Here;

Alexandre Lewkowicz authored May 21, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.

Alexandre Lewkowicz authored May 19, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/tests/safra.cc, src/tests/safra.test: New.

Alexandre Lewkowicz authored May 19, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/twaalgos/safra.cc, src/twaalgos/safra.hh:  Note that the created
automaton is not a true parity automaton as they are not handled yet
by Spot.

Alexandre Lewkowicz authored May 13, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.

Alexandre Lewkowicz authored May 08, 2015 and Alexandre Duret-Lutz committed Feb 12, 2016

* spot/twaalgos/Makefile.am: Update it.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: New.

Those had been incorrectly renamed to buddy/spot/.libs when we rename
the main src/ directory into spot/.  This only affected the setting of
DYLD_LIBRARY_PATH, that used to be needed on Darwin.

* doc/org/.dir-locals.el.in, doc/org/init.el.in, python/ajax/spotcgi.in,
tests/run.in: Fix the PATH.

"1 U (a | Fb)" was not always reduced to "F(a | b)".

Fixes #143.

* spot/tl/simplify.cc: Add the missing recurse() call.
* tests/core/reduc0.test: Add a test.
* NEWS: Mention the bug.

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

Fixes #142, reported by Joachim Klein.

* bin/autfilt.cc, bin/ltlfilt.cc, bin/randaut.cc, bin/randltl.cc: Make
sure all global variables that have a destructor are destructed in the
main.  Otherwise they risk being destructed after the library's global
structures are destructed, causing access to freed memory.
* NEWS: Mention the bug.

* spot/twaalgos/emptiness.hh, spot/twaalgos/emptiness.cc: Add
the method.
* tests/python/highlighting.ipynb: Add a small test.

This fixes the output gliches visible in the previous patches,
where highlighting a state would remove its fill color.

* spot/twaalgos/dot.cc, spot/taalgos/dot.cc: Implement option C(COLOR).
* bin/common_aoutput.cc, doc/org/oaut.org: Document it.
* doc/org/.dir-locals.el.in, doc/org/init.el.in,
python/spot/__init__.py: Use it.
* tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/highlighting.ipynb: Test it.
* tests/core/readsave.test: Adjust.
* NEWS: Mention recent changes.