* doc/Makefile.am: Here.

* doc/org/init.el.in, doc/org/syntax.css: New files.
* configure.ac: Generate init.el from init.el.in, and check for
emacs.
* doc/Makefile.am: Build userdoc/ from org/ and distribute userdoc/.
* README: Mention org/ and userdoc/.

* doc/org/tools.org: Update to 1.0.2.
* doc/org/ltl2tgba.org: Mention monitors in the intro.

* doc/org/ioltl.org: Mention ltl2dstar and the changes to the prefix
parser.
* doc/org/ltlcross.org: Mention bench/ltl2tgba/sum.py.
* doc/org/tools.org: Bump version number.

* doc/org/.dir-locals.el: New files.
* doc/Makefile.am (EXTRA_DIST): Distribute it.

* doc/org/.gitignore, doc/org/genltl.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltlfilt.org, doc/org/randltl.org, doc/org/tools.org: New files.

* iface/dve2/dve2check.cc: Adjust.
* iface/dve2/README: Some (unrelated) typos.

This perform pre- and post-processings in addition to
the LTL-to-TGBA translation.

* src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/postproc.hh: Make the private part protected, so
that we can inherit from that in the translator class.
* src/bin/ltl2tgba.cc: Use the translator class to hide LTL
simplification, translation, and postprocessings.
* NEWS: Mention it.

* src/bin/ltl2tgta.cc: Honor -x.
* src/bin/man/ltl2tgta.x, src/bin/man/spot-x.x: Add cross references.

* src/bin/spot-x.cc, src/bin/man/spot-x.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust.
* src/bin/man/ltl2tgba.x: Remove all fine-tuning options,
and make a reference spot spot-x (7).
* src/bin/common_setup.hh, src/bin/common_setup.cc: Add
a misc_argp_hidden version of the option, so that --help
and --version are not shown in the --help output used
by help2man to generate spot-x.7.
* src/bin/ltl2tgba.cc: Refer to spot-x.7.

* src/tgbaalgos/simulation.cc: Attempt to fix several cases.
* src/tgbatest/sim.test: Add more tests.
* src/tgbatest/sim2.test: New file.
* src/tgbatest/Makefile.am: Add it.

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add an
scc-filter option.
* src/bin/man/ltl2tgba.x: Document it.

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a
"simul-limit" option, and add two new cases to "simul"
for the two don't care simulation
* src/bin/man/ltl2tgba.x: Mention the new options.

Thomas Badie authored Sep 27, 2012 and Alexandre Duret-Lutz committed Apr 09, 2013

* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Add bdd_print_isop
that prints the bdd into a Irreductible Sum Of Product.
* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Add a way to
know which states (in the input) is which (in the result).
* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Add
the Don't Care Simulation and the Don't Care Iterated Simulation.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/spotlbtt.test,
src/tgbatest/Makefile.am, src/tgbatest/sim.test: Test them.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/README,
bench/ltl2tgba/algorithms: Add a way to bench the don't care
simulation.

* src/tgbaalgos/postproc.hh, src/tgbaalgos/postproc.cc: Honor the
"simul" option in the option_map.
(do_simul, do_degen): New method to wrap the algorithms that may be
altered via option_map.
* src/bin/man/ltl2tgba.x (simul): Document this option.

* src/tgbaalgos/sccfilter.cc: Compute useless variable SCC-wise, then
renumber the useful variables so that they can be shared between SCCs.
* src/tgbatest/sccsimpl.test, src/tgbatest/ltl2ta.test: Adjust test
cases.

* src/tgbaalgos/postproc.cc: Add an option_map parameter, and use to get
extra options to pass to the degeneralization algorithm.
* src/tgbaalgos/postproc.hh: Adjust prototype, and store Boolean
variables for degeneralize() options.
* src/bin/ltl2tgba.cc: Add a -x option to fill the option map, and pass
it to the postprocessor.
* src/bin/man/ltl2tgba.x: Document the three degeneralization options.

* src/tgbaalgos/degen.cc (degeneralize): Do not call i->current_state()
to get the current SCC, as we already have the state in d.first.

Because benchmark show that this option usually do not help.

* src/tgbaalgos/degen.hh, src/tgbatest/ltl2tgba.cc: Here.
* src/tgbaalgos/degen.hh: Document the new options.

* src/tgbaalgos/degen.cc: Fixups.
* src/tgbatest/ltl2tgba.cc: Add switches to enable/disable
the options Tomáš added to degeneralize().

Tomáš Babiak authored Dec 05, 2012 and Alexandre Duret-Lutz committed Apr 09, 2013

* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: Add three
options use_z_level, use_cust_acc_orders, and use_lvl_cache.

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

When something like XFa & FXa is reduced, the subformulae XFa and FXa
are both rewritten separately to XFa, and then the vector of arguments
of the And operators, [XFa,XFa], is passed through a specialized loop
that searches of the form X(...) that can potentially be simplified with
some other terms.  This loop converts the vector [XFa,XFa] into the set
{XFa,XFa}={XFa} and forgot to deal with the case where the insertion
would actually not add an existing subformula.

* src/ltlvisit/simplify.cc: Fix the code for Or, and And.
* src/ltltest/reduc0.test: New file, to test it.
* src/ltltest/Makefile.am (TESTS): Add it.
* src/ltltest/reduccmp.test: Add an extra test that does not
trigger the bug (because reduccmp.test uses more than basic
optimizations, and the implication-based simplifications are
already able to detect that XFa and FXa are equivalent).

* NEWS, configure.ac: Bump version.

* src/ltlvisit/simplify.hh (ltl_simplifier_options): add
a boolean_to_isop option
(ltl_simplifier::boolean_to_isop): New method.
* src/ltlvisit/simplify.cc: Implement these.
* src/bin/ltlfilt.cc: Add a --boolean-to-isop option.
* src/ltltest/isop.test: New file.
* src/ltltest/Makefile.am: Add it.
* NEWS: Mention it.

* wrap/python/ajax/spot.in (print_stats): Do not call
sub_stats_reachable on testing automata.

* src/tgbaalgos/postproc.hh (run): Rename the first argument as
input_disown to help Swig.
* wrap/python/spot.i: Wrap spot::postprocessor.
* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add an option for nondeterministic monitor.
* wrap/python/ajax/spot.in: Honor the new option, and rewrite the
monitor production using postprocessor.

* src/tgbatest/ltl2tgba.cc: Calling tgbatest/ltl2tgba -M -O (which
makes no sense, but that is no reason) used the "minimized" variable
for two automata, overwriting one.
* wrap/python/spot.i: The python bindings did not know about
sba_explicit automata, causing memory leaks, and complaints from the
bdd_dict.