From 61b1f200b642568a0d225d8682b729b4abaaf5a7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 6 Mar 2016 11:40:42 +0100 Subject: [PATCH] rename tgba_reachable_iterator as twa_reachable_iterator * spot/twaalgos/reachiter.cc, spot/twaalgos/reachiter.hh: Here. * spot/twaalgos/stats.cc, spot/twaalgos/lbtt.cc: Adjust. * doc/org/upgrade2.org, NEWS: Mention the renaming. --- NEWS | 2 ++ doc/org/upgrade2.org | 3 ++ spot/twaalgos/lbtt.cc | 4 +-- spot/twaalgos/reachiter.cc | 72 +++++++++++++++++++------------------- spot/twaalgos/reachiter.hh | 32 ++++++++--------- spot/twaalgos/stats.cc | 16 ++++----- 6 files changed, 67 insertions(+), 62 deletions(-) diff --git a/NEWS b/NEWS index 445c02701..4e9243b64 100644 --- a/NEWS +++ b/NEWS @@ -7,6 +7,8 @@ New in spot 1.99.8a (not yet released) emptiness_check_instantiator::max_acceptance_conditions() renamed to emptiness_check_instantiator::min_sets() and emptiness_check_instantiator::max_sets(). + * tgba_reachable_iterator (and subclasses) was renamed to + twa_reachable_iterator for consistency. Documentation: diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 372ef5b2e..9c4bdfbf2 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -658,6 +658,9 @@ for (auto i: aut->succ(s)) | ~tgba_explicit_number~ | ~twa_graph~ | new implementation | | ~tgba_explicit_string~ | | deleted | | ~tgba_parse()~ | ~parse_aut()~ | single parser for all automata | +| ~tgba_reachable_iterator~ | ~twa_reachable_iterator~ | | +| ~tgba_reachable_iterator_breadth_first~ | ~twa_reachable_iterator_breadth_first~ | | +| ~tgba_reachable_iterator_depth_first~ | ~twa_reachable_iterator_depth_first~ | | | ~tgba_run_to_tgba()~ | ~twa_run::as_twa()~ | | | ~tgba_run~ | ~twa_run~ | | | ~tgba_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA | diff --git a/spot/twaalgos/lbtt.cc b/spot/twaalgos/lbtt.cc index 5d368cabe..d2c5453da 100644 --- a/spot/twaalgos/lbtt.cc +++ b/spot/twaalgos/lbtt.cc @@ -34,11 +34,11 @@ namespace spot { namespace { - class lbtt_bfs : public tgba_reachable_iterator_breadth_first + class lbtt_bfs final : public twa_reachable_iterator_breadth_first { public: lbtt_bfs(const const_twa_ptr& a, std::ostream& os, bool sba_format) - : tgba_reachable_iterator_breadth_first(a), + : twa_reachable_iterator_breadth_first(a), os_(os), sba_format_(sba_format), sba_(nullptr) diff --git a/spot/twaalgos/reachiter.cc b/spot/twaalgos/reachiter.cc index b07ffbd1a..7253b9f19 100644 --- a/spot/twaalgos/reachiter.cc +++ b/spot/twaalgos/reachiter.cc @@ -25,15 +25,15 @@ namespace spot { - // tgba_reachable_iterator + // twa_reachable_iterator ////////////////////////////////////////////////////////////////////// - tgba_reachable_iterator::tgba_reachable_iterator(const const_twa_ptr& a) + twa_reachable_iterator::twa_reachable_iterator(const const_twa_ptr& a) : aut_(a) { } - tgba_reachable_iterator::~tgba_reachable_iterator() + twa_reachable_iterator::~twa_reachable_iterator() { auto s = seen.begin(); while (s != seen.end()) @@ -46,7 +46,7 @@ namespace spot } void - tgba_reachable_iterator::run() + twa_reachable_iterator::run() { int n = 0; start(); @@ -90,51 +90,51 @@ namespace spot } bool - tgba_reachable_iterator::want_state(const state*) const + twa_reachable_iterator::want_state(const state*) const { return true; } void - tgba_reachable_iterator::start() + twa_reachable_iterator::start() { } void - tgba_reachable_iterator::end() + twa_reachable_iterator::end() { } void - tgba_reachable_iterator::process_state(const state*, int, + twa_reachable_iterator::process_state(const state*, int, twa_succ_iterator*) { } void - tgba_reachable_iterator::process_link(const state*, int, + twa_reachable_iterator::process_link(const state*, int, const state*, int, const twa_succ_iterator*) { } - // tgba_reachable_iterator_breadth_first + // twa_reachable_iterator_breadth_first ////////////////////////////////////////////////////////////////////// - tgba_reachable_iterator_breadth_first:: - tgba_reachable_iterator_breadth_first(const const_twa_ptr& a) - : tgba_reachable_iterator(a) + twa_reachable_iterator_breadth_first:: + twa_reachable_iterator_breadth_first(const const_twa_ptr& a) + : twa_reachable_iterator(a) { } void - tgba_reachable_iterator_breadth_first::add_state(const state* s) + twa_reachable_iterator_breadth_first::add_state(const state* s) { todo.push_back(s); } const state* - tgba_reachable_iterator_breadth_first::next_state() + twa_reachable_iterator_breadth_first::next_state() { if (todo.empty()) return nullptr; @@ -143,16 +143,16 @@ namespace spot return s; } - // tgba_reachable_iterator_depth_first + // twa_reachable_iterator_depth_first ////////////////////////////////////////////////////////////////////// - tgba_reachable_iterator_depth_first:: - tgba_reachable_iterator_depth_first(const const_twa_ptr& a) + twa_reachable_iterator_depth_first:: + twa_reachable_iterator_depth_first(const const_twa_ptr& a) : aut_(a) { } - tgba_reachable_iterator_depth_first::~tgba_reachable_iterator_depth_first() + twa_reachable_iterator_depth_first::~twa_reachable_iterator_depth_first() { auto s = seen.begin(); while (s != seen.end()) @@ -165,7 +165,7 @@ namespace spot } void - tgba_reachable_iterator_depth_first::push(const state* s, int sn) + twa_reachable_iterator_depth_first::push(const state* s, int sn) { twa_succ_iterator* si = aut_->succ_iter(s); process_state(s, sn, si); @@ -175,7 +175,7 @@ namespace spot } void - tgba_reachable_iterator_depth_first::pop() + twa_reachable_iterator_depth_first::pop() { aut_->release_iter(todo.back().it); todo.pop_back(); @@ -184,7 +184,7 @@ namespace spot } void - tgba_reachable_iterator_depth_first::run() + twa_reachable_iterator_depth_first::run() { int n = 1; start(); @@ -240,60 +240,60 @@ namespace spot } bool - tgba_reachable_iterator_depth_first::want_state(const state*) const + twa_reachable_iterator_depth_first::want_state(const state*) const { return true; } void - tgba_reachable_iterator_depth_first::start() + twa_reachable_iterator_depth_first::start() { } void - tgba_reachable_iterator_depth_first::end() + twa_reachable_iterator_depth_first::end() { } void - tgba_reachable_iterator_depth_first::process_state(const state*, int, + twa_reachable_iterator_depth_first::process_state(const state*, int, twa_succ_iterator*) { } void - tgba_reachable_iterator_depth_first::process_link(const state*, int, + twa_reachable_iterator_depth_first::process_link(const state*, int, const state*, int, const twa_succ_iterator*) { } - // tgba_reachable_iterator_depth_first_stack + // twa_reachable_iterator_depth_first_stack ////////////////////////////////////////////////////////////////////// - tgba_reachable_iterator_depth_first_stack:: - tgba_reachable_iterator_depth_first_stack(const const_twa_ptr& a) - : tgba_reachable_iterator_depth_first(a) + twa_reachable_iterator_depth_first_stack:: + twa_reachable_iterator_depth_first_stack(const const_twa_ptr& a) + : twa_reachable_iterator_depth_first(a) { } void - tgba_reachable_iterator_depth_first_stack::push(const state* s, int sn) + twa_reachable_iterator_depth_first_stack::push(const state* s, int sn) { stack_.insert(sn); - this->tgba_reachable_iterator_depth_first::push(s, sn); + this->twa_reachable_iterator_depth_first::push(s, sn); } void - tgba_reachable_iterator_depth_first_stack::pop() + twa_reachable_iterator_depth_first_stack::pop() { stack_.erase(todo.back().src_n); - this->tgba_reachable_iterator_depth_first::pop(); + this->twa_reachable_iterator_depth_first::pop(); } bool - tgba_reachable_iterator_depth_first_stack::on_stack(int sn) const + twa_reachable_iterator_depth_first_stack::on_stack(int sn) const { return stack_.find(sn) != stack_.end(); } diff --git a/spot/twaalgos/reachiter.hh b/spot/twaalgos/reachiter.hh index e0ea4d374..0d1fe0778 100644 --- a/spot/twaalgos/reachiter.hh +++ b/spot/twaalgos/reachiter.hh @@ -31,11 +31,11 @@ namespace spot { /// \ingroup twa_generic /// \brief Iterate over all reachable states of a spot::tgba. - class SPOT_API tgba_reachable_iterator + class SPOT_API twa_reachable_iterator { public: - tgba_reachable_iterator(const const_twa_ptr& a); - virtual ~tgba_reachable_iterator(); + twa_reachable_iterator(const const_twa_ptr& a); + virtual ~twa_reachable_iterator(); /// \brief Iterate over all reachable states of a spot::tgba. /// @@ -47,7 +47,7 @@ namespace spot /// \name Todo list management. /// /// See e.g. - /// spot::tgba_reachable_iterator_breadth_first for precanned + /// spot::twa_reachable_iterator_breadth_first for precanned /// implementations for these functions. /// \{ /// \brief Called by run() to register newly discovered states. @@ -81,7 +81,7 @@ namespace spot /// transition. /// /// The in_s and out_s states are owned by the - /// spot::tgba_reachable_iterator instance and destroyed when the + /// spot::twa_reachable_iterator instance and destroyed when the /// instance is destroyed. virtual void process_link(const state* in_s, int in, const state* out_s, int out, @@ -94,13 +94,13 @@ namespace spot }; /// \ingroup twa_generic - /// \brief An implementation of spot::tgba_reachable_iterator that browses + /// \brief An implementation of spot::twa_reachable_iterator that browses /// states breadth first. - class SPOT_API tgba_reachable_iterator_breadth_first : - public tgba_reachable_iterator + class SPOT_API twa_reachable_iterator_breadth_first : + public twa_reachable_iterator { public: - tgba_reachable_iterator_breadth_first(const const_twa_ptr& a); + twa_reachable_iterator_breadth_first(const const_twa_ptr& a); virtual void add_state(const state* s) override; virtual const state* next_state() override; @@ -111,11 +111,11 @@ namespace spot /// \ingroup twa_generic /// \brief Iterate over all states of an automaton using a DFS. - class SPOT_API tgba_reachable_iterator_depth_first + class SPOT_API twa_reachable_iterator_depth_first { public: - tgba_reachable_iterator_depth_first(const const_twa_ptr& a); - virtual ~tgba_reachable_iterator_depth_first(); + twa_reachable_iterator_depth_first(const const_twa_ptr& a); + virtual ~twa_reachable_iterator_depth_first(); /// \brief Iterate over all reachable states of a spot::tgba. /// @@ -149,7 +149,7 @@ namespace spot /// transition. /// /// The in_s and out_s states are owned by the - /// spot::tgba_reachable_iterator instance and destroyed when the + /// spot::twa_reachable_iterator instance and destroyed when the /// instance is destroyed. virtual void process_link(const state* in_s, int in, const state* out_s, int out, @@ -178,11 +178,11 @@ namespace spot /// /// This variant also maintains a set of states that are on the DFS /// stack. It can be checked using the on_stack() method. - class tgba_reachable_iterator_depth_first_stack - : public tgba_reachable_iterator_depth_first + class twa_reachable_iterator_depth_first_stack + : public twa_reachable_iterator_depth_first { public: - tgba_reachable_iterator_depth_first_stack(const const_twa_ptr& a); + twa_reachable_iterator_depth_first_stack(const const_twa_ptr& a); /// \brief Whether state sn is on the DFS stack. /// /// Note the destination state of a transition is only pushed to diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index 2f352f5a9..6d67f0228 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015, 2016 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 // et Marie Curie. @@ -33,23 +33,23 @@ namespace spot { namespace { - class stats_bfs: public tgba_reachable_iterator_breadth_first + class stats_bfs: public twa_reachable_iterator_breadth_first { public: stats_bfs(const const_twa_ptr& a, twa_statistics& s) - : tgba_reachable_iterator_breadth_first(a), s_(s) + : twa_reachable_iterator_breadth_first(a), s_(s) { } void - process_state(const state*, int, twa_succ_iterator*) + process_state(const state*, int, twa_succ_iterator*) override final { ++s_.states; } void process_link(const state*, int, const state*, int, - const twa_succ_iterator*) + const twa_succ_iterator*) override { ++s_.edges; } @@ -58,7 +58,7 @@ namespace spot twa_statistics& s_; }; - class sub_stats_bfs: public stats_bfs + class sub_stats_bfs final: public stats_bfs { public: sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s) @@ -68,7 +68,7 @@ namespace spot void process_link(const state*, int, const state*, int, - const twa_succ_iterator* it) + const twa_succ_iterator* it) override { ++s_.edges;