* src/neverparse/neverclaimparse.yy, src/neverparse/neverclaimscan.ll:
Allow transitions between do..od, recognize atomic and assert.
* src/neverparse/parsedecl.hh: Pass the error_list to the lexer.
* src/tgbatest/neverclaimread.test: Add a test case.
If all the acceptance set of an SCC but the first one were useless, the
scc_filter() algorithm could abort with a BDD error because of a bug in
the logic.
* src/tgbaalgos/sccfilter.cc (scc_filter): Fix.
* src/tgbatest/sccsimpl.test: Add a test case supplied by Étienne
Renault.
* doc/Doxyfile.in: Update to Doxygen 1.8.4
* doc/footer.html: Point to the mailing list.
* doc/mainpage.dox: Point to spot::translator,
and spot::kripke.
* src/ta/tgta.hh: Do not use \emph.
* src/tgba/succiter.hh: Fix rendering of example.
* src/tgba/tgba.hh: Correct documentation.
* src/tgbaalgos/cycles.hh: Improve rendering of
documentation.
* src/tgbaalgos/lbtt.hh, src/tgbaalgos/minimize.hh:
Document missing arguments.
* src/bin/ltlcross.cc: Implement the new option. Average the product
statistics on all products.
* src/tgbatest/basimul.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlcross2.test, bench/ltl2tgba/tools: Use the new option.
* NEWS: Mention it.
* src/tgba/bdddict.cc, src/tgba/bdddict.hh
(unregister_all_typed_variables): New method.
* src/tgbaalgos/degen.cc (degeneralize): Use it.
* NEWS: Mention it.
* src/tgbaalgos/simulation.hh, src/tgbaalgos/simulation.cc
(simulation_sba, cosimulation_sba, iterated_simulations_sba): New
function. Also speedup the existing functions by avoiding
add_acceptince_conditions() and add_conditions(). Finally, use
scc_filter_states() when dealing with degeneralized automata.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh (do_ba_simul):
New method. Use it after degeneralization.
* src/tgba/tgbaexplicit.hh (get_transition, get_state): New methods.
* src/tgbatest/basimul.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
* NEWS: Introduce the new function and summarize the bug.
The main motivation is the upcoming patch that introduces
simulation_sba() and requires this function.
* src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: Implement it.
* src/tgbaalgos/postproc.cc: Use it for monitors, because we do not
care about acceptance conditions.
* NEWS: Mention it.
* src/bin/ltlfilt.cc: Handle --universal and --eventual. Match
only LTL formulas with --stutter-invariant.
* src/ltltest/ltlfilt.test: New file.
* src/ltltest/Makefile.am (TESTS): Add it.
* NEWS: Mention these bug fixes.
Provide a way to output automata with state-based acceptance. Also
print the guards using to_lbt_string() for consistency: as a
consequence, atomic proposition that do not match p[0-9]+ are now
double-quoted.
* src/tgbaalgos/lbtt.hh (lbtt_reachable): Add a sba option.
* src/tgbaalgos/lbtt.cc: Implement it, and use to_lbt_string().
* src/ltlvisit/lbt.cc (is_pnum): Reject 'p' without number.
* src/bin/ltl2tgba.cc: Activate the sba option of --ba was given.
Add an option --lbtt=t to get the old behavior.
* src/bin/man/ltl2tgba.x: Document the LBTT format we use with
some links and examples.
* src/tgbatest/lbttparse.test: More tests.
* src/tgbatest/ltlcross2.test: Add a check with --lbtt --ba.
* NEWS: Update.
* wrap/python/ajax/ltl2tgba.html: Augment and update tooltips to match
vocabulary in the Spin'13 paper. Hide the compose obligation option
since it's a work in progress.
* src/bin/ltlcross.cc: Implement the counters.
* doc/org/ltlcross.org: Update the documentation.
* bench/ltl2tgba/sum.py: Do not assume a fixed column for the time.
* NEWS: Update.
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Do not pass
automata since they are known from the scc. Avoid several dynamic
casts. Try to match the established vocabulary wrt "weak" and
"inherently weak". The old is_weak_scc() that used to enumerate cycles
is therefore renamed to is_inherently_weak_scc(), while the new
is_weak_scc() will should ensure all transitions are fully accepting.
* NEWS: Mention the new interface.
Provides 3 heurisitics to compute the strength of an SCC:
inherent, structural and syntactic
* src/tgbaalgos/isweakscc.cc: implementation
* src/tgbaalgos/isweakscc.hh: definition
The set of rules enabled by favor_even_univ try to "lift" the
subformulae that are both eventual and universal, so they appear
higher in the AST. This is contrary to what we used to do (and still
do when the option is unset), were we try to postpone such subformulae
(by moving them down the AST). It is still a bit experimental.
* src/ltlvisit/simplify.hh: Add option favor_event_univ.
* src/ltlvisit/simplify.cc: Implement new rewriting rules.
* doc/tl/tl.tex: Document them.
* src/tgbatest/ltl2tgba.cc: Add option -ra to enable them.
* src/tgbatest/spotlbtt.test: Test the translation with this option.
* src/ltltest/reduc.cc, src/ltltest/equals.cc: Add option
to enable the new rules.
* src/ltltest/eventuniv.test: New file to test them.
* src/ltltest/Makefile.am: Add it.
This has to be turned on using "-x comp-susp" and other
related options documented in spot-x (7).
* src/tgbaalgos/translate.hh, src/tgbaalgos/translate.cc:
Add support for calling composition-suspension, with
optional simulation, WDBA-minimization, and composition.
* src/bin/spot-x.cc: Document the new options.
* src/bin/man/spot-x.x: Add some bibliography.
* src/tgbatest/ltlcross2.test: Test it.
* src/tgbaalgos/sccfilter.cc: Reuse existing acceptance set as filler
in SCC sets that need less SCC sets than the other SCCs automaton.
* src/tgbatest/sccsimpl.test: Add more tests.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Do simulation
on the BA produced in --high mode.
* src/bin/spot-x.cc: Document the ba-simul option that can be used
to disable it.
