* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am: Add
$(VISIBILITY_CXXFLAGS).
* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/compsusp.hh,
src/tgbaalgos/cutscc.hh, src/tgbaalgos/cycles.hh,
src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/nsheap.hh,
src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.hh,
src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.hh,
src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.hh,
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.hh,
src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh,
src/tgbaalgos/safety.hh, src/tgbaalgos/save.hh, src/tgbaalgos/scc.hh,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/se05.hh,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.hh,
src/tgbaalgos/stripacc.hh, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.hh, src/tgbaalgos/translate.hh: Mark public
symbol with SPOT_API.

* src/tgba/Makefile.am: Use $(VISIBILITY_CXXFLAGS).
* src/tgba/bdddict.hh, src/tgba/bddprint.hh, src/tgba/formula2bdd.hh,
src/tgba/futurecondcol.hh, src/tgba/state.hh, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.hh, src/tgba/taatgba.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.hh,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh: Mark exported symbols with
SPOT_API.
* src/tgba/public.hh: Mark the file as deprecated.
* src/tgbaalgos/cutscc.hh: Adjust.

* src/misc/bddalloc.cc, src/misc/bddalloc.hh,
src/misc/freelist.cc, src/misc/freelist.hh: Move ...
* src/priv/bddalloc.cc, src/priv/bddalloc.hh,
src/priv/freelist.cc, src/priv/freelist.hh: ... here.
* src/misc/Makefile.am, src/priv/Makefile.am: Adjust.
* src/tgba/bdddict.cc: Adjust include.
* src/tgbaalgos/ltl2tgba_fm.cc: Remove useless include.

* README: Document it.
* configure.ac: Generate src/priv/Makefile.
* src/Makefile.am: Recurse into priv/.
* src/priv/Makefile.am: New file.
* src/misc/acccompl.cc, src/misc/acccompl.hh,
src/misc/accconv.cc, src/misc/accconv.hh: Move to...
* src/priv/acccompl.cc, src/priv/acccompl.hh,
src/priv/accconv.cc, src/priv/accconv.hh: ... here.
* src/misc/Makefile.am: Adjust.
* src/tgbaalgos/scc.cc, src/tgbaalgos/simulation.cc: Adjust
includes.
* src/sanity/style.test: Make sure no public header
file include a private one.

This follows from a discussion with Ernesto Posse.

The semantics for the {...} operator we use in Spot comes from the
cl(...) operator defined by Dax et al. (ATVA'09).  This is slightly
different from the the way the PSL spec interprets a SERE used in the
context of a temporal formula (appendix B.3.1.1.2, item 7).

cl({a;b}[*]) would match any infinite word that starts with a;b, while
in PSL {a;b}[*] would match any infinite word that alternates a and b.

Spot documents that {SERE} in a temporal formula is interpreted like
cl(SERE) however it failed to ignore the empty prefix of SERE.  So
{{a;b}[*]} would match anything, because the empty word is a prefix of
any word, and is also accepted by {a;b}[*].  Some trivial identities
and basic rewritings were also wrongly considering these empty
prefixes as well.

This patch therefore fixes the translation and syntactic
simplification rules, to really ignore these empty prefixes.

In some future version it should probably be wise to rename this {...}
operator as cl(...), and use {...} for the semantics given in appendix
B.3.1.1.2 (item 7) of the PSL specs.

* src/ltlast/unop.cc: Fix trivial identities.  We have
{[*0]} = 0 and !{[*0]} = 1.
* src/ltlvisit/simplify.cc: Fix basic rewriting rules.
{e[*]} = {e} and !{e[*]} = !{e}.
* doc/tl/tl.tex: Adjust documentation.
* doc/tl/tl.bib (dax.09.atva): New entry.
* src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
infinite word for {e[*]} just because the empty
prefix is matched by e[*].
* src/tgbatest/ltl2tgba.test: Add a test case.
* NEWS: Mention it.
* THANKS: Add Ernesto.

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/ltlast/formula.hh, src/ltlvisit/contain.hh,
src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh,
src/ltlvisit/remove_x.hh, src/ltlvisit/simplify.hh, src/ltlvisit/snf.hh,
src/misc/minato.hh, src/misc/optionmap.hh,
src/saba/sabacomplementtgba.hh, src/taalgos/emptinessta.hh,
src/taalgos/minimize.hh, src/taalgos/tgba2ta.hh,
src/tgba/tgbakvcomplement.hh, src/tgbaalgos/cycles.hh,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gv04.hh, src/tgbaalgos/ltl2taa.hh,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.hh,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/se05.hh,
src/tgbaalgos/simulation.hh, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.hh: Surround verbatim blocks with /** ... */
instead of using /// on each line.  Otherwise Doxygen will output the
leading "///" tokens -- apparently this is a feature.
* src/sanity/style.test: Strip multi-line comments before checking
code style.

Using \ingroup between \brief and the rest of the documentation causes
Doxygen to concatenate the brief with the rest of the doc.

* src/sanity/style.test: Warn when \ingroup is found
on the line after \brief.
* src/kripke/fairkripke.hh, src/kripke/kripke.hh,
src/kripke/kripkeprint.hh, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.hh, src/ltlast/binop.hh, src/ltlast/bunop.hh,
src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh,
src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh,
src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh,
src/ltlenv/environment.hh, src/ltlparse/ltlfile.hh,
src/ltlvisit/clone.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/mark.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.hh,
src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh,
src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.hh, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh,
src/misc/freelist.hh, src/misc/hash.hh, src/misc/ltstr.hh,
src/misc/minato.hh, src/misc/modgray.hh, src/misc/optionmap.hh,
src/misc/version.hh, src/saba/explicitstateconjunction.hh,
src/saba/saba.hh, src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
src/saba/sabasucciter.hh, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.hh, src/ta/ta.hh, src/ta/taproduct.hh,
src/ta/tgta.hh, src/taalgos/reachiter.hh, src/taalgos/tgba2ta.hh,
src/tgba/futurecondcol.hh, src/tgba/sba.hh, src/tgba/state.hh,
src/tgba/succiter.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh, src/tgbaalgos/bfssteps.hh,
src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh,
src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/rundotdec.hh, src/tgbaalgos/save.hh,
src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.hh: Move \ingroup
before \brief.

* src/tgbaalgos/simulation.cc: Pass template arguments to base-class
initializer to fix compilation with g++ < 4.5.  Reported by Sonali
Dutta.

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

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.

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

Etienne Renault authored Mar 06, 2013 and Alexandre Duret-Lutz committed Apr 27, 2013

Provides 3 heurisitics to compute the strength of an SCC:
inherent, structural and syntactic

* src/tgbaalgos/isweakscc.cc: implementation
* src/tgbaalgos/isweakscc.hh: definition

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.

* src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh: Add option
for suspended labels removal.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/spotlbtt.test: Test it.

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

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