The previous implementation was fine to catch timeout of third-party
tools (like dot), but to good to catch timeout in Spot itself, because
Python will not deliver a SIGALRM while a native function (e.g. Spot's
translation) is running.  So we fork() the Python process, with a
parent that does nothing but wait for the termination of the child or
for an alarm.  On SIGALRM, the parent kills all children.

* wrap/python/ajax/spot.in: Adjust to fork.
* wrap/python/tests/alarm.py: New test file to test this
scenario in a more controled environment.
* wrap/python/tests/Makefile.am: Add it.

* configure.ac, NEWS: Bump version number.

* src/tgbaparse/public.hh: Hide tgba_parse_errorlist to SWIG.
* wrap/python/spot.i: Export tgba_parse.
* wrap/python/tests/parsetgba.py: New file.
* wrap/python/tests/Makefile.am: Add it.

This is motivated by the fact that sog-its used the low-level data
structures used by the bdd_dict to do such work, and broke because of
the recent changes in this area.

* src/tgba/bdddict.cc, src/tgba/bdddict.hh (oneacc_to_formula):
New method.
* src/tgbaalgos/save.cc: Use it.

Doing so will release all BDD variables used by automata created for
syntactic implication.  This way the main translation will create
acceptance variables again in a more natural order, which will help
the degeneralization (until we get a better degeneralization).

* src/ltlvisit/contain.cc, src/ltlvisit/contain.hh
(language_containment_checker::clear): New method to clear the
containment cache.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
(clear_as_bdd_cache): Also call language_containment_checker::clear.

* m4/lbtt.m4: Check version number.

* configure.ac: Bump the version number to 1.2.1a.
* NEWS: Summarize all changes since 1.2.1.
* README: Warn this is not 1.2.1, and add pointers to NEWS and
ChangeLog.

* bench/ltl2tgba/parseout.pl: Adjust to output nondeterministic
indices and number of nondeterministic automata.
* bench/ltl2tgba/README: Update explanations.

Tomáš Babiak authored May 21, 2012 and Alexandre Duret-Lutz committed May 21, 2012

* src/BuchiAutomaton.h, src/BuchiAutomaton.cc
(BuchiState::isDeterministic, BuchiAutomaton::isDeterministic,
BuchiAutomaton::nondeterminismIndex): New methods.
* src/TestOperations.cc (generateBuchiAutomaton): Collect
nondeterminism indices, and count deterministic automata.
* src/TestStatistics.cc, src/TestStatistics.h: Add storage
for these statistics.
* src/StatDisplay.cc (printBuchiAutomatonStats,
printCollectiveStats): Display these statistics.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
Simplify promises by replacing P(a U b), P(b M a), and P(Fb), by P(b).

This cause double-circles for accepting states in dot output.

* src/tgbatest/ltl2tgba.cc: Set assume_sba for automata read from
neverclaims.  Reset assume_sba after scc_filter and simulation.
* src/tgbatest/neverclaimread.test: Expect a double circle.

Syntactic implication checks may use as_bdd() to compare Boolean
formulae.  By doing so, they register Boolean variables in an order
that is usially detrimental to the LTL translator.  The new,
clear_as_bdd_cache() function offers a mean to unregister these
variables, so that the LTL translator will register them again in the
a more natural way.

* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
(clear_as_bdd_cache): New function.
* src/tgbatest/ltl2tgba.cc, wrap/python/ajax/spot.in: Call it.

* src/ltlvisit/simplify.cc
(ltl_simplifier_cache::syntactic_implication): If the lhs and rhs are
literals that are not equal, return false immediately.

* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh (print_stats):
New function.
* src/tgbatest/ltl2tgba.cc: Call it.

* src/tgbatest/ltl2tgba.cc: Fix mismatch between the help text,
documenting -rL, and the handling code, expecting -rs.

* src/tgbaalgos/ltl2tgba_fm.cc: Here.

* src/tgba/bdddict.hh, src/tgba/bdddict.cc: Store variable types and
associated formula in a vector indexed by BDD variable numbers,
instead of using several maps.
* src/evtgbaalgos/tgba2evtgba.cc, src/tgba/bddprint.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/save.cc: Adjust usage.

* src/tgbaalgos/ltl2tgba_fm.cc (implied_subforfmulae): New function.
(ltl_trad_visitor::visit(const binop*)): Use it.  This is an attempt
to correct the unoptimal translation of 'Fa & GFa' left by previous
patch.  It still fails to optimize 'Fa & GF(a&b)', but this is not a
regression compared to previous version.

* src/tgbaalgos/ltl2tgba_fm.cc: Add a "recurring" mode for the
translation of the child of G.  This generalizes Couvreur's original
trick to translate GFa as (a|Prom(a))&X(GFa) without generating an
intermediate GF(a)&F(a) state that would have to be merged with GF(a)
latter.  This implementation will also speedup formulas such a G((a U
b) & (c M d)).  With this patch, translating GF(p1) & GF(p2) &
... GF(p20) into a TGBA takes 57s instead of 128s on my computer.
However it alsos causes some formulas to be translated into larger
automata that are not immediately reduced (the simulation-reduction is
needed).  For instance Fa & GFa now has a different signature than
GFa, so translating 'Fa & GFa' generates two states where is used to
generate only one.

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/ltlparse/ltlparse.yy: Add new printers.  Suggested by Akim
Demaille.

* src/tgbatest/ltl2tgba.cc (syntax): Here.  Reported by Akim Demaille.

* src/ltlvisit/randomltl.cc: Use the correct flavor of And and Or.
Reported by Etienne Renault.
* NEWS: Mention the bug.

* configure.ac, NEWS: Bump version to 0.9.

* wrap/python/ajax/ltl2tgba.html: Mention PSL.

* doc/tl/tl.tex, src/ltlvisit/simplify.cc: Fix the rule.
* src/ltltest/reduccmp.test, src/ltltest/syntimpl.test:
Add more tests.

Because only the configure macros of spot::srand() had been updated to
the introduction of _config.h, rand() was used even if drand48() was
available, and yet srand48() was being called by spot::srand().  The
consequence is that setting the seed with srand48() had not effect on
the value returned by rand().  Reported by Etienne Renault.

* src/misc/random.cc (drand): Fix configure macros used.

* THANKS, src/tgbaalgos/ltl2tgba_fm.cc: Here.

* src/ltlvisit/tostring.cc (spin_kw): Output X, not ().

* src/sanity/80columns.test: If the system cannot count unicode
characters, only search for long ascii lines.

* src/ltlvisit/simplify.cc (reduce_sere_ltl): Here.
* src/ltltest/reduccmp.test: Add a test case.