Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixing warnings #5

Merged
merged 2 commits into from
Dec 31, 2024
Merged

Fixing warnings #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bf51f9e
fixing warnings I
vhavlena Dec 22, 2024
53920f3
fixing warnings II
vhavlena Dec 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/abstract_complement_alg.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,9 +110,9 @@ class abstract_complement_alg
/// clear breakpoint
virtual void clear_breakpoint() { this->set_breakpoint(std::set<unsigned>()); };

virtual bool subsum_less_early(const mstate& rhs, const std::set<unsigned>& 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<unsigned>& 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() { }
Expand Down
6 changes: 4 additions & 2 deletions src/complement_alg_init_det.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ mstate_set complement_init_det::get_init()
std::set<unsigned> 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<int>(this->part_index_)) {
init_state.insert(orig_init);
}

Expand All @@ -109,10 +109,11 @@ mstate_col_set complement_init_det::get_succ_track(
const mstate_init_det* src_mh = dynamic_cast<const mstate_init_det*>(src);
assert(src_mh);
assert(!src_mh->active_);
(void)src_mh; // make release happy

std::set<unsigned> 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<int>(this->part_index_)) {
states.insert(st);
}
}
Expand All @@ -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<const mstate_init_det*>(src);
assert(src_mh);
assert(src_mh->active_);
Expand Down
9 changes: 4 additions & 5 deletions src/complement_alg_mh.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ class mstate_mh : public abstract_complement_alg::mstate
virtual const std::set<unsigned>& get_breakpoint() const override { return this->breakpoint_; }
virtual void set_breakpoint(const std::set<unsigned>& breakpoint) override { this->breakpoint_ = get_set_intersection(breakpoint, this->states_); }

virtual bool subsum_less_early(const mstate& rhs, const std::set<unsigned>& glob_reached) override {
virtual bool subsum_less_early(const mstate& rhs) override {
auto rhs_mh = dynamic_cast<const mstate_mh*>(&rhs);

auto S_subs = std::includes(states_.begin(), states_.end(), rhs_mh->states_.begin(), rhs_mh->states_.end());
Expand All @@ -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<unsigned>& glob_reached) override {
virtual bool subsum_less_early_plus(const mstate& rhs) override {
auto rhs_mh = dynamic_cast<const mstate_mh*>(&rhs);

auto S_subs = std::includes(states_.begin(), states_.end(), rhs_mh->states_.begin(), rhs_mh->states_.end());
Expand Down Expand Up @@ -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<int>(this->part_index_)) {
init_state.insert(orig_init);
}

Expand All @@ -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<const mstate_mh*>(src);
assert(src_mh);
assert(!src_mh->active_);

std::set<unsigned> 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<int>(this->part_index_)) {
states.insert(st);
}
}
Expand Down
9 changes: 3 additions & 6 deletions src/complement_alg_ncsb.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ class mstate_ncsb : public abstract_complement_alg::mstate
virtual const std::set<unsigned>& get_breakpoint() const override { return this->breakpoint_; }
virtual void set_breakpoint(const std::set<unsigned>& breakpoint) override { this->breakpoint_ = get_set_intersection(breakpoint, this->check_); }

virtual bool subsum_less_early(const mstate& rhs, const std::set<unsigned>& glob_reached) override {
virtual bool subsum_less_early(const mstate& rhs) override {
auto rhs_ncsb = dynamic_cast<const mstate_ncsb*>(&rhs);

std::set<unsigned> S_and_B;
Expand All @@ -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<unsigned>& states,
const bdd& symbol)
Expand Down Expand Up @@ -129,7 +128,7 @@ mstate_set complement_ncsb::get_init()
std::set<unsigned> 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<int>(this->part_index_)) {
init_state.insert(orig_init);
}

Expand All @@ -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 {};
Expand All @@ -161,7 +159,7 @@ mstate_col_set complement_ncsb::get_succ_track(

std::set<unsigned> 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<int>(this->part_index_)) {
if (succ_safe.find(st) == succ_safe.end()) { // if not in safe
succ_states.insert(st);
}
Expand Down Expand Up @@ -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;
Expand Down
32 changes: 25 additions & 7 deletions src/complement_alg_ncsb_delay.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<unsigned>& 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)
{ }
Expand All @@ -18,7 +41,7 @@ mstate_set complement_ncsb_delay::get_init()
std::set<unsigned> 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<int>(this->part_index_)) {
init_state.insert(orig_init);
}

Expand All @@ -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 {};
Expand All @@ -50,7 +72,7 @@ mstate_col_set complement_ncsb_delay::get_succ_track(

std::set<unsigned> 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<int>(this->part_index_)) {
if (succ_safe.find(st) == succ_safe.end()) { // if not in safe
succ_states.insert(st);
}
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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<mstate_ncsb> stack;
auto comparator = [](const mstate_ncsb *const &a,
const mstate_ncsb *const &b)
{ return a->lt(*b); };
// std::set<const mstate_ncsb *, decltype(comparator)> visited(comparator);
std::set<mstate_ncsb> visited;

Expand Down
21 changes: 0 additions & 21 deletions src/complement_alg_ncsb_delay.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<unsigned>& 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
Expand Down
18 changes: 12 additions & 6 deletions src/complement_alg_rank2.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -287,7 +287,7 @@ mstate_set complement_rank2::impl::get_init()
std::set<unsigned> 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<int>(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
Expand All @@ -311,6 +311,10 @@ std::optional<ranking> complement_rank2::impl::maxrank(

// TODO: use bounds!

(void)glob_reached;
(void)f;
(void)symbol;

assert(false);

return std::nullopt;
Expand Down Expand Up @@ -339,6 +343,7 @@ mstate_col_set complement_rank2::impl::get_succ_track(
std::optional<ranking> g = this->maxrank(glob_reached, src_rank->f_, symbol);
assert(false);
}
return result;


} // get_succ_track() }}}
Expand All @@ -349,7 +354,7 @@ std::set<unsigned> complement_rank2::impl::restr_states_to_part(
{ // {{{
std::set<unsigned> 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<int>(this->part_index_)) {
res.insert(st);
}
}
Expand All @@ -370,15 +375,13 @@ ranking complement_rank2::impl::get_rank_bounds(const std::set<unsigned>& 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);
}
}

Expand All @@ -392,6 +395,7 @@ std::vector<ranking> 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
Expand Down Expand Up @@ -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<const mstate_rank*>(src);
assert(src_rank);
assert(src_rank->active_);
Expand All @@ -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() }}}


Expand Down
Loading
Loading