diff --git a/ChangeLog b/ChangeLog index b5771072d..e34eb6625 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2004-02-08 Alexandre Duret-Lutz + + This should help getting accurate statistics (on both the + formula automaton and the synchronized product) from LBTT. + Idea from Jean-Michel Couvreur. + + * src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class. + (nonacceptant_lbtt_reachable): New function. + * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New + function. + * src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable + if the -T option is used. + * src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by + default. + 2004-02-05 Alexandre Duret-Lutz * src/tgbaalgos/lbtt.hh: Typos. diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index a51728e85..8be8d1a42 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,17 +19,18 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include "lbtt.hh" #include "misc/hash.hh" #include #include #include #include #include -#include "tgba/tgba.hh" #include "save.hh" #include "tgba/bddprint.hh" #include "ltlvisit/tostring.hh" #include "tgba/bddprint.hh" +#include "reachiter.hh" #include "misc/bddlt.hh" namespace spot @@ -277,4 +278,64 @@ namespace spot } return os; } + + + class nonacceptant_lbtt_bfs : public tgba_reachable_iterator_breadth_first + { + public: + nonacceptant_lbtt_bfs(const tgba* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), os_(os), acc_count_(0) + { + // Count the number of acceptance_conditions. + bdd all = a->all_acceptance_conditions(); + while (all != bddfalse) + { + bdd one = bdd_satone(all); + all -= one; + ++acc_count_; + } + } + + void + process_state(const state*, int n, tgba_succ_iterator*) + { + --n; + if (n == 0) + body_ << "0 1 -1" << std::endl; + else + body_ << "-1" << std::endl << n << " 0 -1" << std::endl; + } + + void + process_link(int, int out, const tgba_succ_iterator* si) + { + --out; + std::string s = + bdd_to_lbtt(si->current_condition(), automata_->get_dict()); + body_ << out << " " << s << std::endl; + } + + void + end() + { + os_ << seen.size() << " " << acc_count_ << std::endl + << body_.str() << "-1" << std::endl; + } + + private: + std::ostream& os_; + std::ostringstream body_; + unsigned acc_count_; + }; + + + std::ostream& + nonacceptant_lbtt_reachable(std::ostream& os, const tgba* g) + { + nonacceptant_lbtt_bfs b(g, os); + b.run(); + return os; + } + + } diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index ab80394f7..4c17006a9 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -50,6 +50,23 @@ namespace spot /// \param g The automata to print. /// \param os Where to print. std::ostream& lbtt_reachable(std::ostream& os, const tgba* g); + + /// \brief Print an LBTT automaton for statistics. + /// + /// Output \a g in LBTT's format but ignoring the acceptance + /// conditions, of all its transitions. This produces an automaton + /// that has the same size as \a g, and whose synchronized product + /// with another automaton also has the same size. This will also + /// declare as much acceptance conditions has there is in \a g (they + /// will just be never used). + /// + /// The produced automaton will not recognize any word (unless \a g + /// has no acceptance condition, in which case this function is a + /// no-op). + /// + /// The produced automaton is useful to obtain accurate statistics + /// from LBTT, without any size blow up of the automata. + std::ostream& nonacceptant_lbtt_reachable(std::ostream& os, const tgba* g); } #endif // SPOT_TGBAALGOS_LBTT_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 189f7f774..5f0621666 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -76,6 +76,8 @@ syntax(char* prog) << " -S convert to explicit automata, and number states " << "in BFS order" << std::endl << " -t display reachable states in LBTT's format" << std::endl + << " -T display reachable states in LBTT's format w/o " + << "acceptance conditions" << std::endl << " -v display the BDD variables used by the automaton" << std::endl << " -X do not compute an automaton, read it from a file" @@ -197,6 +199,10 @@ main(int argc, char** argv) { output = 6; } + else if (!strcmp(argv[formula_index], "-T")) + { + output = 7; + } else if (!strcmp(argv[formula_index], "-v")) { output = 5; @@ -318,6 +324,9 @@ main(int argc, char** argv) case 6: spot::lbtt_reachable(std::cout, a); break; + case 7: + spot::nonacceptant_lbtt_reachable(std::cout, a); + break; default: assert(!"unknown output option"); } diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 4a33c3516..0bb9b8bef 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -42,6 +42,13 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- LaCIM), fake" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -T'" + Enabled = no +} + Algorithm { Name = "Spot (Couvreur -- FM)" @@ -56,11 +63,21 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM), fake" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -T'" + Enabled = no +} + GlobalOptions { Rounds = 100 Interactive = Never # Verbosity = 5 +# ComparisonCheck = no +# ConsistencyCheck = no +# IntersectionCheck = no } FormulaOptions