diff --git a/ChangeLog b/ChangeLog index 0517916c2..b332d59d1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2004-11-10 Alexandre Duret-Lutz + * src/tgbaalgos/replayrun.hh, + src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug' + option to decide whether the output should look like that of + print_tgba_run() or a complete debug trace. + * src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with + debug=true. + * iface/gspn/ltlgspn.cc (main): Adjust to recent changes to src/tgbaalgos/magic.cc, call explicit_magic_search() instead of building a spot::magic_search. diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index 3a1ba09e9..975af5c8b 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/src/tgbaalgos/replayrun.cc @@ -41,7 +41,8 @@ namespace spot } bool - replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run) + replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run, + bool debug) { const state* s = a->get_init_state(); int serial = 1; @@ -58,47 +59,58 @@ namespace spot { l = &run->cycle; in = "cycle"; + if (!debug) + os << "No prefix.\nCycle:" << std::endl; } else { l = &run->prefix; in = "prefix"; + if (!debug) + os << "Prefix:" << std::endl; } tgba_run::steps::const_iterator i = l->begin(); if (s->compare(i->s)) { - os << "ERROR: First state of run (in " << in << "): " - << a->format_state(i->s) << std::endl - << "does not match initial state of automata: " - << a->format_state(s) << std::endl; + if (debug) + os << "ERROR: First state of run (in " << in << "): " + << a->format_state(i->s) << std::endl + << "does not match initial state of automata: " + << a->format_state(s) << std::endl; delete s; return false; } for (; i != l->end(); ++serial) { - // Keep track of the serial associated to each state so we - // can note duplicate states and make the replay easier to read. - state_map::iterator o = seen.find(s); - std::ostringstream msg; - if (o != seen.end()) + if (debug) { - std::set::const_iterator d; - for (d = o->second.begin(); d != o->second.end(); ++d) - msg << " == " << *d; - o->second.insert(serial); - delete s; - s = o->first; + // Keep track of the serial associated to each state so we + // can note duplicate states and make the replay easier to read. + state_map::iterator o = seen.find(s); + std::ostringstream msg; + if (o != seen.end()) + { + std::set::const_iterator d; + for (d = o->second.begin(); d != o->second.end(); ++d) + msg << " == " << *d; + o->second.insert(serial); + delete s; + s = o->first; + } + else + { + seen[s].insert(serial); + } + os << "state " << serial << " in " << in << msg.str() << ": "; } else { - seen[s].insert(serial); + os << " "; } - - os << "state " << serial << " in " << in << msg.str() << ": " - << a->format_state(s) << std::endl; + os << a->format_state(s) << std::endl; // expected outgoing transition bdd label = i->label; @@ -118,6 +130,8 @@ namespace spot l = &run->cycle; in = "cycle"; i = l->begin(); + if (!debug) + std::cout << "Cycle:" << std::endl; } next = l->begin()->s; } @@ -144,37 +158,53 @@ namespace spot } if (j->done()) { - os << "ERROR: no transition with label=" - << bdd_format_formula(a->get_dict(), label) - << " and acc=" << bdd_format_accset(a->get_dict(), acc) - << " leaving state " << serial - << " for state " << a->format_state(next) - << std::endl - << "The following transitions leave state " << serial - << ":" << std::endl; - for (j->first(); !j->done(); j->next()) + if (debug) { - const state* s2 = j->current_state(); - os << " *"; - print_annotation(os, a, j); - os << " label=" << bdd_format_formula(a->get_dict(), - j->current_condition()) - << " and acc=" - << bdd_format_accset(a->get_dict(), - j->current_acceptance_conditions()) - << " going to " << a->format_state(s2) << std::endl; - delete s2; + os << "ERROR: no transition with label=" + << bdd_format_formula(a->get_dict(), label) + << " and acc=" << bdd_format_accset(a->get_dict(), acc) + << " leaving state " << serial + << " for state " << a->format_state(next) + << std::endl + << "The following transitions leave state " << serial + << ":" << std::endl; + for (j->first(); !j->done(); j->next()) + { + const state* s2 = j->current_state(); + os << " *"; + print_annotation(os, a, j); + os << " label=" + << bdd_format_formula(a->get_dict(), + j->current_condition()) + << " and acc=" + << bdd_format_accset(a->get_dict(), + j->current_acceptance_conditions()) + << " going to " << a->format_state(s2) << std::endl; + delete s2; + } } delete j; delete s; return false; } - os << "transition"; - print_annotation(os, a, j); - os << " with label=" - << bdd_format_formula(a->get_dict(), label) - << " and acc=" << bdd_format_accset(a->get_dict(), acc) - << std::endl; + if (debug) + { + os << "transition"; + print_annotation(os, a, j); + os << " with label=" + << bdd_format_formula(a->get_dict(), label) + << " and acc=" << bdd_format_accset(a->get_dict(), acc) + << std::endl; + } + else + { + os << " | "; + print_annotation(os, a, j); + bdd_print_formula(os, a->get_dict(), label); + os << "\t"; + bdd_print_accset(os, a->get_dict(), acc); + os << std::endl; + } delete j; // Sum acceptance conditions. @@ -184,22 +214,24 @@ namespace spot if (!all_acc_seen && all_acc == expected_all_acc) { all_acc_seen = true; - os << "all acceptance conditions (" - << bdd_format_accset(a->get_dict(), all_acc) - << ") have been seen" - << std::endl; + if (debug) + os << "all acceptance conditions (" + << bdd_format_accset(a->get_dict(), all_acc) + << ") have been seen" + << std::endl; } } } delete s; if (all_acc != expected_all_acc) { - os << "ERROR: The cycle's acceptance conditions (" - << bdd_format_accset(a->get_dict(), all_acc) << ") do not" - << std::endl - << "match those of the automata (" - << bdd_format_accset(a->get_dict(), expected_all_acc) - << std::endl; + if (debug) + os << "ERROR: The cycle's acceptance conditions (" + << bdd_format_accset(a->get_dict(), all_acc) << ") do not" + << std::endl + << "match those of the automata (" + << bdd_format_accset(a->get_dict(), expected_all_acc) + << std::endl; return false; } diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh index 62e3cdaec..f8c375055 100644 --- a/src/tgbaalgos/replayrun.hh +++ b/src/tgbaalgos/replayrun.hh @@ -31,11 +31,20 @@ namespace spot /// \brief Replay a tgba_run on a tgba. /// + /// This is similar to print_tgba_run(), except that the run is + /// actually replayed on the automaton while it is printed. Doing + /// so makes it possible to display transition annotations (returned + /// by spot::tgba::transition_annotation()). The output will stop + /// if the run cannot be completed. + /// /// \param run the run to replay /// \param a the automata on which to replay that run /// \param os the stream on which the replay should be traced + /// \param debug if set the output will be more verbose and extra + /// debugging informations will be output on failure /// \return true iff the run could be completed - bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run); + bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run, + bool debug = false); } #endif // SPOT_TGBAALGOS_REPLAYRUN_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 1563a2b86..fa53d25c9 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -619,7 +619,8 @@ main(int argc, char** argv) else { spot::print_tgba_run(std::cout, ec_a, run); - if (!spot::replay_tgba_run(std::cout, ec_a, run)) + if (!spot::replay_tgba_run(std::cout, ec_a, run, + true)) exit_code = 1; } delete run;