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; };