diff --git a/ChangeLog b/ChangeLog index f18b49fb7..730c5b377 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-12-07 Denis Poitrenaud + + * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc + (set_init_state): Return a pointer to the initial state. + + * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc + (tgba_run_to_tgba): New function. + * src/tgbatest/ltl2tgba.cc: Add option -G. + 2004-12-08 Alexandre Duret-Lutz * src/tgbaalgos/replayrun.cc (replay_tgba_run): More comments. diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index d75ca9750..4b2eb156c 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -152,11 +152,12 @@ namespace spot return i->second; } - void + tgba_explicit::state* tgba_explicit::set_init_state(const std::string& state) { tgba_explicit::state* s = add_state(state); init_ = s; + return s; } tgba_explicit::transition* diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 08492b99d..c65419c33 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -51,7 +51,7 @@ namespace spot const state* dest; }; - void set_init_state(const std::string& state); + state* set_init_state(const std::string& state); transition* create_transition(const std::string& source, const std::string& dest); diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 90a96291f..9293f3d54 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -19,9 +19,11 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include #include "emptiness.hh" #include "tgba/tgba.hh" #include "tgba/bddprint.hh" +#include "tgba/tgbaexplicit.hh" namespace spot { @@ -80,7 +82,6 @@ namespace spot return os; } - tgba_run& tgba_run::operator=(const tgba_run& run) { @@ -108,4 +109,118 @@ namespace spot { return os; } + + namespace + { + std::string format_state(const tgba* a, const state* s, int n) + { + std::ostringstream os; + os << a->format_state(s) << " (" << n << ")"; + return os.str(); + } + } + + tgba* tgba_run_to_tgba(const tgba* a, const tgba_run* run) + { + tgba_explicit* res = new tgba_explicit(a->get_dict()); + res->copy_acceptance_conditions_of(a); + + const state* s = a->get_init_state(); + int number = 1; + tgba_explicit::state* source; + tgba_explicit::state* dest; + const tgba_run::steps* l; + bdd seen_acc = bddfalse; + + typedef Sgi::hash_map state_map; + state_map seen; + + if (run->prefix.empty()) + l = &run->cycle; + else + l = &run->prefix; + + tgba_run::steps::const_iterator i = l->begin(); + + assert(s->compare(i->s) == 0); + source = res->set_init_state(format_state(a, i->s, number)); + ++number; + seen.insert(std::make_pair(i->s, source)); + + for (; i != l->end(); ) + { + // expected outgoing transition + bdd label = i->label; + bdd acc = i->acc; + + // compute the next expected state + const state* next; + ++i; + if (i != l->end()) + { + next = i->s; + } + else + { + if (l == &run->prefix) + { + l = &run->cycle; + i = l->begin(); + } + next = l->begin()->s; + } + + // browse the actual outgoing transitions + tgba_succ_iterator* j = a->succ_iter(s); + delete s; + for (j->first(); !j->done(); j->next()) + { + if (j->current_condition() != label + || j->current_acceptance_conditions() != acc) + continue; + + const state* s2 = j->current_state(); + if (s2->compare(next) != 0) + { + delete s2; + continue; + } + else + { + s = s2; + break; + } + } + assert(!j->done()); + delete j; + + state_map::const_iterator its = seen.find(next); + if (its == seen.end()) + { + dest = res->add_state(format_state(a, next, number)); + ++number; + seen.insert(std::make_pair(next, dest)); + } + else + dest = its->second; + + tgba_explicit::transition* t = res->create_transition(source, dest); + res->add_conditions(t, label); + res->add_acceptance_conditions(t, acc); + source = dest; + + // Sum acceptance conditions. + if (l == &run->cycle && i != l->begin()) + seen_acc |= acc; + } + delete s; + + assert(seen_acc == a->all_acceptance_conditions()); + + res->merge_transitions(); + + return res; + } + } diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 5d9bd1f59..972dcc54c 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -179,12 +179,23 @@ namespace spot /// annotation). /// /// (\a a is used here only to format states and transitions.) + /// + /// Output the prefix and cycle of the tgba_run \a run, even if it + /// does not corresponds to an actual run of the automaton \a a. + /// This is unlike replay_tgba_run(), which will ensure the run + /// actually exist in the automaton (and will display any transition + /// annotation). std::ostream& print_tgba_run(std::ostream& os, - const tgba* a, - const tgba_run* run); + const tgba* a, + const tgba_run* run); + + /// \brief Return an explicit_tgba corresponding to \a run (i.e. comparable + /// states are merged). + /// + /// \pre \a run must correspond to an actual run of the automaton \a a. + tgba* tgba_run_to_tgba(const tgba* a, const tgba_run* run); + /// @} - - } #endif // SPOT_TGBAALGOS_EMPTINESS_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 19936972e..c007ba91a 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -74,6 +74,8 @@ syntax(char* prog) << " -F read the formula from the file" << std::endl << " -g graph the accepting run on the automaton (requires -e)" << std::endl + << " -G graph the accepting run seen as an automaton " + << " (requires -e)" << std::endl << " -L fair-loop approximation (implies -f)" << std::endl << " -m try to reduce accepting runs, in a second pass" << std::endl @@ -170,6 +172,7 @@ main(int argc, char** argv) bool post_branching = false; bool fair_loop_approx = false; bool graph_run_opt = false; + bool graph_run_tgba_opt = false; bool opt_reduce = false; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; @@ -241,6 +244,10 @@ main(int argc, char** argv) { graph_run_opt = true; } + else if (!strcmp(argv[formula_index], "-G")) + { + graph_run_tgba_opt = true; + } else if (!strcmp(argv[formula_index], "-L")) { fair_loop_approx = true; @@ -443,9 +450,10 @@ main(int argc, char** argv) } } - if (graph_run_opt && (echeck_algo == "" || !expect_counter_example)) + if ((graph_run_opt || graph_run_tgba_opt) && + (echeck_algo == "" || !expect_counter_example)) { - std::cerr << argv[0] << ": error: -g requires -e." << std::endl; + std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl; exit(1); } @@ -690,7 +698,7 @@ main(int argc, char** argv) { ec = spot::explicit_tau03_search(a); } - + break; case Tau03OptSearch: ec = spot::explicit_tau03_opt_search(a); break; @@ -704,7 +712,7 @@ main(int argc, char** argv) do { spot::emptiness_check_result* res = ec->check(); - if (!graph_run_opt) + if (!graph_run_opt && !graph_run_tgba_opt) ec->print_stats(std::cout); if (expect_counter_example != !!res && (!bit_state_hashing || !expect_counter_example)) @@ -746,6 +754,12 @@ main(int argc, char** argv) spot::tgba_run_dotty_decorator deco(run); spot::dotty_reachable(std::cout, a, &deco); } + else if (graph_run_tgba_opt) + { + spot::tgba* ar = spot::tgba_run_to_tgba(a, run); + spot::dotty_reachable(std::cout, ar); + delete ar; + } else { spot::print_tgba_run(std::cout, a, run);