* src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* wrap/python/spot.i: Wrap them.
* wrap/python/ajax/spot.in: Display count of nondeterministic
states.
* src/tgbatest/ltl2tgba.cc (-kt): Likewise.
* NEWS: Upadte.

* src/tgba/tgbaexplicit.hh (num_states): New method.
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
(minimize_obligation): Add a reject_bigger option.
* src/tgbatest/ltl2tgba.cc (-RM): New option.
* src/tgbatest/spotlbtt.test: Test -RM.
* bench/ltl2tgba/algorithms: Include -RM in addition to -Rm, and
replace -RDS by -RIS.
* NEWS: Mention this.

Thomas Badie authored Aug 18, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/tgbaalgos/simulation.cc: Create the iterated_simulations.
(direct_simulation) Add an attribute "stat" that represents the
number of states and transitions of the resulting automaton.
* src/tgbaalgos/simulation.hh: Declare the iterated_simulations.
* src/tgbatest/spotlbtt.test: Test the iterated_simulations.
* src/tgbatest/ltl2tgba.cc: Associate the option -RIS to the
iterated_simulations.

Thomas Badie authored Aug 06, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/tgbaalgos/simulation.cc: Add the cosimulation:
(acc_compl_automaton) Add a template parameter.
(acc_compl_automaton::process_link) Add a swap source destination.
(direct_simulation) Add a template parameter.
(direct_simulation::compute_sig) Add a flag in the signature to
know if the state is initial.
(direct_simulation::build_result) Remove the flag before reading
the signature.
Swap source and destination when building the new automaton.
* src/tgbaalgos/simulation.hh: Declare and document the
Cosimulation.
* src/tgbatest/ltl2tgba.cc: Associate the cosimulation with the -RRS
option.
* src/tgbatest/spotlbtt.test: Add a test on the cosimulation.

* src/tgbaalgos/simulation.cc: Remove unused typedef.

* src/tgbaalgos/sccfilter.cc: tgba_explicit_numbered replace
tgba_explicit_string for the general case.  This way we don't have to
prefix the result of format_state() in case to states have the same
description.  We just number the states instead.  For the specific
cases where the input automata are instance of tgba_explicit_string or
tgba_explicit_formula, we clone the label.

* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: New files, with
most of the logic extracted from src/tgba/tgbatba.cc (SBA version).
* src/tgbaalgos/Makefile.am: Distribute these.
* src/tgbatest/ltl2tgba.cc: Use the new degeneralization instead of
the on-the-fly version.

* src/ltlvisit/simplify.cc, src/tgba/tgbaproduct.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc: Here.

This helps reducing (p&XF!p)|(!p&XFp)|X(Fp&F!p) to (p&XF!p)|(!p&XFp).

* src/tgbaalgos/ltl2tgba_fm.cc: Adjust rewriting rules of X.
* src/tgbatest/ltl2tgba.test: Add a test case.

* src/tgbaalgos/minimize.cc (minimize_obligation): Delete the powerset
automaton when we return 0 because we know if the result is correct
and don't have the formulae to check it.  Reported by Étienne Renault.

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.

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

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

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

* src/misc/acccompl.hh, src/misc/acccompl.cc (AccCompl): Rename to
acc_compl.
* src/tgbaalgos/simulation.cc (AccComplAutomaton, Simulation): Rename
to acc_compl_automaton and direct_simulation.  At the same time,
reindent the whole file.
* src/sanity/style.test: Detect capitalized class names.
* src/kripke/kripkeexplicit.hh (KripkePrint): Remove useless
predeclaration.
* src/tgbaalgos/simulation.hh: Typo in comment.

The distinction makes no sense since Spot 0.5, where we switched from
mutable furmulae to immutable formulae.  The difference between
const_visitor and visitor made no sense either.  They have been merged
into one: visitor.

* iface/dve2/dve2check.cc, iface/gspn/ltlgspn.cc,
src/eltlparse/eltlparse.yy, src/eltlparse/public.hh,
src/evtgbatest/ltl2evtgba.cc, src/kripkeparse/kripkeparse.yy,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/visitor.hh, src/ltlenv/declenv.cc, src/ltlenv/declenv.hh,
src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
src/ltlenv/environment.hh, src/ltlparse/ltlfile.cc,
src/ltlparse/ltlfile.hh, src/ltlparse/ltlparse.yy,
src/ltlparse/public.hh, src/ltltest/consterm.cc,
src/ltltest/equals.cc, src/ltltest/genltl.cc, src/ltltest/kind.cc,
src/ltltest/length.cc, src/ltltest/randltl.cc, src/ltltest/readltl.cc,
src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
src/ltltest/tostring.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/ltlvisit/dotty.cc,
src/ltlvisit/length.cc, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/lunabbrev.hh, src/ltlvisit/mark.cc, src/ltlvisit/mark.hh,
src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/reduce.cc, src/ltlvisit/reduce.hh,
src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/ltlvisit/snf.cc, src/ltlvisit/snf.hh, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh,
src/neverparse/neverclaimparse.yy, src/sabatest/sabacomplementtgba.cc,
src/tgba/bdddict.cc, src/tgba/formula2bdd.cc, src/tgba/taatgba.cc,
src/tgba/taatgba.hh, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/minimize.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/randtgba.cc: Massive adjustment!
* src/tgbatest/reductgba.cc: Delete.

* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Change the return
type.

* src/tgba/tgbaexplicit.hh: Rerganize a bit to
allow different functions to be used to format
states.  Add an enabled_utf8() method to
tgba_explicit_formula.
* src/tgbaalgos/dotty.hh, src/tgbaalgos/dotty.cc:
Simplify the interface by not depending on
dotty_decorator explicitely.
* src/tgba/bddprint.hh (enable_utf8): New function.
* src/tgba/bddprint.cc (enable_utf8): Implement it
and use the global utf8 flag in other functions.
* src/tgbatest/ltl2tgba.cc: Add an -8 option for
UTF-8 outpout.
* wrap/python/spot.i: Adjust for tgbexplicit.hh
changes.

* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc:
Return a tgba*, not a const tgba*.

It was a mistake to try to overload And/Or LTL operator for these when
trivial simplification are performed.  The reason is so simple it is
embarassing: And(f,1)=f is a trivial identity that should not be
applied with AndRat.  E.g. AndRat(a;b, 1) is equal to 0, not a;b.

* src/ltlast/multop.hh, src/ltlast/multop.cc: Add the AndRat and OrRat
operators.
* src/ltlparse/ltlparse.yy: Build them.
* src/ltlvisit/mark.cc, src/ltlvisit/simplify.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Adjust all switches.

* src/tgbaalgos/ltl2tgba_fm.cc: Here.
The check is done by next patch.

* src/ltlast/bunop.hh, src/ltlast/bunop.cc, src/ltlvisit/randomltl.cc,
src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
src/tgbaalgos/ltl2tgba_fm.cc: Remove all traces of these two
operators since they are not handled like sugar.
* doc/tl/tl.tex: Adjust documentation to reflect the fact that these
two operators are sugar.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_ratexp): Replace
a dynamic cast by a call to kind().

* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc (mark_concat_ops,
simplify_mark): Rewrite these two functions as methods of
(mark_tools): this new class.
* src/ltlast/binop.cc, src/ltlast/unop.cc: Adjust computation
of not_marked to ignore marked operators that are not at
the top-level.  I.e., something like X(!{a}) is not marked.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::mt): New
instance of mark_tools.
(formula_canonizer::translate) Adjust calls to
mark_concat_ops() and simplify_mark().

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not
translate a subformula if we have already proved it useless in
a previous rational expression.
* src/tgbatest/ltl2tgba.test: Add an example, although that
test does not ensure the subformula is ignored early in the
translation.  I.e., it would still work without the patch.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate,
ltl_to_tgba_fm): Do not convert labels as Boolean formulas before
creating transitions.  Use the bdd directly, and register the used
transitions later.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd):
Use boolean_to_bdd()

We used to cache it only for formulas used as states.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd): New method.
(ltl_trad_visitor::recurse): Use ltl_to_bdd().
(formula_canonizer): Likewise.
(ltl_to_tgba_fm): Adjust.