From bf51f9e74edd46f6434110292b01cdbc1f9e5162 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sun, 22 Dec 2024 23:39:54 +0100 Subject: [PATCH 1/2] fixing warnings I --- src/abstract_complement_alg.hpp | 4 ++-- src/complement_alg_mh.cpp | 9 ++++----- src/complement_alg_ncsb.cpp | 9 +++------ src/complement_alg_ncsb_delay.cpp | 32 ++++++++++++++++++++++++------- src/complement_alg_ncsb_delay.hpp | 21 -------------------- src/complement_alg_safra.cpp | 18 ++++++++--------- src/complement_sync.cpp | 25 ++++++++---------------- src/complement_sync.hpp | 6 +++--- src/decomposer.cpp | 4 ++-- src/decomposer.hpp | 2 +- src/emptiness_check.cpp | 3 ++- src/emptiness_check.hpp | 2 +- src/inclusion_check.cpp | 2 +- 13 files changed, 60 insertions(+), 77 deletions(-) diff --git a/src/abstract_complement_alg.hpp b/src/abstract_complement_alg.hpp index ae02094..5071a4a 100644 --- a/src/abstract_complement_alg.hpp +++ b/src/abstract_complement_alg.hpp @@ -110,9 +110,9 @@ class abstract_complement_alg /// clear breakpoint virtual void clear_breakpoint() { this->set_breakpoint(std::set()); }; - virtual bool subsum_less_early(const mstate& rhs, const std::set& glob_reached) { return this->eq(rhs); }; + virtual bool subsum_less_early(const mstate& rhs) { return this->eq(rhs); }; - virtual bool subsum_less_early_plus(const mstate& rhs, const std::set& glob_reached) { return this->eq(rhs); }; + virtual bool subsum_less_early_plus(const mstate& rhs) { return this->eq(rhs); }; /// virtual destructor (to allow deletion via pointer) virtual ~mstate() { } diff --git a/src/complement_alg_mh.cpp b/src/complement_alg_mh.cpp index d758b96..05f722f 100644 --- a/src/complement_alg_mh.cpp +++ b/src/complement_alg_mh.cpp @@ -40,7 +40,7 @@ class mstate_mh : public abstract_complement_alg::mstate virtual const std::set& get_breakpoint() const override { return this->breakpoint_; } virtual void set_breakpoint(const std::set& breakpoint) override { this->breakpoint_ = get_set_intersection(breakpoint, this->states_); } - virtual bool subsum_less_early(const mstate& rhs, const std::set& glob_reached) override { + virtual bool subsum_less_early(const mstate& rhs) override { auto rhs_mh = dynamic_cast(&rhs); auto S_subs = std::includes(states_.begin(), states_.end(), rhs_mh->states_.begin(), rhs_mh->states_.end()); @@ -49,7 +49,7 @@ class mstate_mh : public abstract_complement_alg::mstate return (S_subs && B_subs); }; - virtual bool subsum_less_early_plus(const mstate& rhs, const std::set& glob_reached) override { + virtual bool subsum_less_early_plus(const mstate& rhs) override { auto rhs_mh = dynamic_cast(&rhs); auto S_subs = std::includes(states_.begin(), states_.end(), rhs_mh->states_.begin(), rhs_mh->states_.end()); @@ -103,7 +103,7 @@ mstate_set complement_mh::get_init() unsigned orig_init = this->info_.aut_->get_init_state_number(); - if (this->info_.st_to_part_map_.at(orig_init) == this->part_index_) { + if (this->info_.st_to_part_map_.at(orig_init) == static_cast(this->part_index_)) { init_state.insert(orig_init); } @@ -124,13 +124,12 @@ mstate_col_set complement_mh::get_succ_track( DEBUG_PRINT_LN("src = " + std::to_string(*src)); DEBUG_PRINT_LN("symbol = " + std::to_string(symbol)); - const mstate_mh* src_mh = dynamic_cast(src); assert(src_mh); assert(!src_mh->active_); std::set states; for (unsigned st : glob_reached) { - if (this->info_.st_to_part_map_.at(st) == this->part_index_) { + if (this->info_.st_to_part_map_.at(st) == static_cast(this->part_index_)) { states.insert(st); } } diff --git a/src/complement_alg_ncsb.cpp b/src/complement_alg_ncsb.cpp index bf78980..9bb7be2 100644 --- a/src/complement_alg_ncsb.cpp +++ b/src/complement_alg_ncsb.cpp @@ -42,7 +42,7 @@ class mstate_ncsb : public abstract_complement_alg::mstate virtual const std::set& get_breakpoint() const override { return this->breakpoint_; } virtual void set_breakpoint(const std::set& breakpoint) override { this->breakpoint_ = get_set_intersection(breakpoint, this->check_); } - virtual bool subsum_less_early(const mstate& rhs, const std::set& glob_reached) override { + virtual bool subsum_less_early(const mstate& rhs) override { auto rhs_ncsb = dynamic_cast(&rhs); std::set S_and_B; @@ -62,7 +62,6 @@ class mstate_ncsb : public abstract_complement_alg::mstate /// a set of states over the given symbol in the SCC the source state is in bool contains_accepting_outgoing_transitions_in_scc( const spot::const_twa_graph_ptr& aut, - const kofola::StateToPartitionMap& st_to_part_map, const spot::scc_info& scc_info, const std::set& states, const bdd& symbol) @@ -129,7 +128,7 @@ mstate_set complement_ncsb::get_init() std::set init_state; unsigned orig_init = this->info_.aut_->get_init_state_number(); - if (this->info_.st_to_part_map_.at(orig_init) == this->part_index_) { + if (this->info_.st_to_part_map_.at(orig_init) == static_cast(this->part_index_)) { init_state.insert(orig_init); } @@ -150,7 +149,6 @@ mstate_col_set complement_ncsb::get_succ_track( // check that safe states do not see accepting transition in the same SCC if (contains_accepting_outgoing_transitions_in_scc( this->info_.aut_, - this->info_.st_to_part_map_, this->info_.scc_info_, src_ncsb->safe_, symbol)) { return {}; @@ -161,7 +159,7 @@ mstate_col_set complement_ncsb::get_succ_track( std::set succ_states; for (unsigned st : glob_reached) { - if (this->info_.st_to_part_map_.at(st) == this->part_index_) { + if (this->info_.st_to_part_map_.at(st) == static_cast(this->part_index_)) { if (succ_safe.find(st) == succ_safe.end()) { // if not in safe succ_states.insert(st); } @@ -252,7 +250,6 @@ mstate_col_set complement_ncsb::get_succ_active( // 3) delta(src_ncsb->breakpoint_, symbol) contains no accepting condition if (contains_accepting_outgoing_transitions_in_scc( this->info_.aut_, - this->info_.st_to_part_map_, this->info_.scc_info_, src_ncsb->breakpoint_, symbol)) { return result; diff --git a/src/complement_alg_ncsb_delay.cpp b/src/complement_alg_ncsb_delay.cpp index d0b6785..a4d62eb 100644 --- a/src/complement_alg_ncsb_delay.cpp +++ b/src/complement_alg_ncsb_delay.cpp @@ -8,6 +8,29 @@ using namespace kofola; using mstate_set = abstract_complement_alg::mstate_set; using mstate_col_set = abstract_complement_alg::mstate_col_set; +namespace { + +/// returns true of there is at least one outgoing accepting transition from +/// a set of states over the given symbol in the SCC the source state is in +bool contains_accepting_outgoing_transitions_in_scc( + const spot::const_twa_graph_ptr& aut, + const spot::scc_info& scc_info, + const std::set& states, + const bdd& symbol) +{ // {{{ + for (unsigned s : states) { + for (const auto &t : aut->out(s)) { + if (scc_info.scc_of(s) == scc_info.scc_of(t.dst) && bdd_implies(symbol, t.cond)) { + if (t.acc) { return true; } + } + } + } + + return false; +} // contains_accepting_outgoing_transitions() }}} + +} + complement_ncsb_delay::complement_ncsb_delay(const cmpl_info& info, unsigned part_index) : complement_ncsb(info, part_index) { } @@ -18,7 +41,7 @@ mstate_set complement_ncsb_delay::get_init() std::set init_state; unsigned orig_init = this->info_.aut_->get_init_state_number(); - if (this->info_.st_to_part_map_.at(orig_init) == this->part_index_) { + if (this->info_.st_to_part_map_.at(orig_init) == static_cast(this->part_index_)) { init_state.insert(orig_init); } @@ -39,7 +62,6 @@ mstate_col_set complement_ncsb_delay::get_succ_track( // check that safe states do not see accepting transition in the same SCC if (contains_accepting_outgoing_transitions_in_scc( this->info_.aut_, - this->info_.st_to_part_map_, this->info_.scc_info_, src_ncsb->safe_, symbol)) { return {}; @@ -50,7 +72,7 @@ mstate_col_set complement_ncsb_delay::get_succ_track( std::set succ_states; for (unsigned st : glob_reached) { - if (this->info_.st_to_part_map_.at(st) == this->part_index_) { + if (this->info_.st_to_part_map_.at(st) == static_cast(this->part_index_)) { if (succ_safe.find(st) == succ_safe.end()) { // if not in safe succ_states.insert(st); } @@ -154,7 +176,6 @@ mstate_col_set complement_ncsb_delay::get_succ_active( // 3) delta(src_ncsb->breakpoint_, symbol) contains no accepting condition if (contains_accepting_outgoing_transitions_in_scc( this->info_.aut_, - this->info_.st_to_part_map_, this->info_.scc_info_, src_ncsb->breakpoint_, symbol)) { active_mstates_.insert(new_state); @@ -195,9 +216,6 @@ bool complement_ncsb_delay::closes_a_cycle(const mstate_ncsb *src, const mstate_ // is there a path from dst to src? std::stack stack; - auto comparator = [](const mstate_ncsb *const &a, - const mstate_ncsb *const &b) - { return a->lt(*b); }; // std::set visited(comparator); std::set visited; diff --git a/src/complement_alg_ncsb_delay.hpp b/src/complement_alg_ncsb_delay.hpp index eaa9536..66896b8 100644 --- a/src/complement_alg_ncsb_delay.hpp +++ b/src/complement_alg_ncsb_delay.hpp @@ -45,27 +45,6 @@ class mstate_ncsb : public abstract_complement_alg::mstate friend class kofola::complement_ncsb_delay; }; // mstate_ncsb }}} - -/// returns true of there is at least one outgoing accepting transition from -/// a set of states over the given symbol in the SCC the source state is in -bool contains_accepting_outgoing_transitions_in_scc( - const spot::const_twa_graph_ptr& aut, - const kofola::StateToPartitionMap& st_to_part_map, - const spot::scc_info& scc_info, - const std::set& states, - const bdd& symbol) -{ // {{{ - for (unsigned s : states) { - for (const auto &t : aut->out(s)) { - if (scc_info.scc_of(s) == scc_info.scc_of(t.dst) && bdd_implies(symbol, t.cond)) { - if (t.acc) { return true; } - } - } - } - - return false; -} // contains_accepting_outgoing_transitions() }}} - } // anonymous namespace }}} std::string mstate_ncsb::to_string() const diff --git a/src/complement_alg_safra.cpp b/src/complement_alg_safra.cpp index d88767a..41b70f9 100644 --- a/src/complement_alg_safra.cpp +++ b/src/complement_alg_safra.cpp @@ -21,6 +21,7 @@ class mstate_safra : public abstract_complement_alg::mstate /// the corresponding Safra tree safra_tree st_; + std::set empty_breakpoint {}; public: // METHODS @@ -34,8 +35,8 @@ class mstate_safra : public abstract_complement_alg::mstate virtual bool lt(const mstate& rhs) const override; virtual ~mstate_safra() override { }; - virtual const std::set& get_breakpoint() const override { return std::set(); } - virtual void set_breakpoint(const std::set& breakpoint) override { } + virtual const std::set& get_breakpoint() const override { return this->empty_breakpoint; } + virtual void set_breakpoint(const std::set& breakpoint) override { (void)breakpoint; } friend class kofola::complement_safra; }; // mstate_safra }}} @@ -69,8 +70,6 @@ bool compare_braces(const std::vector& braces, int a, int b) std::vector b_pattern; a_pattern.reserve(a + 1); b_pattern.reserve(b + 1); - unsigned size_a = 0; - unsigned size_b = 0; while (a != b) { if (a > b) @@ -78,14 +77,12 @@ bool compare_braces(const std::vector& braces, int a, int b) a_pattern.emplace_back(a); // go to the parent a = braces[a]; - size_a ++; } else { b_pattern.emplace_back(b); // go to the parent b = braces[b]; - size_b ++; } } return nesting_cmp(a_pattern, b_pattern); @@ -177,7 +174,7 @@ unsigned determine_color (safra_tree& next) decr_by.assign(next.braces_.size(), 0); unsigned decr = 0; - for (int b = 0; b < next.braces_.size(); ++b) + for (int b = 0; b < static_cast(next.braces_.size()); ++b) { // At first, set it to iself highest_green_ancestor[b] = b; @@ -318,7 +315,7 @@ mstate_set complement_safra::get_init() { // {{{ std::set init_states; unsigned orig_init = this->info_.aut_->get_init_state_number(); - if (this->info_.st_to_part_map_.at(orig_init) == this->part_index_) { + if (this->info_.st_to_part_map_.at(orig_init) == static_cast(this->part_index_)) { init_states.insert(orig_init); } @@ -341,6 +338,7 @@ mstate_col_set complement_safra::get_succ_track( const bdd& /*symbol*/) { // {{{ assert(false); + return {}; } // get_succ_track() }}} @@ -360,11 +358,11 @@ mstate_col_set complement_safra::get_succ_active( const bdd& symbol, bool resample) { // {{{ + (void)resample; const mstate_safra* src_safra = dynamic_cast(src); assert(src_safra); // all states in the scc_index should be on the same order - const int min_new_brace = src_safra->st_.braces_.size(); DEBUG_PRINT_LN("src: " + src_safra->to_string()); DEBUG_PRINT_LN("glob_reached: " + std::to_string(glob_reached)); DEBUG_PRINT_LN("part_index_: " + std::to_string(this->part_index_)); @@ -400,7 +398,7 @@ mstate_col_set complement_safra::get_succ_active( DEBUG_PRINT_LN("this->info_.st_to_part_map_.at(state) = " + std::to_string(this->info_.st_to_part_map_.at(state))); DEBUG_PRINT_LN("succ_part = " + std::to_string(succ_part)); - if (tr.acc || this->info_.st_to_part_map_.at(state) != succ_part) + if (tr.acc || this->info_.st_to_part_map_.at(state) != static_cast(succ_part)) { // accepting edges or leaving the partition (TODO: should be SCC?) // Step A1: Accepting edges generate new braces newb = braces.size(); diff --git a/src/complement_sync.cpp b/src/complement_sync.cpp index 349487a..34f287a 100644 --- a/src/complement_sync.cpp +++ b/src/complement_sync.cpp @@ -121,7 +121,6 @@ namespace cola { // obtain the types of each SCC scc_types_ = get_scc_types(si_); // find out the DACs and NACs - unsigned nonacc_weak = 0; for (unsigned i = 0; i < scc_types_.size(); i++) { if (is_accepting_weakscc(scc_types_, i)) { weaksccs_.push_back(i); @@ -243,7 +242,6 @@ namespace cola { for (unsigned i = 0; i != implications.size(); ++i) { if (!si_.reachable_state(i)) continue; - unsigned scc_of_i = si_.scc_of(i); for (unsigned j = 0; j != implications.size(); ++j) { // reachable states if (!si_.reachable_state(j)) @@ -328,8 +326,8 @@ namespace cola { list_vector[s] = std::vector(list_set[s].begin(), list_set[s].end()); } - for (int s = 0; s < aut_->num_states(); s++) { - std::set tmp({s}); + for (unsigned int s = 0; s < aut_->num_states(); s++) { + std::set tmp({static_cast(s)}); reachable_vector[s] = reachable_vertices(list_vector, tmp); } @@ -1076,7 +1074,7 @@ namespace cola { tnba_complement::uberstate::get_part_macrostates() const { return this->part_macrostates_; } /// returns the index of the active SCC (INACTIVE_SCC if no active) - const int tnba_complement::uberstate::get_active_scc() const { return this->active_scc_; } + int tnba_complement::uberstate::get_active_scc() const { return this->active_scc_; } /// get shared breakpoint const std::set & @@ -1157,11 +1155,6 @@ namespace cola { enum { SINK_COLOUR = 0 }; - // static const unsigned RR_COLOUR = 1; // colour for round robin ### we will choose it dynamically - static const size_t RESERVED_COLOURS = 1; // how many colours are reserved - - /// index of active SCC if no SCC is active - static const int INACTIVE_SCC = -1; /// accessor into the uberstate table unsigned cola::tnba_complement::uberstate_to_num(const cola::tnba_complement::uberstate &us) const { // {{{ @@ -1170,6 +1163,7 @@ namespace cola { return it->second; } else { assert(false); + return 0; } } // uberstate_to_num() }}} @@ -1213,7 +1207,7 @@ namespace cola { } } - for (size_t i = 0; i < std::min(prev + 1, static_cast(alg_vec.size())); ++i) { + for (int i = 0; i < std::min(prev + 1, static_cast(alg_vec.size())); ++i) { if (alg_vec[i]->use_round_robin()) { return i; } @@ -1294,7 +1288,6 @@ namespace cola { " for symbol " + std::to_string(symbol)); using mstate = kofola::abstract_complement_alg::mstate; using mstate_set = kofola::abstract_complement_alg::mstate_set; - using mstate_col = kofola::abstract_complement_alg::mstate_col; using mstate_taggedcol = std::pair, std::set>>; using mstate_col_set = kofola::abstract_complement_alg::mstate_col_set; using mstate_taggedcol_set = std::vector; @@ -1350,7 +1343,7 @@ namespace cola { if (alg_vec_[i]->use_shared_breakpoint()) { mcs = alg_vec_[i]->get_succ_active(all_succ, ms, symbol, sh_break.empty()); - } else if (active_index == i || !alg_vec_[i]->use_round_robin()) { + } else if (active_index == static_cast(i) || !alg_vec_[i]->use_round_robin()) { mcs = alg_vec_[i]->get_succ_active(all_succ, ms, symbol); } else { mcs = alg_vec_[i]->get_succ_track(all_succ, ms, symbol); @@ -1388,12 +1381,11 @@ namespace cola { vec_state_taggedcol result; for (const auto &vec: cp) { vec_macrostates vm; - bool found = false; std::set breakpoint; std::set> cols; assert(alg_vec_.size() == vec.size()); - for (int i = 0; i < vec.size(); i++) { + for (size_t i = 0; i < vec.size(); i++) { if (alg_vec_[i]->use_shared_breakpoint()) { const std::set &vb = vec[i].first->get_breakpoint(); breakpoint.insert(vb.begin(), vb.end()); @@ -1459,7 +1451,7 @@ namespace cola { DEBUG_PRINT_LN("obtained initial state for algs " + std::to_string(i) + ": " + std::to_string(init_mstates)); - if (i == init_active || !alg_vec_[i]->use_round_robin()) { // make the partial macrostate active + if (static_cast(i) == init_active || !alg_vec_[i]->use_round_robin()) { // make the partial macrostate active mstate_set new_mstates; for (const auto &st: init_mstates) { mstate_set lifted = alg_vec_[i]->lift_track_to_active(st.get()); @@ -1831,7 +1823,6 @@ namespace cola { } for (const auto &st_trans_pair: compl_states) { const unsigned &src = st_trans_pair.first; - unsigned spot_state = result->new_state(); assert(spot_state == src); for (const auto &bdd_vec_tgt_pair: st_trans_pair.second) { diff --git a/src/complement_sync.hpp b/src/complement_sync.hpp index fbb7924..1f88de3 100644 --- a/src/complement_sync.hpp +++ b/src/complement_sync.hpp @@ -239,7 +239,7 @@ namespace cola bool subsum_less_early(const uberstate& b) { for(unsigned i = 0; i < part_macrostates_.size(); i++) { - if(!(std::includes(this->reached_states_.begin(), this->reached_states_.end(), b.reached_states_.begin(), b.reached_states_.end()) && this->part_macrostates_[i]->subsum_less_early(*(b.part_macrostates_[i]), reached_states_))) { + if(!(std::includes(this->reached_states_.begin(), this->reached_states_.end(), b.reached_states_.begin(), b.reached_states_.end()) && this->part_macrostates_[i]->subsum_less_early(*(b.part_macrostates_[i])))) { return false; } } @@ -250,7 +250,7 @@ namespace cola bool subsum_less_early_plus(const uberstate& b) { for(unsigned i = 0; i < part_macrostates_.size(); i++) { - if(!(std::includes(this->reached_states_.begin(), this->reached_states_.end(), b.reached_states_.begin(), b.reached_states_.end()) && this->part_macrostates_[i]->subsum_less_early_plus(*(b.part_macrostates_[i]), reached_states_))) { + if(!(std::includes(this->reached_states_.begin(), this->reached_states_.end(), b.reached_states_.begin(), b.reached_states_.end()) && this->part_macrostates_[i]->subsum_less_early_plus(*(b.part_macrostates_[i])))) { return false; } } @@ -275,7 +275,7 @@ namespace cola const vec_macrostates& get_part_macrostates() const; /// returns the index of the active SCC (INACTIVE_SCC if no active) - const int get_active_scc() const; + int get_active_scc() const; /// get shared breakpoint const std::set& get_shared_breakpoint() const; diff --git a/src/decomposer.cpp b/src/decomposer.cpp index 1aa6510..252f391 100644 --- a/src/decomposer.cpp +++ b/src/decomposer.cpp @@ -113,14 +113,14 @@ decomposer::run(bool nonacc_pred, bool merge_iwa, bool merge_det) } if (! remaining_sccs.empty()) { - spot::twa_graph_ptr aut = make_twa_with_scc(si, remaining_sccs, reach_sccs, nonacc_pred, merge_iwa, merge_det); + spot::twa_graph_ptr aut = make_twa_with_scc(si, remaining_sccs, reach_sccs, nonacc_pred); result.push_back(aut); } return result; } spot::twa_graph_ptr -decomposer::make_twa_with_scc(spot::scc_info& si, std::set sccs, std::vector& reach_sccs, bool nonacc_pred, bool merge_iwa, bool merge_det) +decomposer::make_twa_with_scc(spot::scc_info& si, std::set sccs, std::vector& reach_sccs, bool nonacc_pred) { assert(! sccs.empty()); diff --git a/src/decomposer.hpp b/src/decomposer.hpp index f6b33e8..d1dc60c 100644 --- a/src/decomposer.hpp +++ b/src/decomposer.hpp @@ -32,7 +32,7 @@ namespace cola int num_nbas_; spot::twa_graph_ptr - make_twa_with_scc(spot::scc_info& si, std::set sccs, std::vector& reach_sccs, bool nonacc_pred = false, bool merge_iwa = false, bool merge_det = false); + make_twa_with_scc(spot::scc_info& si, std::set sccs, std::vector& reach_sccs, bool nonacc_pred = false); public: decomposer(spot::twa_graph_ptr &nba) diff --git a/src/emptiness_check.cpp b/src/emptiness_check.cpp index f9dd0e5..4540bd4 100644 --- a/src/emptiness_check.cpp +++ b/src/emptiness_check.cpp @@ -60,8 +60,9 @@ namespace kofola { bool emptiness_check::check_simul_less(const std::shared_ptr &dst_mstate) { auto cond = dst_mstate->get_acc(); + spot::acc_cond::mark_t zero{0}; // traversing 'stack' in reversed order, while according to theorem in thesis, the cond has to be 0 - for (auto it = dfs_acc_stack_.rbegin(); it != dfs_acc_stack_.rend() && cond == 0; ++it) { + for (auto it = dfs_acc_stack_.rbegin(); it != dfs_acc_stack_.rend() && cond == zero; ++it) { const auto &s = (*it).first; if (incl_checker_->subsum_less_early(dst_mstate, s)) { for (auto it2 = dfs_acc_stack_.rbegin(); it2 != dfs_acc_stack_.rend() && (*it2).first != s; ++it2) { diff --git a/src/emptiness_check.hpp b/src/emptiness_check.hpp index c304836..bb13a2e 100644 --- a/src/emptiness_check.hpp +++ b/src/emptiness_check.hpp @@ -65,7 +65,7 @@ namespace kofola private: inclusion_check *incl_checker_; /// instance of abstract_successor that provides states and transitions - unsigned cnt_ = 0; /// number of states, for benchmarks + // unsigned cnt_ = 0; /// number of states, for benchmarks const int UNDEFINED = -1; diff --git a/src/inclusion_check.cpp b/src/inclusion_check.cpp index 698359d..efa083c 100644 --- a/src/inclusion_check.cpp +++ b/src/inclusion_check.cpp @@ -175,7 +175,7 @@ namespace kofola { for(unsigned i = offset_; i < orig_to_new.size() - 1; i++) { for(unsigned j = 0; j < offset_; j++) { //if state of A merged to state of B => simulated, not considering transition prunning (-1 in condition) - if(orig_to_new[i] == orig_to_new[j] && orig_to_new[i] < offset_ && orig_to_new[i] != -1) { + if(orig_to_new[i] == orig_to_new[j] && orig_to_new[i] < offset_ && static_cast(orig_to_new[i]) != -1) { dir_simul_[i - offset_].emplace_back(j); } } From 53920f3f83efebfcf0708fef41efbbc79fad286c Mon Sep 17 00:00:00 2001 From: vhavlena Date: Mon, 23 Dec 2024 22:56:55 +0100 Subject: [PATCH 2/2] fixing warnings II --- src/complement_alg_init_det.cpp | 6 ++++-- src/complement_alg_rank2.cpp | 18 ++++++++++++------ src/complement_alg_subs_tuple.cpp | 26 ++++++++------------------ src/util.cpp | 1 + 4 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/complement_alg_init_det.cpp b/src/complement_alg_init_det.cpp index 2715aa5..256d493 100644 --- a/src/complement_alg_init_det.cpp +++ b/src/complement_alg_init_det.cpp @@ -85,7 +85,7 @@ mstate_set complement_init_det::get_init() std::set init_state; unsigned orig_init = this->info_.aut_->get_init_state_number(); - if (this->info_.st_to_part_map_.at(orig_init) == this->part_index_) { + if (this->info_.st_to_part_map_.at(orig_init) == static_cast(this->part_index_)) { init_state.insert(orig_init); } @@ -109,10 +109,11 @@ mstate_col_set complement_init_det::get_succ_track( const mstate_init_det* src_mh = dynamic_cast(src); assert(src_mh); assert(!src_mh->active_); + (void)src_mh; // make release happy std::set states; for (unsigned st : glob_reached) { - if (this->info_.st_to_part_map_.at(st) == this->part_index_) { + if (this->info_.st_to_part_map_.at(st) == static_cast(this->part_index_)) { states.insert(st); } } @@ -137,6 +138,7 @@ mstate_col_set complement_init_det::get_succ_active( const bdd& symbol, bool resample) { + (void)resample; // make release happy const mstate_init_det* src_mh = dynamic_cast(src); assert(src_mh); assert(src_mh->active_); diff --git a/src/complement_alg_rank2.cpp b/src/complement_alg_rank2.cpp index e0a34f7..839135b 100644 --- a/src/complement_alg_rank2.cpp +++ b/src/complement_alg_rank2.cpp @@ -287,7 +287,7 @@ mstate_set complement_rank2::impl::get_init() std::set init_state; unsigned orig_init = this->info_.aut_->get_init_state_number(); - if (this->info_.st_to_part_map_.at(orig_init) == this->part_index_) { + if (this->info_.st_to_part_map_.at(orig_init) == static_cast(this->part_index_)) { init_state.insert(orig_init); } else { // TODO: we assert that the partition block is reachable from initial // FIXME: the box should not be necessary in cases such as a NAC reachable @@ -311,6 +311,10 @@ std::optional complement_rank2::impl::maxrank( // TODO: use bounds! + (void)glob_reached; + (void)f; + (void)symbol; + assert(false); return std::nullopt; @@ -339,6 +343,7 @@ mstate_col_set complement_rank2::impl::get_succ_track( std::optional g = this->maxrank(glob_reached, src_rank->f_, symbol); assert(false); } + return result; } // get_succ_track() }}} @@ -349,7 +354,7 @@ std::set complement_rank2::impl::restr_states_to_part( { // {{{ std::set res; for (unsigned st : states) { - if (this->info_.st_to_part_map_.at(st) == this->part_index_) { + if (this->info_.st_to_part_map_.at(st) == static_cast(this->part_index_)) { res.insert(st); } } @@ -370,15 +375,13 @@ ranking complement_rank2::impl::get_rank_bounds(const std::set& states DEBUG_PRINT_LN("FIXME: get tighter bounds!"); if (kofola::is_in(BOX, states)) { - auto it_bool_pair = bounds.emplace(BOX, max_rank); - assert(it_bool_pair.second); + bounds.emplace(BOX, max_rank); max_rank -= 2; } for (unsigned st : states) { if (BOX != st) { - auto it_bool_pair = bounds.emplace(st, max_rank); - assert(it_bool_pair.second); + bounds.emplace(st, max_rank); } } @@ -392,6 +395,7 @@ std::vector complement_rank2::impl::get_max_tight_rankings_with_rank( const ranking& bounds) { // {{{ assert(rank % 2 == 1); // rank should be odd + (void)bounds; // here, CORE will be the states that keep the tight ranking of a run, cf. // our CONCUR'21 paper; RANKED CORE are states of a CORE with assigned ranks @@ -560,6 +564,7 @@ mstate_col_set complement_rank2::impl::get_succ_active( const bdd& symbol, bool resample) { // {{{ + (void)resample; const mstate_rank* src_rank = dynamic_cast(src); assert(src_rank); assert(src_rank->active_); @@ -577,6 +582,7 @@ mstate_col_set complement_rank2::impl::get_succ_active( mstate_col_set track_succ = this->get_succ_track(glob_reached, tmp_track.get(), symbol); assert(false); + return {}; } // get_succ_active() }}} diff --git a/src/complement_alg_subs_tuple.cpp b/src/complement_alg_subs_tuple.cpp index e438340..5c26f95 100644 --- a/src/complement_alg_subs_tuple.cpp +++ b/src/complement_alg_subs_tuple.cpp @@ -15,6 +15,7 @@ namespace { // anonymous namespace {{{ std::deque, int> > greedy_tuple_; bool active_; // true = active ; false = track bool breakpoint_; + std::set empty_breakpoint {}; public: // METHODS @@ -37,9 +38,10 @@ namespace { // anonymous namespace {{{ virtual ~mstate_subs_tuple() override {} - virtual const std::set &get_breakpoint() const override { /*return this->breakpoint_*/; } + virtual const std::set &get_breakpoint() const override { return empty_breakpoint; } virtual void set_breakpoint(const std::set &breakpoint) override { + (void)breakpoint; /*this->breakpoint_ = get_set_intersection(breakpoint, this->check_)*/; } @@ -50,7 +52,6 @@ namespace { // anonymous namespace {{{ bool is_acc_transition( const spot::const_twa_graph_ptr& aut, - const kofola::StateToPartitionMap& st_to_part_map, const spot::scc_info& scc_info, unsigned src, unsigned dst, @@ -100,7 +101,7 @@ bool mstate_subs_tuple::is_upper_part() const { std::deque, int> > tuple = greedy_tuple_; - for(const auto component : tuple) { + for(const auto& component : tuple) { int color = component.second; if(color != -1 && color != -2) { return false; @@ -141,7 +142,7 @@ mstate_set complement_subs_tuple::get_init() std::deque, int> > init_state; unsigned orig_init = this->info_.aut_->get_init_state_number(); - if (this->info_.st_to_part_map_.at(orig_init) == this->part_index_) { + if (this->info_.st_to_part_map_.at(orig_init) == static_cast(this->part_index_)) { init_state.emplace_back(std::set{orig_init}, -1); //get_all_successors_in_scc(this->info_.aut_,); //this->info_.aut_->edge_storage() state_is_accepting() @@ -171,7 +172,6 @@ mstate_col_set complement_subs_tuple::upper_succ( std::deque, int> > lower_part; bool breakp = true; int last_color = -10; // no color - bool contains_zero = false; for(auto component = src_subs_tuple->greedy_tuple_.rbegin(); component != src_subs_tuple->greedy_tuple_.rend(); component++) { int color = component->second; @@ -189,7 +189,6 @@ mstate_col_set complement_subs_tuple::upper_succ( if(!visited.count(succ)) { if(is_acc_transition( this->info_.aut_, - this->info_.st_to_part_map_, this->info_.scc_info_, state, succ, symbol)) { acc_states.insert(succ); @@ -223,8 +222,6 @@ mstate_col_set complement_subs_tuple::upper_succ( lower_part.emplace_front(non_acc_states, -3); else lower_part.emplace_front(non_acc_states, 0); - - contains_zero = true; } } // fix: only states from our SCC can be there, now takes all @@ -234,7 +231,7 @@ mstate_col_set complement_subs_tuple::upper_succ( auto it = new_runs.begin(); while (it != new_runs.end()) { - if (this->info_.st_to_part_map_.at(*it) != this->part_index_) { + if (this->info_.st_to_part_map_.at(*it) != static_cast(this->part_index_)) { it = new_runs.erase(it); } else { ++it; @@ -245,7 +242,6 @@ mstate_col_set complement_subs_tuple::upper_succ( if(last_color != -1) { // also when there is -10 -> nothing new, so also in this case succ_tuple.emplace_front(new_runs, -1); lower_part.emplace_front(new_runs, 0); - contains_zero = true; } else{ succ_tuple[0].first.insert(new_runs.begin(), new_runs.end()); // union of the first set and the incoming runs @@ -295,7 +291,6 @@ mstate_col_set complement_subs_tuple::lower_succ( std::deque, int> > succ_tuple; int last_color = -10; // no color bool breakp = true; - bool contains_zero = false; bool discont_2 = false; bool found_right = false; @@ -315,7 +310,6 @@ mstate_col_set complement_subs_tuple::lower_succ( if(!visited.count(succ)) { if(is_acc_transition( this->info_.aut_, - this->info_.st_to_part_map_, this->info_.scc_info_, state, succ, symbol)) { acc_states.insert(succ); @@ -366,7 +360,6 @@ mstate_col_set complement_subs_tuple::lower_succ( } else { succ_tuple.emplace_front(acc_states, color); // colors 0 and -3 - contains_zero = true; } last_color = succ_tuple[0].second; @@ -401,9 +394,6 @@ mstate_col_set complement_subs_tuple::lower_succ( else succ_tuple.emplace_front(non_acc_states, color); - if(color == 0 || color == -3) - contains_zero = true; - last_color = succ_tuple[0].second; if(last_color == 2) breakp = false; @@ -432,7 +422,7 @@ mstate_col_set complement_subs_tuple::lower_succ( auto it = new_runs.begin(); while (it != new_runs.end()) { - if (this->info_.st_to_part_map_.at(*it) != this->part_index_) { + if (this->info_.st_to_part_map_.at(*it) != static_cast(this->part_index_)) { it = new_runs.erase(it); } else { ++it; @@ -442,7 +432,6 @@ mstate_col_set complement_subs_tuple::lower_succ( if(!new_runs.empty()) { if(last_color == -3 || last_color == -10 || last_color == 1 || last_color == 2 || last_color == 11) { // also when there is -10 -> nothing new, so also in this case succ_tuple.emplace_front(new_runs, 0); - contains_zero = true; } else{ succ_tuple[0].first.insert(new_runs.begin(), new_runs.end()); // union of the first set and the incoming runs @@ -548,6 +537,7 @@ mstate_col_set complement_subs_tuple::get_succ_active( const bdd& symbol, bool resample) { + (void)resample; const mstate_subs_tuple* src_subs_tuple = dynamic_cast(src); assert(src_subs_tuple); assert(src_subs_tuple->active_); diff --git a/src/util.cpp b/src/util.cpp index d2c45ba..5145e6b 100644 --- a/src/util.cpp +++ b/src/util.cpp @@ -26,6 +26,7 @@ bool all_out_trans_in_scc_acc( unsigned scc, const spot::scc_info& si) { // {{{ + (void)scc; auto current_scc = si.scc_of(current_state); for (auto &t : aut->out(current_state)) {