diff --git a/NEWS b/NEWS index ad4324de037e6270a3daeea70d4e24926deb20af..b10103d37c4cb69a7c441385412cde5543a9c300 100644 --- a/NEWS +++ b/NEWS @@ -52,6 +52,7 @@ New in spot 1.99.4a (not yet released) ltl_simplifier -> tl_simplifier tgba_statistics::transitions -> twa_statistics::edges tgba_sub_statistics::sub_transitions -> twa_sub_statistics::transitions + tgba_run -> twa_run Python: diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index 749c8620ce3d4fa5bb9a87c5d1c4f298cb99d995..0375c88c335fca26b329d08099f5018cda64bf8d 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -314,7 +314,7 @@ checked_main(int argc, char **argv) else if (accepting_run) { - spot::tgba_run_ptr run; + spot::twa_run_ptr run; tm.start("computing accepting run"); try { @@ -340,7 +340,7 @@ checked_main(int argc, char **argv) tm.stop("reducing accepting run"); tm.start("printing accepting run"); - spot::print_tgba_run(std::cout, product, run); + spot::print_twa_run(std::cout, product, run); tm.stop("printing accepting run"); } } diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc index aba54c06c5350dbdf1e3b4068007f96b3eb7e6c2..6a62eca423c8ec8a60c1738aee8d5306746ed0b4 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_tgba_run(std::cout, ec->automaton(), run); + spot::print_twa_run(std::cout, ec->automaton(), run); } } else diff --git a/src/tests/emptchk.cc b/src/tests/emptchk.cc index c75372ffd3f254bb116e085400005065ed166f96..093722ffcff9460cb7405f8d48ddd0fe33b299e9 100644 --- a/src/tests/emptchk.cc +++ b/src/tests/emptchk.cc @@ -161,7 +161,7 @@ main(int argc, char** argv) std::cout << ce_found << " counterexample found\n"; if (auto run = res->accepting_run()) { - auto ar = spot::tgba_run_to_tgba(a, run); + auto ar = spot::twa_run_to_tgba(a, run); spot::print_dot(std::cout, ar); } std::cout << '\n'; diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index a76861bd785f14d16e9d9468acae1836fa1f048d..a1eceec86ee8aa2eb0c26135af5b384b3aa729fa 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -1586,7 +1586,7 @@ checked_main(int argc, char** argv) if (accepting_run_replay) { tm.start("replaying acc. run"); - if (!spot::replay_tgba_run(std::cout, a, + if (!spot::replay_twa_run(std::cout, a, run, true)) exit_code = 1; tm.stop("replaying acc. run"); @@ -1596,12 +1596,12 @@ checked_main(int argc, char** argv) tm.start("printing accepting run"); if (graph_run_tgba_opt) { - auto ar = spot::tgba_run_to_tgba(a, run); + auto ar = spot::twa_run_to_tgba(a, run); spot::print_dot(std::cout, ar); } else { - spot::print_tgba_run(std::cout, a, run); + spot::print_twa_run(std::cout, a, run); } tm.stop("printing accepting run"); } diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index be80aa490250a82005d582dcf4b9f697064a1d64..f4e8196ae1cea22654f1590f0c4d5370fd6702bb 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -379,7 +379,7 @@ struct ar_stat } void - count(const spot::const_tgba_run_ptr& run) + count(const spot::const_twa_run_ptr& run) { int p = run->prefix.size(); int c = run->cycle.size(); @@ -986,7 +986,7 @@ main(int argc, char** argv) ++n_non_empty; if (opt_replay) { - spot::tgba_run_ptr run; + spot::twa_run_ptr run; bool done = false; tm_ar.start(algo); for (int count = opt_R;;) @@ -1026,7 +1026,7 @@ main(int argc, char** argv) { tm_ar.stop(algo); std::ostringstream s; - if (!spot::replay_tgba_run(s, + if (!spot::replay_twa_run(s, res->automaton(), run)) { @@ -1051,7 +1051,7 @@ main(int argc, char** argv) { auto redrun = spot::reduce_run(res->automaton(), run); - if (!spot::replay_tgba_run(s, + if (!spot::replay_twa_run(s, res ->automaton(), redrun)) diff --git a/src/twa/twa.hh b/src/twa/twa.hh index aa8add15b69a44af7fc9707e1ee948610b92a973..f1ceae30198c3c8a1f2101b7d12095656cdc8e3a 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -642,7 +642,7 @@ namespace spot /// is the empty string. /// /// This method is used for instance in print_dot(), - /// and replay_tgba_run(). + /// and replay_twa_run(). /// /// \param t a non-done twa_succ_iterator for this automaton virtual std::string diff --git a/src/twaalgos/bfssteps.cc b/src/twaalgos/bfssteps.cc index b2e7ac84fbd349d6e67386f7508d8a8817ac4ba2..2248c3494e87d30350b9bd75696bf7c5eea4604a 100644 --- a/src/twaalgos/bfssteps.cc +++ b/src/twaalgos/bfssteps.cc @@ -38,20 +38,20 @@ namespace spot } void - bfs_steps::finalize(const std::map& father, const tgba_run::step& s, - const state* start, tgba_run::steps& l) + bfs_steps::finalize(const std::map& father, const twa_run::step& s, + const state* start, twa_run::steps& l) { - tgba_run::steps p; - tgba_run::step current = s; + twa_run::steps p; + twa_run::step current = s; for (;;) { - tgba_run::step tmp = current; + twa_run::step tmp = current; tmp.s = tmp.s->clone(); p.push_front(tmp); if (current.s == start) break; - std::map::const_iterator it = father.find(current.s); assert(it != father.end()); current = it->second; @@ -60,11 +60,11 @@ namespace spot } const state* - bfs_steps::search(const state* start, tgba_run::steps& l) + bfs_steps::search(const state* start, twa_run::steps& l) { // Records backlinks to parent state during the BFS. // (This also stores the propositions of this link.) - std::map father; // BFS queue. std::deque todo; @@ -84,7 +84,7 @@ namespace spot bdd cond = i->current_condition(); acc_cond::mark_t acc = i->current_acceptance_conditions(); - tgba_run::step s = { src, cond, acc }; + twa_run::step s = { src, cond, acc }; if (match(s, dest)) { diff --git a/src/twaalgos/bfssteps.hh b/src/twaalgos/bfssteps.hh index f6df574cdafb90b48bfdd8ebb5e229bdb554e47e..c704ee11020f0be3e0bdb0c5f29bc37b4117786f 100644 --- a/src/twaalgos/bfssteps.hh +++ b/src/twaalgos/bfssteps.hh @@ -28,7 +28,7 @@ namespace spot { /// \ingroup twa_misc - /// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps. + /// \brief Make a BFS in a spot::tgba to compute a twa_run::steps. /// /// This class should be used to compute the shortest path /// between a state of a spot::tgba and the first transition or @@ -48,7 +48,7 @@ namespace spot /// /// \return the destination state of the last step (not included /// in \a l) if a matching path was found, or 0 otherwise. - const state* search(const state* start, tgba_run::steps& l); + const state* search(const state* start, twa_run::steps& l); /// \brief Return a state* that is unique for \a a. /// @@ -82,7 +82,7 @@ namespace spot /// and when this happens the list argument of search() is be /// augmented with the shortest past that ends with this /// transition. - virtual bool match(tgba_run::step& step, const state* dest) = 0; + virtual bool match(twa_run::step& step, const state* dest) = 0; /// \brief Append the resulting path to the resulting run. /// @@ -90,11 +90,11 @@ namespace spot /// resulting path to \a l. This seldom needs to be overridden, /// unless you do not want \a l to be updated (in which case an empty /// finalize() will do). - virtual void finalize(const std::map& father, - const tgba_run::step& s, + const twa_run::step& s, const state* start, - tgba_run::steps& l); + twa_run::steps& l); protected: const_twa_ptr a_; ///< The spot::tgba we are searching into. diff --git a/src/twaalgos/emptiness.cc b/src/twaalgos/emptiness.cc index fd0f376090bc6e4c8f943273b3a4d8d6bc6aba75..cd943d2d4cf111b52e17efb161db0620ab48ecfe 100644 --- a/src/twaalgos/emptiness.cc +++ b/src/twaalgos/emptiness.cc @@ -34,10 +34,10 @@ namespace spot { - // tgba_run + // twa_run ////////////////////////////////////////////////////////////////////// - tgba_run::~tgba_run() + twa_run::~twa_run() { for (auto i : prefix) i.s->destroy(); @@ -45,7 +45,7 @@ namespace spot i.s->destroy(); } - tgba_run::tgba_run(const tgba_run& run) + twa_run::twa_run(const twa_run& run) { for (steps::const_iterator i = run.prefix.begin(); i != run.prefix.end(); ++i) @@ -61,28 +61,28 @@ namespace spot } } - tgba_run& - tgba_run::operator=(const tgba_run& run) + twa_run& + twa_run::operator=(const twa_run& run) { if (&run != this) { - this->~tgba_run(); - new(this) tgba_run(run); + this->~twa_run(); + new(this) twa_run(run); } return *this; } - // print_tgba_run + // print_twa_run ////////////////////////////////////////////////////////////////////// std::ostream& - print_tgba_run(std::ostream& os, + print_twa_run(std::ostream& os, const const_twa_ptr& a, - const const_tgba_run_ptr& run) + const const_twa_run_ptr& run) { bdd_dict_ptr d = a->get_dict(); os << "Prefix:" << std::endl; - for (tgba_run::steps::const_iterator i = run->prefix.begin(); + for (twa_run::steps::const_iterator i = run->prefix.begin(); i != run->prefix.end(); ++i) { os << " " << a->format_state(i->s) << std::endl; @@ -93,7 +93,7 @@ namespace spot os << std::endl; } os << "Cycle:" << std::endl; - for (tgba_run::steps::const_iterator i = run->cycle.begin(); + for (twa_run::steps::const_iterator i = run->cycle.begin(); i != run->cycle.end(); ++i) { os << " " << a->format_state(i->s) << std::endl; @@ -109,7 +109,7 @@ namespace spot // emptiness_check_result ////////////////////////////////////////////////////////////////////// - tgba_run_ptr + twa_run_ptr emptiness_check_result::accepting_run() { return nullptr; @@ -287,11 +287,11 @@ namespace spot return nullptr; } - // tgba_run_to_tgba + // twa_run_to_tgba ////////////////////////////////////////////////////////////////////// twa_graph_ptr - tgba_run_to_tgba(const const_twa_ptr& a, const const_tgba_run_ptr& run) + twa_run_to_tgba(const const_twa_ptr& a, const const_twa_run_ptr& run) { auto d = a->get_dict(); auto res = make_twa_graph(d); @@ -301,7 +301,7 @@ namespace spot const state* s = a->get_init_state(); unsigned src; unsigned dst; - const tgba_run::steps* l; + const twa_run::steps* l; acc_cond::mark_t seen_acc = 0U; typedef std::unordered_mapprefix; - tgba_run::steps::const_iterator i = l->begin(); + twa_run::steps::const_iterator i = l->begin(); assert(s->compare(i->s) == 0); src = res->new_state(); diff --git a/src/twaalgos/emptiness.hh b/src/twaalgos/emptiness.hh index 97d4c27dc6fb93dea4249fe9d85dd0d718488ab5..09b371933ac6fa4df52b4e49ce6f430087ee625b 100644 --- a/src/twaalgos/emptiness.hh +++ b/src/twaalgos/emptiness.hh @@ -32,9 +32,9 @@ namespace spot { - struct tgba_run; - typedef std::shared_ptr tgba_run_ptr; - typedef std::shared_ptr const_tgba_run_ptr; + struct twa_run; + typedef std::shared_ptr twa_run_ptr; + typedef std::shared_ptr const_twa_run_ptr; /// \addtogroup emptiness_check Emptiness-checks /// \ingroup twa_algorithms @@ -64,7 +64,7 @@ namespace spot /// /// The acceptance run returned by /// spot::emptiness_check_result::accepting_run(), if any, is of - /// type spot::tgba_run. \ref tgba_run "This page" gathers existing + /// type spot::twa_run. \ref twa_run "This page" gathers existing /// operations on these objects. /// /// @{ @@ -100,7 +100,7 @@ namespace spot /// cannot produce a counter example (that does not mean there /// is no counter-example; the mere existence of an instance of /// this class asserts the existence of a counter-example). - virtual tgba_run_ptr accepting_run(); + virtual twa_run_ptr accepting_run(); /// The automaton on which an accepting_run() was found. const const_twa_ptr& @@ -263,7 +263,7 @@ namespace spot /// @{ /// An accepted run, for a tgba. - struct SPOT_API tgba_run + struct SPOT_API twa_run { struct step { const state* s; @@ -284,39 +284,39 @@ namespace spot steps prefix; steps cycle; - ~tgba_run(); - tgba_run() + ~twa_run(); + twa_run() { }; - tgba_run(const tgba_run& run); - tgba_run& operator=(const tgba_run& run); + twa_run(const twa_run& run); + twa_run& operator=(const twa_run& run); }; - /// \brief Display a tgba_run. + /// \brief Display a twa_run. /// - /// Output the prefix and cycle parts of the tgba_run \a run on \a os. + /// 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 tgba_run you are trying to print appears to connect states + /// the twa_run you are trying to print appears to connect states /// of \a a that are not connected. /// - /// This is unlike replay_tgba_run(), which will ensure the run + /// 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_tgba_run(std::ostream& os, + print_twa_run(std::ostream& os, const const_twa_ptr& a, - const const_tgba_run_ptr& run); + const const_twa_run_ptr& 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. SPOT_API twa_graph_ptr - tgba_run_to_tgba(const const_twa_ptr& a, const const_tgba_run_ptr& run); + twa_run_to_tgba(const const_twa_ptr& a, const const_twa_run_ptr& run); /// @} diff --git a/src/twaalgos/gtec/ce.cc b/src/twaalgos/gtec/ce.cc index bb73562eb6e4010c17319cc73bfde2bf9b2ab370..71a4fcf12bf99bf64425c6f06b02858eb8f9c569 100644 --- a/src/twaalgos/gtec/ce.cc +++ b/src/twaalgos/gtec/ce.cc @@ -39,7 +39,7 @@ namespace spot } const state* - search(const state* start, tgba_run::steps& l) + search(const state* start, twa_run::steps& l) { return this->bfs_steps::search(filter(start), l); } @@ -60,7 +60,7 @@ namespace spot } bool - match(tgba_run::step&, const state* dest) + match(twa_run::step&, const state* dest) { return target->find(dest) != target->end(); } @@ -91,10 +91,10 @@ namespace spot return count; } - tgba_run_ptr + twa_run_ptr couvreur99_check_result::accepting_run() { - run_ = std::make_shared(); + run_ = std::make_shared(); assert(!ecs_->root.empty()); @@ -106,7 +106,7 @@ namespace spot // Register all states from the cycle as target of the BFS. state_set ss; - for (tgba_run::steps::const_iterator i = run_->cycle.begin(); + for (twa_run::steps::const_iterator i = run_->cycle.begin(); i != run_->cycle.end(); ++i) ss.insert(i->s); shortest_path shpath(&ss, ecs_, this); @@ -132,7 +132,7 @@ namespace spot } // Locate cycle_entry_point on the cycle. - tgba_run::steps::iterator cycle_ep_it; + twa_run::steps::iterator cycle_ep_it; for (cycle_ep_it = run_->cycle.begin(); cycle_ep_it != run_->cycle.end() && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) @@ -201,7 +201,7 @@ namespace spot } virtual bool - match(tgba_run::step& st, const state* s) + match(twa_run::step& st, const state* s) { acc_cond::mark_t less_acc = acc_to_traverse - st.acc; diff --git a/src/twaalgos/gtec/ce.hh b/src/twaalgos/gtec/ce.hh index 71be722f950906cc2ebd39a7246ee33de683eafb..8b3fadf3c2b2f3ede3edb8e9f58b4f3a4df76c71 100644 --- a/src/twaalgos/gtec/ce.hh +++ b/src/twaalgos/gtec/ce.hh @@ -38,7 +38,7 @@ namespace spot std::shared_ptr& ecs, option_map o = option_map()); - virtual tgba_run_ptr accepting_run(); + virtual twa_run_ptr accepting_run(); void print_stats(std::ostream& os) const; @@ -51,6 +51,6 @@ namespace spot private: std::shared_ptr ecs_; - tgba_run_ptr run_; + twa_run_ptr run_; }; } diff --git a/src/twaalgos/gv04.cc b/src/twaalgos/gv04.cc index 65c37005e2d37466daf78e6a33498ab8f9368c10..dcdea7af56edb381282b2c0b8a074298fc632533 100644 --- a/src/twaalgos/gv04.cc +++ b/src/twaalgos/gv04.cc @@ -284,10 +284,10 @@ namespace spot return s; } - virtual tgba_run_ptr + virtual twa_run_ptr accepting_run() { - auto res = std::make_shared(); + auto res = std::make_shared(); update_lowlinks(); #ifdef TRACE @@ -309,7 +309,7 @@ namespace spot int father = data.stack[scc_root].pre; while (father >= 0) { - tgba_run::step st = + twa_run::step st = { data.stack[father].s->clone(), data.stack[father].lasttr->current_condition(), @@ -360,7 +360,7 @@ namespace spot } virtual bool - match(tgba_run::step& step, const state*) + match(twa_run::step& step, const state*) { return step.acc != 0U; } @@ -375,7 +375,7 @@ namespace spot } virtual bool - match(tgba_run::step&, const state* s) + match(twa_run::step&, const state* s) { return s == target; } diff --git a/src/twaalgos/magic.cc b/src/twaalgos/magic.cc index 9d4f5b0e36f1655096ec780c53aab14427b3a0d7..1302b12f36504dd21d35522518cef6c91dc0fc14 100644 --- a/src/twaalgos/magic.cc +++ b/src/twaalgos/magic.cc @@ -328,15 +328,15 @@ namespace spot { } - virtual tgba_run_ptr accepting_run() + virtual twa_run_ptr accepting_run() { assert(!ms_->st_blue.empty()); assert(!ms_->st_red.empty()); - auto run = std::make_shared(); + auto run = std::make_shared(); typename stack_type::const_reverse_iterator i, j, end; - tgba_run::steps* l; + twa_run::steps* l; l = &run->prefix; @@ -345,21 +345,21 @@ namespace spot j = i; ++j; for (; i != end; ++i, ++j) { - tgba_run::step s = { i->s->clone(), j->label, j->acc }; + twa_run::step s = { i->s->clone(), j->label, j->acc }; l->push_back(s); } l = &run->cycle; j = ms_->st_red.rbegin(); - tgba_run::step s = { i->s->clone(), j->label, j->acc }; + twa_run::step s = { i->s->clone(), j->label, j->acc }; l->push_back(s); i = j; ++j; end = ms_->st_red.rend(); --end; for (; i != end; ++i, ++j) { - tgba_run::step s = { i->s->clone(), j->label, j->acc }; + twa_run::step s = { i->s->clone(), j->label, j->acc }; l->push_back(s); } @@ -408,7 +408,7 @@ namespace spot delete computer; } - virtual tgba_run_ptr accepting_run() + virtual twa_run_ptr accepting_run() { return computer->accepting_run(); } diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index aff462559cae092498efb1a2039a7427d9644c81..26adcdc54e7f145934635e9104103be9060b48b3 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -197,7 +197,7 @@ namespace spot } virtual bool - match(tgba_run::step&, const state* to) + match(twa_run::step&, const state* to) { return to == dest; } @@ -220,14 +220,14 @@ namespace spot // Find a loop around START in SCC #n. wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start); - tgba_run::steps loop; + twa_run::steps loop; const state* reached = wsal.search(start, loop); assert(reached == start); (void)reached; // Build an automaton representing this loop. auto loop_a = make_twa_graph(det_a->get_dict()); - tgba_run::steps::const_iterator i; + twa_run::steps::const_iterator i; int loop_size = loop.size(); loop_a->new_states(loop_size); int n; diff --git a/src/twaalgos/ndfs_result.hxx b/src/twaalgos/ndfs_result.hxx index b9caf317a45c59199a3461fd64fdb5f3c6cfca73..6ea6b32a2b73ea579b4a443f1b32332163d3d863 100644 --- a/src/twaalgos/ndfs_result.hxx +++ b/src/twaalgos/ndfs_result.hxx @@ -104,7 +104,7 @@ namespace spot { } - virtual tgba_run_ptr accepting_run() + virtual twa_run_ptr accepting_run() { const stack_type& stb = ms_->get_st_blue(); const stack_type& str = ms_->get_st_red(); @@ -194,7 +194,7 @@ namespace spot assert(!acc_trans.empty()); - auto run = std::make_shared(); + auto run = std::make_shared(); // construct run->cycle from acc_trans. construct_cycle(run, acc_trans); // construct run->prefix (a minimal path from the initial state to any @@ -389,7 +389,7 @@ namespace spot } } - const state* search(const state* start, tgba_run::steps& l) + const state* search(const state* start, twa_run::steps& l) { const state* s = filter(start); if (s) @@ -412,9 +412,9 @@ namespace spot return s; } - void finalize(const std::map&, - const tgba_run::step&, const state*, tgba_run::steps&) + const twa_run::step&, const state*, twa_run::steps&) { } @@ -423,7 +423,7 @@ namespace spot return seen; } - bool match(tgba_run::step&, const state* dest) + bool match(twa_run::step&, const state* dest) { return target->compare(dest) == 0; } @@ -438,7 +438,7 @@ namespace spot bool search(const state* start, const state* target, state_set& dead) { - tgba_run::steps path; + twa_run::steps path; if (start->compare(target) == 0) return true; @@ -484,7 +484,7 @@ namespace spot } } - const state* search(const state* start, tgba_run::steps& l) + const state* search(const state* start, twa_run::steps& l) { const state* s = filter(start); if (s) @@ -514,7 +514,7 @@ namespace spot return s; } - bool match(tgba_run::step&, const state* dest) + bool match(twa_run::step&, const state* dest) { ndfsr_trace << "match: " << a_->format_state(dest) << std::endl; @@ -528,7 +528,7 @@ namespace spot const heap& h; }; - void construct_cycle(tgba_run_ptr run, + void construct_cycle(twa_run_ptr run, const accepting_transitions_list& acc_trans) { assert(!acc_trans.empty()); @@ -551,7 +551,7 @@ namespace spot ndfsr_trace << "(self loop " << a_->format_state(i->source) << " -> " << a_->format_state(i->dest) << " ignored) "; - tgba_run::step st = { i->source->clone(), i->label, i->acc }; + twa_run::step st = { i->source->clone(), i->label, i->acc }; run->cycle.push_back(st); } else @@ -563,7 +563,7 @@ namespace spot } ndfsr_trace << std::endl; - tgba_run::step st = { current.source->clone(), current.label, + twa_run::step st = { current.source->clone(), current.label, current.acc }; run->cycle.push_back(st); @@ -590,7 +590,7 @@ namespace spot } current = i->second; // complete the path with the corresponding transition - tgba_run::step st = { current.source->clone(), current.label, + twa_run::step st = { current.source->clone(), current.label, current.acc }; run->cycle.push_back(st); // remove this source state of target @@ -617,7 +617,7 @@ namespace spot } } - void construct_prefix(tgba_run_ptr run) + void construct_prefix(twa_run_ptr run) { m_source_trans target; transition tmp; @@ -625,7 +625,7 @@ namespace spot tmp.acc = 0U; // Register all states from the cycle as target of the BFS. - for (tgba_run::steps::const_iterator i = run->cycle.begin(); + for (twa_run::steps::const_iterator i = run->cycle.begin(); i != run->cycle.end(); ++i) target.emplace(i->s, tmp); @@ -653,7 +653,7 @@ namespace spot } // Locate cycle_entry_point on the cycle. - tgba_run::steps::iterator cycle_ep_it; + twa_run::steps::iterator cycle_ep_it; for (cycle_ep_it = run->cycle.begin(); cycle_ep_it != run->cycle.end() && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) diff --git a/src/twaalgos/projrun.cc b/src/twaalgos/projrun.cc index fb665ba25c81082bf9075079c317ce05f23495f4..24790a41ddd3f2a897f4d313a3bface89a03dea3 100644 --- a/src/twaalgos/projrun.cc +++ b/src/twaalgos/projrun.cc @@ -27,12 +27,12 @@ namespace spot { - tgba_run_ptr - project_tgba_run(const const_twa_ptr& a_run, + twa_run_ptr + project_twa_run(const const_twa_ptr& a_run, const const_twa_ptr& a_proj, - const const_tgba_run_ptr& run) + const const_twa_run_ptr& run) { - auto res = std::make_shared(); + auto res = std::make_shared(); 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/projrun.hh b/src/twaalgos/projrun.hh index d93305c912bafc2f0847fa10803c1b46bed3160a..6f5ca025319ec78818c5b44d998893c2f669e1af 100644 --- a/src/twaalgos/projrun.hh +++ b/src/twaalgos/projrun.hh @@ -29,20 +29,20 @@ namespace spot { - struct tgba_run; + struct twa_run; /// \ingroup twa_run - /// \brief Project a tgba_run on a tgba. + /// \brief Project a twa_run on a tgba. /// - /// If a tgba_run has been generated on a product, or any other + /// If a twa_run has been generated on a product, or any other /// on-the-fly algorithm with tgba operands, /// /// \param run the run to replay /// \param a_run the automata on which the run was generated /// \param a_proj the automata on which to project the run /// \return true iff the run could be completed - SPOT_API tgba_run_ptr - project_tgba_run(const const_twa_ptr& a_run, + SPOT_API twa_run_ptr + project_twa_run(const const_twa_ptr& a_run, const const_twa_ptr& a_proj, - const const_tgba_run_ptr& run); + const const_twa_run_ptr& run); } diff --git a/src/twaalgos/reducerun.cc b/src/twaalgos/reducerun.cc index 287017c78cb7d1bf8eb886bb354a0cf14778dcc9..9b0b1c9ca43b2f6e8e322a36c269a716511fa8f7 100644 --- a/src/twaalgos/reducerun.cc +++ b/src/twaalgos/reducerun.cc @@ -56,7 +56,7 @@ namespace spot } const state* - search(const state* start, tgba_run::steps& l) + search(const state* start, twa_run::steps& l) { return this->bfs_steps::search(filter(start), l); } @@ -76,7 +76,7 @@ namespace spot } bool - match(tgba_run::step&, const state* dest) + match(twa_run::step&, const state* dest) { return target->find(dest) != target->end(); } @@ -87,10 +87,10 @@ namespace spot }; } - tgba_run_ptr - reduce_run(const const_twa_ptr& a, const const_tgba_run_ptr& org) + twa_run_ptr + reduce_run(const const_twa_ptr& a, const const_twa_run_ptr& org) { - auto res = std::make_shared(); + auto res = std::make_shared(); state_set ss; shortest_path shpath(a); shpath.set_target(&ss); @@ -104,7 +104,7 @@ namespace spot // Start from the end of the original cycle, and rewind until all // acceptance sets have been seen. acc_cond::mark_t seen_acc = 0U; - tgba_run::steps::const_iterator seg = org->cycle.end(); + twa_run::steps::const_iterator seg = org->cycle.end(); do { assert(seg != org->cycle.begin()); @@ -122,7 +122,7 @@ namespace spot assert(seg != org->cycle.end()); seen_acc |= seg->acc; - tgba_run::step st = { seg->s->clone(), seg->label, seg->acc }; + twa_run::step st = { seg->s->clone(), seg->label, seg->acc }; res->cycle.push_back(st); ++seg; @@ -145,7 +145,7 @@ namespace spot // state of the automata to any state of the cycle. // Register all states from the cycle as target of the BFS. - for (tgba_run::steps::const_iterator i = res->cycle.begin(); + for (twa_run::steps::const_iterator i = res->cycle.begin(); i != res->cycle.end(); ++i) ss.insert(i->s); @@ -170,7 +170,7 @@ namespace spot } // Locate cycle_entry_point on the cycle. - tgba_run::steps::iterator cycle_ep_it; + twa_run::steps::iterator cycle_ep_it; for (cycle_ep_it = res->cycle.begin(); cycle_ep_it != res->cycle.end() && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) diff --git a/src/twaalgos/reducerun.hh b/src/twaalgos/reducerun.hh index a9aace3a4073952b19662e96053535df1840959b..db6a58558e91f8e249cd82f0d7ee08dac2cc224a 100644 --- a/src/twaalgos/reducerun.hh +++ b/src/twaalgos/reducerun.hh @@ -33,6 +33,6 @@ namespace spot /// /// Return a run which is accepting for \a a and that is no longer /// than \a org. - SPOT_API tgba_run_ptr - reduce_run(const const_twa_ptr& a, const const_tgba_run_ptr& org); + SPOT_API twa_run_ptr + reduce_run(const const_twa_ptr& a, const const_twa_run_ptr& org); } diff --git a/src/twaalgos/replayrun.cc b/src/twaalgos/replayrun.cc index acd4b43f171f5535bca4939acb47d6498eb43cbb..c9fcdc8a27e9f9ef49a2d86499121078b9ee1a3f 100644 --- a/src/twaalgos/replayrun.cc +++ b/src/twaalgos/replayrun.cc @@ -44,12 +44,12 @@ namespace spot } bool - replay_tgba_run(std::ostream& os, const const_twa_ptr& a, - const const_tgba_run_ptr& run, bool debug) + replay_twa_run(std::ostream& os, const const_twa_ptr& a, + const const_twa_run_ptr& run, bool debug) { const state* s = a->get_init_state(); int serial = 1; - const tgba_run::steps* l; + const twa_run::steps* l; std::string in; acc_cond::mark_t all_acc = 0U; bool all_acc_seen = false; @@ -72,7 +72,7 @@ namespace spot os << "Prefix:\n"; } - tgba_run::steps::const_iterator i = l->begin(); + twa_run::steps::const_iterator i = l->begin(); if (s->compare(i->s)) { diff --git a/src/twaalgos/replayrun.hh b/src/twaalgos/replayrun.hh index e9f5607c34e55e96c471b76e049029e26491b21d..3fc86e6466e27a33594f4357d582cb75071d013e 100644 --- a/src/twaalgos/replayrun.hh +++ b/src/twaalgos/replayrun.hh @@ -29,12 +29,12 @@ namespace spot { - struct tgba_run; + struct twa_run; /// \ingroup twa_run - /// \brief Replay a tgba_run on a tgba. + /// \brief Replay a twa_run on a tgba. /// - /// This is similar to print_tgba_run(), except that the run is + /// This is similar to print_twa_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 @@ -47,8 +47,8 @@ namespace spot /// debugging informations will be output on failure /// \return true iff the run could be completed SPOT_API bool - replay_tgba_run(std::ostream& os, + replay_twa_run(std::ostream& os, const const_twa_ptr& a, - const const_tgba_run_ptr& run, + const const_twa_run_ptr& run, bool debug = false); } diff --git a/src/twaalgos/se05.cc b/src/twaalgos/se05.cc index 9fc245e760e7b0ab2a01070453919a14df2b4881..13f7841e81fc703f3e52cf5165ffde5678e4d9a7 100644 --- a/src/twaalgos/se05.cc +++ b/src/twaalgos/se05.cc @@ -334,15 +334,15 @@ namespace spot { } - virtual tgba_run_ptr accepting_run() + virtual twa_run_ptr accepting_run() { assert(!ms_->st_blue.empty()); assert(!ms_->st_red.empty()); - auto run = std::make_shared(); + auto run = std::make_shared(); typename stack_type::const_reverse_iterator i, j, end; - tgba_run::steps* l; + twa_run::steps* l; const state* target = ms_->st_red.front().s; @@ -355,7 +355,7 @@ namespace spot { if (l == &run->prefix && i->s->compare(target) == 0) l = &run->cycle; - tgba_run::step s = { i->s->clone(), j->label, j->acc }; + twa_run::step s = { i->s->clone(), j->label, j->acc }; l->push_back(s); } @@ -364,14 +364,14 @@ namespace spot assert(l == &run->cycle); j = ms_->st_red.rbegin(); - tgba_run::step s = { i->s->clone(), j->label, j->acc }; + twa_run::step s = { i->s->clone(), j->label, j->acc }; l->push_back(s); i = j; ++j; end = ms_->st_red.rend(); --end; for (; i != end; ++i, ++j) { - tgba_run::step s = { i->s->clone(), j->label, j->acc }; + twa_run::step s = { i->s->clone(), j->label, j->acc }; l->push_back(s); } @@ -420,7 +420,7 @@ namespace spot delete computer; } - virtual tgba_run_ptr accepting_run() + virtual twa_run_ptr accepting_run() { return computer->accepting_run(); } diff --git a/src/twaalgos/word.cc b/src/twaalgos/word.cc index dbfd1e829da5f83f5748b452108f784333386b2c..6306a1d59ef61f6e04c481b5dd9e310b4a5c6e12 100644 --- a/src/twaalgos/word.cc +++ b/src/twaalgos/word.cc @@ -23,12 +23,12 @@ namespace spot { - tgba_word::tgba_word(const tgba_run_ptr run) + tgba_word::tgba_word(const twa_run_ptr run) { - for (tgba_run::steps::const_iterator i = run->prefix.begin(); + for (twa_run::steps::const_iterator i = run->prefix.begin(); i != run->prefix.end(); ++i) prefix.push_back(i->label); - for (tgba_run::steps::const_iterator i = run->cycle.begin(); + for (twa_run::steps::const_iterator i = run->cycle.begin(); i != run->cycle.end(); ++i) cycle.push_back(i->label); } diff --git a/src/twaalgos/word.hh b/src/twaalgos/word.hh index 2a37c59ece249a65716430c90969c250c15e205e..8e832ba741f273418c8e82e20a29f06e03b3ff83 100644 --- a/src/twaalgos/word.hh +++ b/src/twaalgos/word.hh @@ -28,7 +28,7 @@ namespace spot /// \brief An infinite word stored as a lasso. struct SPOT_API tgba_word { - tgba_word(const tgba_run_ptr run); + tgba_word(const twa_run_ptr run); void simplify(); std::ostream& print(std::ostream& os, const bdd_dict_ptr& d) const; diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in index 696c721768b45ceb7c5019c31990dff62e311104..1dd661c1aac3a2f0e0bc0ebfb9718d9108309c84 100755 --- a/wrap/python/ajax/spotcgi.in +++ b/wrap/python/ajax/spotcgi.in @@ -841,12 +841,12 @@ if output_type == 'r': if ec_run: if print_acc_run: s = spot.ostringstream() - spot.print_tgba_run(s, ec_a, ec_run) + spot.print_twa_run(s, ec_a, ec_run) unbufprint('
%s
' % cgi.escape(s.str())) del s if draw_acc_run: - render_automaton(spot.tgba_run_to_tgba(ec_a, ec_run), False) + render_automaton(spot.twa_run_to_tgba(ec_a, ec_run), False) del ec_run del ec_res unbufprint('') diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 13fe3b940fcec349be151b23d2caa6d785a3ae12..22b20c87c9438a4a26d5594c83e9af42442b1cb1 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -60,7 +60,7 @@ %shared_ptr(spot::taa_tgba_string) %shared_ptr(spot::taa_tgba_formula) %shared_ptr(spot::twa_safra_complement) -%shared_ptr(spot::tgba_run) +%shared_ptr(spot::twa_run) %shared_ptr(spot::emptiness_check_result) %shared_ptr(spot::emptiness_check) %shared_ptr(spot::emptiness_check_instantiator)