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