From 360db2f76bca82bf009fab6f9f8e362aa83bc277 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 4 Jan 2025 20:46:33 +0100 Subject: [PATCH 1/2] early: optimize subsumption checking --- src/complement_alg_mh.cpp | 7 +++++-- src/complement_alg_ncsb.cpp | 10 +++++++--- src/complement_sync.hpp | 5 ++++- src/emptiness_check.cpp | 3 ++- src/inclusion_check.cpp | 14 ++++---------- src/inclusion_check.hpp | 4 ++-- 6 files changed, 24 insertions(+), 19 deletions(-) diff --git a/src/complement_alg_mh.cpp b/src/complement_alg_mh.cpp index 05f722f..d240e64 100644 --- a/src/complement_alg_mh.cpp +++ b/src/complement_alg_mh.cpp @@ -44,9 +44,12 @@ class mstate_mh : public abstract_complement_alg::mstate auto rhs_mh = dynamic_cast(&rhs); auto S_subs = std::includes(states_.begin(), states_.end(), rhs_mh->states_.begin(), rhs_mh->states_.end()); - auto B_subs = std::includes(breakpoint_.begin(), breakpoint_.end(), rhs_mh->breakpoint_.begin(), rhs_mh->breakpoint_.end()); + if(!S_subs) { + return false; + } - return (S_subs && B_subs); + auto B_subs = std::includes(breakpoint_.begin(), breakpoint_.end(), rhs_mh->breakpoint_.begin(), rhs_mh->breakpoint_.end()); + return B_subs; }; virtual bool subsum_less_early_plus(const mstate& rhs) override { diff --git a/src/complement_alg_ncsb.cpp b/src/complement_alg_ncsb.cpp index 9bb7be2..67b3932 100644 --- a/src/complement_alg_ncsb.cpp +++ b/src/complement_alg_ncsb.cpp @@ -45,13 +45,17 @@ class mstate_ncsb : public abstract_complement_alg::mstate virtual bool subsum_less_early(const mstate& rhs) override { auto rhs_ncsb = dynamic_cast(&rhs); + auto S_subs = std::includes(this->safe_.begin(), this->safe_.end(), rhs_ncsb->safe_.begin(), rhs_ncsb->safe_.end()); + if(!S_subs) { + return false; + } + std::set S_and_B; set_union(safe_.begin(), safe_.end(), breakpoint_.begin() , breakpoint_.end(), std::inserter(S_and_B, S_and_B.begin())); auto B_subs = std::includes(S_and_B.begin(), S_and_B.end(), rhs_ncsb->breakpoint_.begin(), rhs_ncsb->breakpoint_.end()); - auto S_subs = std::includes(this->safe_.begin(), this->safe_.end(), rhs_ncsb->safe_.begin(), rhs_ncsb->safe_.end()); - - return (B_subs && S_subs); + + return B_subs; }; friend class kofola::complement_ncsb; diff --git a/src/complement_sync.hpp b/src/complement_sync.hpp index 1f88de3..bb05e33 100644 --- a/src/complement_sync.hpp +++ b/src/complement_sync.hpp @@ -238,8 +238,11 @@ namespace cola bool subsum_less_early(const uberstate& b) { + if(!std::includes(this->reached_states_.begin(), this->reached_states_.end(), b.reached_states_.begin(), b.reached_states_.end())) { + return false; + } 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])))) { + if(!this->part_macrostates_[i]->subsum_less_early(*(b.part_macrostates_[i]))) { return false; } } diff --git a/src/emptiness_check.cpp b/src/emptiness_check.cpp index 4540bd4..bbad4a6 100644 --- a/src/emptiness_check.cpp +++ b/src/emptiness_check.cpp @@ -218,8 +218,9 @@ namespace kofola { auto dst_mstate = succs.back(); succs.pop_back(); - if(empty_lang(dst_mstate)) + if(empty_lang(dst_mstate)) { continue; + } // init structure if(dfs_num_.count(dst_mstate) == 0) diff --git a/src/inclusion_check.cpp b/src/inclusion_check.cpp index efa083c..46d954f 100644 --- a/src/inclusion_check.cpp +++ b/src/inclusion_check.cpp @@ -249,20 +249,14 @@ namespace kofola { std::cout << std::endl << "==================" << std::endl; } - bool inclusion_check::subsum_less_early(const std::shared_ptr a, const std::shared_ptr b) { - auto casted_a = a; - auto casted_b = b; - + bool inclusion_check::subsum_less_early(const std::shared_ptr& a, const std::shared_ptr& b) { // between states of A only identity - return (casted_a->state_.first == casted_b->state_.first && aut_B_compl_.subsum_less_early(casted_a->state_.second, casted_b->state_.second)); + return (a->state_.first == b->state_.first && aut_B_compl_.subsum_less_early(a->state_.second, b->state_.second)); } - bool inclusion_check::subsum_less_early_plus(const std::shared_ptr a, const std::shared_ptr b) { - auto casted_a = a; - auto casted_b = b; - + bool inclusion_check::subsum_less_early_plus(const std::shared_ptr& a, const std::shared_ptr& b) { // between states of A only identity - return (casted_a->state_.first == casted_b->state_.first && aut_B_compl_.subsum_less_early_plus(casted_a->state_.second, casted_b->state_.second)); + return (a->state_.first == b->state_.first && aut_B_compl_.subsum_less_early_plus(a->state_.second, b->state_.second)); } cola::tnba_complement::vec_state_taggedcol inclusion_check::get_successors_compl(unsigned compl_state, const bdd& letter) { diff --git a/src/inclusion_check.hpp b/src/inclusion_check.hpp index 05500a2..e5c0371 100644 --- a/src/inclusion_check.hpp +++ b/src/inclusion_check.hpp @@ -128,10 +128,10 @@ namespace kofola { std::vector> get_succs(const std::shared_ptr &src); /// returns true if a is early simul. less than b - bool subsum_less_early(const std::shared_ptr a, const std::shared_ptr b); + bool subsum_less_early(const std::shared_ptr& a, const std::shared_ptr& b); /// returns true if a is early+1 simul. less than b - bool subsum_less_early_plus(const std::shared_ptr a, const std::shared_ptr b); + bool subsum_less_early_plus(const std::shared_ptr& a, const std::shared_ptr& b); /// returns true when the provided mark_t satisfies acc_cond_, for the need of emptiness check bool is_accepting(spot::acc_cond::mark_t inf_cond); From e6e21b8ed5f981a8be433a9ec48a2da5503f970c Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 9 Jan 2025 13:13:42 +0100 Subject: [PATCH 2/2] change storing empty states; limit max size for subsumption --- src/emptiness_check.cpp | 17 ++++++++++++----- src/emptiness_check.hpp | 5 ++++- src/inclusion_check.hpp | 2 ++ 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/emptiness_check.cpp b/src/emptiness_check.cpp index bbad4a6..a15b304 100644 --- a/src/emptiness_check.cpp +++ b/src/emptiness_check.cpp @@ -274,22 +274,29 @@ namespace kofola { tmp = tarjan_stack_.back(); tarjan_stack_.pop_back(); dfs_acc_stack_.pop_back(); on_stack_[tmp] = false; - empty_lang_states_.emplace_back(tmp); // when here, each state has empty language, otherwise we would have ended + empty_lang_states_[tmp->get_intersect_state().first].emplace_back(tmp); // when here, each state has empty language, otherwise we would have ended } while (src_mstate != tmp); } bool emptiness_check::empty_lang(const std::shared_ptr & dst_mstate) { if(kofola::OPTIONS.params.count("early_sim") != 0 && kofola::OPTIONS.params["early_sim"] == "yes") { - for (const auto &empty_state: empty_lang_states_) { + const auto& col = empty_lang_states_[dst_mstate->get_intersect_state().first]; + if(col.size() > MAX_SUBSUM_BUCKET) { + return false; + } + for (const auto &empty_state: col) { if (incl_checker_->subsum_less_early(dst_mstate, empty_state)) { return true; } } } - if(kofola::OPTIONS.params.count("early_plus_sim") != 0 && kofola::OPTIONS.params["early_plus_sim"] == "yes") - { - for (const auto &empty_state: empty_lang_states_) { + if(kofola::OPTIONS.params.count("early_plus_sim") != 0 && kofola::OPTIONS.params["early_plus_sim"] == "yes") { + const auto& col = empty_lang_states_[dst_mstate->get_intersect_state().first]; + if(col.size() > MAX_SUBSUM_BUCKET) { + return false; + } + for (const auto &empty_state: col) { if (incl_checker_->subsum_less_early_plus(dst_mstate, empty_state)) { return true; } diff --git a/src/emptiness_check.hpp b/src/emptiness_check.hpp index bb13a2e..8ae0675 100644 --- a/src/emptiness_check.hpp +++ b/src/emptiness_check.hpp @@ -22,6 +22,8 @@ #define INCLUSION 1 #define HYPERLTL_MC_EMPTINESS 2 +#define MAX_SUBSUM_BUCKET 100 + namespace kofola { class inclusion_check; @@ -86,7 +88,8 @@ namespace kofola std::vector, spot::acc_cond::mark_t>> dfs_acc_stack_; /// this stack could probably be omitted and use SCCs_ instead - std::vector> empty_lang_states_; /// stores states from non-trivial SCCs with empty language + /// stores states from non-trivial SCCs with empty language. Indexed by the states of the first automaton + std::map>> empty_lang_states_; /// to stop searching when counter-example bool decided_ = false; diff --git a/src/inclusion_check.hpp b/src/inclusion_check.hpp index e5c0371..1b77886 100644 --- a/src/inclusion_check.hpp +++ b/src/inclusion_check.hpp @@ -53,6 +53,8 @@ namespace kofola { ~inclusion_mstate() {} + const intersect_mstate& get_intersect_state() const { return state_; } + friend class inclusion_check; };