diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index 8b68618bd..d8c8aa647 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -179,7 +179,7 @@ public: { auto run = res->accepting_run(); assert(run); - run = reduce_run(aut, run); + run = reduce_run(run); spot::tgba_word w(run); w.simplify(); std::ostringstream out; diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index db48a3f0b..8c557cd3b 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -703,7 +703,7 @@ namespace auto run = res->accepting_run(); if (run) { - run = reduce_run(prod, run); + run = reduce_run(run); std::cerr << "; both automata accept the infinite word\n" << " "; spot::tgba_word w(run); diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc index 6a62eca42..0e86faf54 100644 --- a/src/tests/complementation.cc +++ b/src/tests/complementation.cc @@ -248,7 +248,7 @@ int main(int argc, char* argv[]) if (auto run = res->accepting_run()) { spot::print_dot(std::cout, ec->automaton()); - spot::print_twa_run(std::cout, ec->automaton(), run); + std::cout << run; } } else diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index a1eceec86..3e1a9b746 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -1580,14 +1580,13 @@ checked_main(int argc, char** argv) if (opt_reduce) { tm.start("reducing accepting run"); - run = spot::reduce_run(res->automaton(), run); + run = spot::reduce_run(run); tm.stop("reducing accepting run"); } if (accepting_run_replay) { tm.start("replaying acc. run"); - if (!spot::replay_twa_run(std::cout, a, - run, true)) + if (!spot::replay_twa_run(std::cout, run, true)) exit_code = 1; tm.stop("replaying acc. run"); } @@ -1601,7 +1600,7 @@ checked_main(int argc, char** argv) } else { - spot::print_twa_run(std::cout, a, run); + std::cout << run; } tm.stop("printing accepting run"); } diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index f4e8196ae..4988b1122 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -1026,9 +1026,7 @@ main(int argc, char** argv) { tm_ar.stop(algo); std::ostringstream s; - if (!spot::replay_twa_run(s, - res->automaton(), - run)) + if (!spot::replay_twa_run(s, run)) { if (!opt_paper) std::cout << ", but could not replay " @@ -1049,12 +1047,8 @@ main(int argc, char** argv) if (opt_reduce) { - auto redrun = - spot::reduce_run(res->automaton(), run); - if (!spot::replay_twa_run(s, - res - ->automaton(), - redrun)) + auto redrun = spot::reduce_run(run); + if (!spot::replay_twa_run(s, redrun)) { if (!opt_paper) std::cout diff --git a/src/twaalgos/emptiness.cc b/src/twaalgos/emptiness.cc index cd943d2d4..c3329653c 100644 --- a/src/twaalgos/emptiness.cc +++ b/src/twaalgos/emptiness.cc @@ -47,16 +47,15 @@ namespace spot twa_run::twa_run(const twa_run& run) { - for (steps::const_iterator i = run.prefix.begin(); - i != run.prefix.end(); ++i) + aut = run.aut; + for (step s : run.prefix) { - step s = { i->s->clone(), i->label, i->acc }; + s.s = s.s->clone(); prefix.push_back(s); } - for (steps::const_iterator i = run.cycle.begin(); - i != run.cycle.end(); ++i) + for (step s : run.cycle) { - step s = { i->s->clone(), i->label, i->acc }; + s.s = s.s->clone(); cycle.push_back(s); } } @@ -72,37 +71,27 @@ namespace spot return *this; } - // print_twa_run - ////////////////////////////////////////////////////////////////////// - std::ostream& - print_twa_run(std::ostream& os, - const const_twa_ptr& a, - const const_twa_run_ptr& run) + operator<<(std::ostream& os, const twa_run_ptr& run) { + auto& a = run->aut; bdd_dict_ptr d = a->get_dict(); + + auto pstep = [&](const twa_run::step& st) + { + os << " " << a->format_state(st.s) << "\n | "; + bdd_print_formula(os, d, st.label); + if (st.acc) + os << '\t' << st.acc; + os << '\n'; + }; + os << "Prefix:" << std::endl; - for (twa_run::steps::const_iterator i = run->prefix.begin(); - i != run->prefix.end(); ++i) - { - os << " " << a->format_state(i->s) << std::endl; - os << " | "; - bdd_print_formula(os, d, i->label); - os << '\t'; - os << a->acc().format(i->acc); - os << std::endl; - } + for (auto& s: run->prefix) + pstep(s); os << "Cycle:" << std::endl; - for (twa_run::steps::const_iterator i = run->cycle.begin(); - i != run->cycle.end(); ++i) - { - os << " " << a->format_state(i->s) << std::endl; - os << " | "; - bdd_print_formula(os, d, i->label); - os << '\t'; - os << a->acc().format(i->acc); - os << '\n'; - } + for (auto& s: run->cycle) + pstep(s); return os; } diff --git a/src/twaalgos/emptiness.hh b/src/twaalgos/emptiness.hh index 09b371933..d79a65d1c 100644 --- a/src/twaalgos/emptiness.hh +++ b/src/twaalgos/emptiness.hh @@ -257,13 +257,12 @@ namespace spot /// \addtogroup emptiness_check_algorithms Emptiness-check algorithms /// \ingroup emptiness_check - - /// \addtogroup twa_run TGBA runs and supporting functions + /// \addtogroup twa_run TωA runs and supporting functions /// \ingroup emptiness_check /// @{ - /// An accepted run, for a tgba. - struct SPOT_API twa_run + /// An accepted run, for a twa. + struct SPOT_API twa_run final { struct step { const state* s; @@ -283,33 +282,34 @@ namespace spot steps prefix; steps cycle; + const_twa_ptr aut; ~twa_run(); - twa_run() + twa_run(const const_twa_ptr& aut) + : aut(aut) { - }; + } twa_run(const twa_run& run); twa_run& operator=(const twa_run& run); + + /// \brief Display a twa_run. + /// + /// Output the prefix and cycle parts of the twa_run \a run on \a os. + /// + /// The automaton object (stored by \a run) is used only to format + /// the states, and to know how to print the BDDs describing the + /// conditions and acceptance conditions of the run; it is + /// not used to replay the run. In other words this + /// function will work even if the twa_run you are trying to print + /// appears to connect states that are not connected. + /// + /// This is unlike replay_twa_run(), which will ensure the run + /// actually exists in the automaton (and will also display any + /// transition annotation). + SPOT_API + friend std::ostream& operator<<(std::ostream& os, const twa_run_ptr& run); }; - /// \brief Display a twa_run. - /// - /// Output the prefix and cycle parts of the twa_run \a run on \a os. - /// - /// The automaton \a a is used only to format the states, and - /// to know how to print the BDDs describing the conditions and - /// acceptance conditions of the run; it is not used to - /// replay the run. In other words this function will work even if - /// the twa_run you are trying to print appears to connect states - /// of \a a that are not connected. - /// - /// This is unlike replay_twa_run(), which will ensure the run - /// actually exists in the automaton (and will also display any - /// transition annotation). - SPOT_API std::ostream& - print_twa_run(std::ostream& os, - const const_twa_ptr& a, - const const_twa_run_ptr& run); /// \brief Return an explicit_tgba corresponding to \a run (i.e. comparable /// states are merged). diff --git a/src/twaalgos/gtec/ce.cc b/src/twaalgos/gtec/ce.cc index 71a4fcf12..dff850ffb 100644 --- a/src/twaalgos/gtec/ce.cc +++ b/src/twaalgos/gtec/ce.cc @@ -94,7 +94,7 @@ namespace spot twa_run_ptr couvreur99_check_result::accepting_run() { - run_ = std::make_shared(); + run_ = std::make_shared(ecs_->aut); assert(!ecs_->root.empty()); diff --git a/src/twaalgos/gv04.cc b/src/twaalgos/gv04.cc index dcdea7af5..8b568a5f9 100644 --- a/src/twaalgos/gv04.cc +++ b/src/twaalgos/gv04.cc @@ -287,7 +287,7 @@ namespace spot virtual twa_run_ptr accepting_run() { - auto res = std::make_shared(); + auto res = std::make_shared(automaton()); update_lowlinks(); #ifdef TRACE diff --git a/src/twaalgos/magic.cc b/src/twaalgos/magic.cc index 1302b12f3..034e2f2e1 100644 --- a/src/twaalgos/magic.cc +++ b/src/twaalgos/magic.cc @@ -333,7 +333,7 @@ namespace spot assert(!ms_->st_blue.empty()); assert(!ms_->st_red.empty()); - auto run = std::make_shared(); + auto run = std::make_shared(automaton()); typename stack_type::const_reverse_iterator i, j, end; twa_run::steps* l; diff --git a/src/twaalgos/ndfs_result.hxx b/src/twaalgos/ndfs_result.hxx index 6ea6b32a2..edaaa72e8 100644 --- a/src/twaalgos/ndfs_result.hxx +++ b/src/twaalgos/ndfs_result.hxx @@ -194,7 +194,7 @@ namespace spot assert(!acc_trans.empty()); - auto run = std::make_shared(); + auto run = std::make_shared(automaton()); // construct run->cycle from acc_trans. construct_cycle(run, acc_trans); // construct run->prefix (a minimal path from the initial state to any diff --git a/src/twaalgos/projrun.cc b/src/twaalgos/projrun.cc index 24790a41d..8c36995bc 100644 --- a/src/twaalgos/projrun.cc +++ b/src/twaalgos/projrun.cc @@ -32,7 +32,7 @@ namespace spot const const_twa_ptr& a_proj, const const_twa_run_ptr& run) { - auto res = std::make_shared(); + auto res = std::make_shared(a_proj); for (auto& i: run->prefix) res->prefix.emplace_back(a_run->project_state(i.s, a_proj), i.label, i.acc); diff --git a/src/twaalgos/reducerun.cc b/src/twaalgos/reducerun.cc index 9b0b1c9ca..4813e34e4 100644 --- a/src/twaalgos/reducerun.cc +++ b/src/twaalgos/reducerun.cc @@ -88,9 +88,10 @@ namespace spot } twa_run_ptr - reduce_run(const const_twa_ptr& a, const const_twa_run_ptr& org) + reduce_run(const const_twa_run_ptr& org) { - auto res = std::make_shared(); + auto& a = org->aut; + auto res = std::make_shared(a); state_set ss; shortest_path shpath(a); shpath.set_target(&ss); diff --git a/src/twaalgos/reducerun.hh b/src/twaalgos/reducerun.hh index db6a58558..f95c9759f 100644 --- a/src/twaalgos/reducerun.hh +++ b/src/twaalgos/reducerun.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2010, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita. // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -31,8 +31,8 @@ namespace spot /// \ingroup twa_run /// \brief Reduce an accepting run. /// - /// Return a run which is accepting for \a a and that is no longer - /// than \a org. + /// Return a run which is still accepting for org->aut, + /// but is no longer than \a org. SPOT_API twa_run_ptr - reduce_run(const const_twa_ptr& a, const const_twa_run_ptr& org); + reduce_run(const const_twa_run_ptr& org); } diff --git a/src/twaalgos/replayrun.cc b/src/twaalgos/replayrun.cc index c9fcdc8a2..f330ded0e 100644 --- a/src/twaalgos/replayrun.cc +++ b/src/twaalgos/replayrun.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -44,9 +44,10 @@ namespace spot } bool - replay_twa_run(std::ostream& os, const const_twa_ptr& a, + replay_twa_run(std::ostream& os, const const_twa_run_ptr& run, bool debug) { + auto& a = run->aut; const state* s = a->get_init_state(); int serial = 1; const twa_run::steps* l; diff --git a/src/twaalgos/replayrun.hh b/src/twaalgos/replayrun.hh index 3fc86e646..b95ca342a 100644 --- a/src/twaalgos/replayrun.hh +++ b/src/twaalgos/replayrun.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -34,21 +34,19 @@ namespace spot /// \ingroup twa_run /// \brief Replay a twa_run on a tgba. /// - /// This is similar to print_twa_run(), except that the run is + /// This is similar to os << 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 + /// by spot::twa::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 SPOT_API bool replay_twa_run(std::ostream& os, - const const_twa_ptr& a, - const const_twa_run_ptr& run, - bool debug = false); + const const_twa_run_ptr& run, + bool debug = false); } diff --git a/src/twaalgos/se05.cc b/src/twaalgos/se05.cc index 13f7841e8..b90182d3e 100644 --- a/src/twaalgos/se05.cc +++ b/src/twaalgos/se05.cc @@ -339,7 +339,7 @@ namespace spot assert(!ms_->st_blue.empty()); assert(!ms_->st_red.empty()); - auto run = std::make_shared(); + auto run = std::make_shared(automaton()); typename stack_type::const_reverse_iterator i, j, end; twa_run::steps* l; diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in index 1dd661c1a..3aebc0a31 100755 --- a/wrap/python/ajax/spotcgi.in +++ b/wrap/python/ajax/spotcgi.in @@ -840,11 +840,8 @@ if output_type == 'r': unbufprint('
An accepting run was found.
') if ec_run: if print_acc_run: - s = spot.ostringstream() - spot.print_twa_run(s, ec_a, ec_run) unbufprint('
%s
' % - cgi.escape(s.str())) - del s + cgi.escape(str(ec_run))) if draw_acc_run: render_automaton(spot.twa_run_to_tgba(ec_a, ec_run), False) del ec_run diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 22b20c87c..298f08a63 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -383,6 +383,15 @@ namespace std { } } +%extend spot::twa_run_ptr { + std::string __str__() + { + std::ostringstream os; + os << *self; + return os.str(); + } +} + %nodefaultctor std::ostream; namespace std { class ostream {};