* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Add an options
parameter.
* src/bin/randaut.cc, src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
src/bin/ltl2tgba.cc, wrap/python/ajax/spot.in: Use it.
* src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/monitor.test,
src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test,
src/graphtest/tgbagraph.test: Adjust
because automata are now output horizontally.
* NEWS: Mention the change.
This is a huge patch, that took over a month to complete. The bit sets
are currently restricted to what 'unsigned can store', but it should be
easy to extend it to 'uint64_t' should we need it.
* NEWS: Update.
* src/tgba/acc.hh: New file.
* src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
* src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: Delete. The KV
complementation is too slow to be used in practice, and I somehow broke
it during the conversion to bitsets. The tgba->sgba conversion was only
used for the KV complementation, and should be better redone on
tgba_digraph_ptr should it be needed again.
* src/bin/ltlcross.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/nsa2tgba.cc, src/graphtest/tgbagraph.cc,
src/graphtest/tgbagraph.test, src/kripke/fairkripke.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.cc, src/kripke/kripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/misc/hash.hh, src/neverparse/neverclaimparse.yy, src/priv/accmap.hh,
src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgta.cc,
src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
src/taalgos/tgba2ta.cc, src/tgba/Makefile.am, src/tgba/fwd.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh,
src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/complete.cc,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/hoaf.cc,
src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/postproc.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reducerun.cc, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc,
src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
src/tgbaalgos/stripacc.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc,
src/tgbaalgos/weight.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/Makefile.am, src/tgbatest/complementation.cc,
src/tgbatest/complementation.test, src/tgbatest/degenlskip.test,
src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/emptchk.cc,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test,
src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test,
src/tgbatest/neverclaimread.test, src/tgbatest/randtgba.cc,
src/tgbatest/readsave.test, src/tgbatest/sim.test,
src/tgbatest/sim2.test, src/tgbatest/spotlbtt.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
iface/dve2/dve2.cc: Adjust or use to the new acceptance interface.
* src/tgba/tgbagraph.hh: Remove the set_bprop/get_bprop interface.
* src/tgba/tgba.cc, src/tgba/tgba.hh: Add a new interface for
setting/querying/copying the following properties: single_acc_set,
state_based_acc, inherently_weak, deterministic.
* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/neverparse/neverclaimparse.yy, src/saba/sabacomplementtgba.cc,
src/tgba/tgbagraph.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/isdet.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/postproc.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc, src/tgbatest/degenlskip.test,
src/tgbatest/ltl2tgba.cc: Adjust to the new interface, or use
it to bypass some useless work.
* src/tgba/tgbagraph.hh: Automatize the setting of the SingleAccSet
property.
* src/tgbaalgos/minimize.cc: Do not bother setting SingleAccSet.
* src/tgba/sba.hh: Delete.
* src/tgba/Makefile.am, wrap/python/spot.i: Adjust.
* src/taalgos/tgba2ta.cc: Do not include sba.hh.
* src/neverparse/neverclaimparse.yy: Set the SBA property on the output.
* src/tgbaalgos/lbtt.cc (lbtt_read_gba): Set the StateBasedAcc property
on output.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Do not rely on
the sba interface.
* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/tgbaalgos/simulation.cc, src/tgbaalgos/sccfilter.cc: Set
tgba_digraph::StateBasedAcc as appropriate.
* src/tgbatest/ltl2tgba.cc: Add extra assert.
This is a huge patch. tgba_digraph are equiped with some boolean
properties that can be used to indicate whether they represent SBA
(and will carry more informations later). All algorithms that produce
or use sba_explicit_* automata are changed to use tgba_digraph.
postproc has been rewritten using only tgba_digraph, and this required
changing the return types of many algorithms from tgba* to
tgba_digraph*.
* src/bin/dstar2tgba.cc, src/bin/ltlfilt.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/dstar2tgba.cc, src/dstarparse/nra2nba.cc,
src/dstarparse/nsa2tgba.cc, src/dstarparse/public.hh,
src/tgba/tgbagraph.hh, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/minimize.cc,
src/tgbaalgos/minimize.hh, src/tgbaalgos/postproc.cc,
src/tgbaalgos/postproc.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/stripacc.cc,
src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.cc,
src/tgbaalgos/translate.hh, src/tgbatest/ltl2tgba.cc,
wrap/python/spot.i: Update.
* src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh
(minimize_dfa, minimize_wdba): Return a sba_explicit_number automaton
instead of tgba_explicit_number.
* src/tgba/tgbaexplicit.hh (declare_acceptance_condition): Fix code
so it works on sba as well.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Specialize
for sba instead of tgba_sba_proxy.
* src/tgbaalgos/neverclaim.hh: Point to degeneralize().
* 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/neverclaim.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/save.cc: Prefer '\n' over std::endl to speedup I/O.
* src/ltltest/genltl.cc (syntax): Use '\n' too, although it won't
make a big difference.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a new
assume_sba argument.
* src/tgbaalgos/dotty.cc (dotty_bfs): Take a new
mark_accepting_states arguments.
(dotty_bfs::process_state): Check if a state is accepting using
the state_is_accepting() method for tgba_sba_proxies, or by
looking at the first outgoing transition of the state. Pass
the result to the dectorator.
(dotty_reachable): Adjust function.
* src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc,
src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc
(state_decl): Add an "accepting" argument, and use it to
decorate accepting states with a double border.
* src/tgbatest/ltl2tgba.cc: Keep track of whether the output
is an SBA or not, so that we can tell it to dotty().
* wrap/python/ajax/spot.in: Likewise.
* wrap/python/cgi-bin/ltl2tgba.in: Likewise.
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
as third parameter.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
dotty_bfs::process_link): Use the decorator.
* src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
is given.
* src/tgbatest/emptchk.test: Exercize -g.
(tgba_reachable_iterator::process_link): Take the state* as arguments
in addition to the state numbers.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(tgba_explicit::copy_acceptance_conditions_of): New method.
* tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
copy_acceptance_conditions_of.
(dupexp_iter::process_state, duplex_iter::declare_state,
dupexp_iter::name_): Remove.
(dupexp_iter::process_link): Adjust prototype, and format
the state here rather than in process_state.
* tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
of process_link.
just strip the last one. Escaping must be done at output.
* iface/gspn/gspm.cc (format_state): Likewise.
* src/misc/escape.hh, src/misc/escape.cc: New files.
* src/misc/Makefile.am: Add them.
* src/tgba/bddprint.cc (bdd_format_accset): New function.
* src/tgba/bddprint.hh (bdd_format_accset): New function.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state):
Escape the state name using escape_str().
(dotty_bfs::process_link): Escape conditions and acceptance
conditions using escape_str().
* src/tgbaalgos/save.cc (save_bfs::start): Call print_acc().
(save_bfs::print_acc): New function extracted from save_bfs::start().
Escape each acceptance condition.
(save_bfs::process_state): Use escape_str() and print_acc()
arcs. ltl2tgba_fm benefits from this and join multiple arcs with
the same destination and acceptance conditions.
* src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files.
* src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula,
bdd_format_formula): New functions.
* src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition,
tgba_explicit::add_condition, tgba_explicit::add_neg_condition,
tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition,
tgba_explicit::get_accepting_condition,
tgba_explicit::add_accepting_condition): Take a const formula*.
* src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition):
Rewrite using formula_to_bdd.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use
bdd_print_formula to display conditions.
* src/tgbaalgos/save.cc (save_bfs::process_state): Likewise.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula):
New function.
(translate_dict::conj_bdd_to_atomic_props): Remove.
(ltl_to_tgba_fm): Factor successors on accepting conditions
and destinations, not conditions. Use bdd_to_formula to translate
the conditions.
* src/tgbaparse/tgbaparse.yy: Expect conditions as a formula
in a string, call the LTL parser for this.
* src/tgbaparse/tgbascan.ll: Process " and \ escapes in
strings.
* src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explprod.test, src/tgbatest/mixprod.test,
src/tgbatest/readsave.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust to new syntax for explicit
automata.
the size of dot's output to 1024x1024.
* src/tgbaalgos/dotty.cc (dotty_bfs::start): Do not preset
the size of the graph. Set height=0 for the invisible state.
of these accepting set so that they are really usable. Provide
a all_accepting_conditions() method for use in the emptyness
check, and a neg_accepting_conditions() for products.
Predeclare TGBA accepting conditions is the i/o.
* src/tgba/bddprint.cc (want_prom): Rename as ...
(want_prom): ... this.
(print_handler): Adjust to display Acc[].
(print_acc_handler, bdd_print_acc): New functions.
* src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
New functions.
* src/tgba/succiter.hh (current_promise): Rename as ...
(current_accepting_conditions): ... this.
* src/tgba/succiterconcrete.cc (current_state):
Rename next to now.
(current_promise): Rename as ...
(current_accepting_conditions): ... this, and compute
the accepting conditions.
* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
src/tgba/succiterconcrete.hh,
src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.cc,
src/tgbaalgos/dotty.cc: Adjust to new names.
* src/tgba/tgba.hh (all_accepting_conditions,
neg_accepting_conditions): New functions.
* src/tgba/tgbabddconcretefactory.cc: Adjust to new
names, and record accepting conditions instead of promises.
* src/tgba/tgbabddcoredata.hh (accepting_conditions,
all_accepting_conditions, negacc_set): New variables.
(notnow_set, notprom_set, declare_promise): Rename as ...
(notnext_set, notacc_set, declare_accepting_condition): ... these.
* src/tgba/tgbaexplicit.hh
(tgba_explicit_succ_iterator::current_promise): Rename as ...
(tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
(tgba_explicit::add_promise): Rename as ...
(tgba_explicit::add_accepting_condition): ... this.
(tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition): New variables.
(tgba_explicit::get_promise): Rename as ...
(tgba_explicit::get_accepting_condition): ... this.
(tgba_explicit::all_accepting_conditions,
tgba_explicit::neg_accepting_conditions): Implement them.
(all_accepting_conditions, neg_accepting_conditions,
all_accepting_conditions): New variables.
(tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
* src/tgba/tgbaexplicit.cc: Likewise.
* src/tgba/tgbaproduct.hh
(tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
(tgba_product::all_accepting_conditions,
tgba_product::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.hh:
(tgba_translate_proxy::all_accepting_conditions,
tgba_translate_proxy::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.cc: Likewise.
* src/tgbaalgos/save.cc (save_rec): Call bdd_print
(tgba_save_reachable): Output the `acc =' line.
* src/tgbaparse/tgbaparse.yy: Support the for
accepting conditions definitions using an "acc =" line
at the start. Later, use has_accepting_condition while
parsing accepting conditions to ensure they were declared.
Disallow !cond in accepting conditions.
* src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
* src/tgbatest/explicit.cc (main): Declare accepting conditions.
* src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
and -R new options.
* src/tgbatest/tgbaread.cc (main): Really exit on parse error.
* src/tgbatest/explicit.test, src/tgbatest/explprod.test,
src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
recent changes.
* tgba/state.hh (state::translate, state::clone, state::as_bdd):
New virtual methods.
* tgba/stataebdd.cc (state::translate, state::clone): New methods.
* tgba/stataebdd.hh (state::translate, state::clone): New methods.
* tgba/tgbabddprod.cc (state_bdd_product::clone,
tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
New methods.
(tgba_bdd_product_succ_iterator::first): Reset right_
if any of left_ or right_ is already done (i.e., is empty).
(tgba_bdd_product_succ_iterator::done): Return true
if right_ is NULL.
(tgba_bdd_product_succ_iterator::current_state,
tgba_bdd_product::get_init_state): Work directory with `state's.
* tgba/tgbabddprod.hh (state_bdd_product::clone,
tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
New methods.
* tgba/tgbabddtranslateproxy.cc
(tgba_bdd_translate_proxy_succ_iterator::
tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator.
(tgba_bdd_translate_proxy_succ_iterator::
~tgba_bdd_translate_proxy_succ_iterator): New method.
(tgba_bdd_translate_proxy_succ_iterator::current_state,
tgba_bdd_translate_proxy::get_init_state,
tgba_bdd_translate_proxy::succ_iter): Work on `state's and
`tgba_succ_iterator's directlry.
(tgba_bdd_translate_proxy::format_state): Delegate formating
to the proxied automata.
* tgba/tgbaexplicit.cc (state_explicit::clone): New method.
* src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
tgba_explicit::get_promise): Call ltl::destroy on existing formulae.
* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(explprod_SOURCES): New variable.
(TESTS): Add explprod.test.
(CLEANFILES): Add input1 and input2.
* src/tgba/bddprint.cc (bdd_format_set): Likewise.
* src/tgba/state.hh: Add Doxygen comments.
(state::compare): Take a state*, not a state&.
(state_ptr_less_than): New functor.
* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
state&.
* src/tgba/statebdd.cc (state_bdd::compare): Likewise.
* src/tgba/succiter.hh: Add Doxygen comments.
* src/tgba/tgba.hh: Mention promises.
(tgba::formate_state): New pure virtual method.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state):
New method.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state):
Likewise.
* src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than
and tgba::formate_state.
Return a state*, not a state_bdd.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::current_state): Return a state_bdd*,
not a state_bdd.
* src/tgba/state.hh (state::as_bdd): New abstract method.
* src/tgba/statebdd.hh (state_bdd::as_bdd): Move definitions ...
* src/tgba/statebdd.cc (state_bdd::as_bdd): ... here.
* src/tgba/tgba.hh: Add Doxygen comments.
(tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state):
Return a state_bdd*, not a state_bdd.
(tgba_bdd_concrete::get_init_bdd): New method.
(tgba_bdd_concrete::succ_uter): Take a state* as argument.
* src/tgba/tgbabddconcrete.cc: Likewise.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
tgba_bdd_concrete::get_init_bdd.
* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust
to use state* instead of state_bdd.
* src/tgba/succlist.hh: Delete. (Leftover from a previous
draft.)
