2009-11-23 Alexandre Duret-Lutz * src/tgbaalgos/sccfilter.cc (create_transition): Do not clone the same node twice when dealing with loops. 2009-11-23 Alexandre Duret-Lutz Use bdd_satprefix() to speedup minato on BDDs that are almost cubes. * src/misc/minato.cc (minato_isop::minato_isop): Call bdd_satprefix. (minato_isop::next): Avoid useless intermediate variables. * src/misc/minato.hh: Typo in comments. 2009-11-23 Alexandre Duret-Lutz Specialize scc_filter when handling tgba_explicit_formula automata. If the input is a tgba_explicit_formula we can output a tgba_explicit_formula too, and we want to do that because it is more space efficient. * src/tgba/tgbaexplicit.hh (get_label): New method. * src/tgbaalgos/sccfilter.cc (create_transition): New function, to handle tgba_explicit_formula and tgba_explicit_string output differently. (filter_iter): Template it on the output tgba type, and adjust to call create_transition. (scc_filter): Use filter_iter or filter_iter depending on the input tgba type. 2009-11-20 Alexandre Duret-Lutz Strip useless acceptance conditions in scc_filter(). A useless acceptance conditions is one that is always implied by another. * src/misc/bddop.hh, src/misc/bddop.cc (compute_neg_acceptance_conditions): New function. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (set_acceptance_conditions): New function. * src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot): Keep track of useful acceptance conditions. (useful_acc_of): New function. * src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New attributes. * src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter useless acceptance conditions. (scc_filter): Compute useful acceptance conditions and pass them to filter_iter. 2009-11-20 Alexandre Duret-Lutz * src/tgbaalgos/sccfilter.cc (scc_filter): Merge transitions after removing acceptance conditions. 2009-11-18 Alexandre Duret-Lutz Remove prune_scc(), prune_acc(), and related fonctions. * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh (prune_scc, prune_acc, remove_component, compute_scc, remove_acc, is_not_accepting, delete_scc, is_terminal, remove_scc, display_scc): Remove anything related to the simplification of SCCs. 2009-11-18 Alexandre Duret-Lutz Replace prune_scc() by scc_filter(). prune_scc() leaked memory and failed to remove chains of useless SCCs. * src/tgbaalgos/reductgba_sim.cc (reduc_tgba_sim): Call scc_filter() instead of prune_scc(), and do it before running any simulation-based reduction. * src/tgbaalgos/reductgba_sim.hh (reduc_tgba_sim): Return a const tgba*. * src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Call scc_filter() instead of prune_scc(). * src/tgbatest/scc.test: Add two more tests that failed with prune_scc(). 2009-11-18 Alexandre Duret-Lutz Quick implementation of a "useless SCC" filter using scc_map. * src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: New files. * src/tgbaalgos/Makefile.am: Add them. 2009-11-18 Alexandre Duret-Lutz Fix acceptance check in scc_map: trivial SCCs are not accepting. Also compute useless SCCs. * src/tgbaalgos/scc.cc (scc_map::scc::trivial): New field. (scc_stats::useless_scc_map): New field. * src/tgbaalgos/scc.cc (scc_map::build_map): Mark SCCs that are not trivial. (scc_map::accepting): Always return false for trivial SCC. (build_scc_stats): Fill in useless_scc_map. 2009-11-18 Alexandre Duret-Lutz Make it easy to filter states while iterating over an automaton. * src/tgbaalgos/reachiter.hh (tgba_reachable_iterator::want_state): New method. * src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::want_state): Implement it. (tgba_reachable_iterator::run): Call want_state before processing a state. 2009-11-17 Alexandre Duret-Lutz * src/tgbaalgos/cutscc.cc (cut_scc): Pass `s' by reference instead of by pointer. * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Fix copyright header. 2009-11-13 Alexandre Duret-Lutz Replace the hash key construction of LTL formulae by a simple counter updated each time we create a new (unique) formula. Doing so saves a lot of memory during the translation of the ltlcounter formulae, because the formulae are quite big and storing a string representation of each formula on its node was a bad idea. For instance with n=12, the translation now uses 40MB where it used 290MB. (Note: in both cases, 20MB is being used by the BDD cache.) * src/ltlast/formula.hh (hash_key_): Rename as ... (count_): ... this. (hash): Adjust. (max_count): New static variable to count the number of formulae created. (formula): Update max_count and set count_. (dump): Make it a virtual pure method. (set_key_): Remove. (formula_ptr_less_than): Speed up and return false when the two formula pointer are equal. * src/ltlast/formula.cc (set_key_, dump): Remove. * 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/constant.cc, src/ltlast/constant.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh: Empty the constructor (do not precompute the dump_ anymore), and add a dump() implementation. 2009-11-12 Alexandre Duret-Lutz Use -l wherever we where expecting ltl2tgba to default to LaCIM. * bench/ltl2tgba/algorithms: Use -l for all LaCIM invocations. * src/tgbatest/dupexp.test, src/tgbatest/emptchk.test, src/tgbatest/spotlbtt.test: Likewise. 2009-11-12 Alexandre Duret-Lutz Cleanup the help of ltl2tgba. * src/tgbatest/ltl2tgba.cc (syntax): Reorganize the help text, so that we can find options without resorting to grep... Also cleanup the program name if it is a libtool wrapper. 2009-11-12 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (-l): New option to select the lacim translation. It still is the default translation. (opt_fm, opt_taa): Replace these two variables by ... (translation): ... this enum. And use a switch to call the correct translation. 2009-11-11 Alexandre Duret-Lutz Remove python bindings for ltl::clone and ltl::destroy. * wrap/python/spot.i: Do not include clone.hh and destroy.hh. 2009-11-10 Alexandre Duret-Lutz Typo from a previous patch. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Fix a typo introduced three patches ago in the handling of unobserved events. 2009-11-10 Alexandre Duret-Lutz Do not comment states in the never claim by default. It takes too much time when the formula is large, and it is useless when the purpose is model-checking with Spin. * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the comments option. * src/tgbaalgos/neverclaim.cc (never_claim_bfs, never_claim_reachable): Honor the comment option. * src/tgba/tests/ltl2tgba.cc (-N): Do not comment states. (-NN) New option to output a commented never claim. 2009-11-10 Damien Lefortier * src/tgba/taa.cc, src/tgba/taa.hh: Fix it. * src/tgbaalgos/ltl2taa.cc: Do NOT use the same bdd_dict for both the translation and the language containment checker. * src/tgbatest/spotlbtt.test: Update TAA related tests. 2009-11-10 Alexandre Duret-Lutz Use tgba_explicit_formula instead of tgba_explicit_string in FM. This gives a nice speedup (>1.4) in the ltlcounter benchmark, because we no longer have to generate a copy the string representations of the LTL formulae. * src/tgbaalgos/ltl2tgba_fm.cc: Adjust. Also get rid of the formulae_seen map, since we can now ask the tgba_explicit_formula if it knows the state. 2009-11-10 Alexandre Duret-Lutz Ease debugging of LTL formulae leaks. * src/tgbatest/ltl2tgba.cc: Dump all LTLinstances with their reference count. 2009-11-10 Alexandre Duret-Lutz Introduce tgba_explicit_labelled