change storing empty states; limit max size for subsumption

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

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<std::pair<std::shared_ptr<inclusion_mstate>, spot::acc_cond::mark_t>> dfs_acc_stack_; /// this stack could probably be omitted and use SCCs_ instead
 
-        std::vector<std::shared_ptr<inclusion_mstate>> 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<unsigned, std::vector<std::shared_ptr<inclusion_mstate>>> empty_lang_states_;
 
         /// to stop searching when counter-example
         bool decided_ = false;

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