Merge pull request #8 from VeriFIT/early-opt

src/complement_alg_mh.cpp

@@ -44,9 +44,12 @@ class mstate_mh : public abstract_complement_alg::mstate
       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());
-      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 {

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<const mstate_ncsb*>(&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<unsigned> 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;

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

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)
@@ -273,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.cpp

@@ -249,20 +249,14 @@ namespace kofola {
         std::cout << std::endl << "==================" << std::endl; 
     }
 
-    bool inclusion_check::subsum_less_early(const std::shared_ptr<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b) {
-        auto casted_a = a;
-        auto casted_b = b;
-
+    bool inclusion_check::subsum_less_early(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& 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<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b) {
-        auto casted_a = a;
-        auto casted_b = b;
-
+    bool inclusion_check::subsum_less_early_plus(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& 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) {

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;
     };
 
@@ -128,10 +130,10 @@ namespace kofola {
         std::vector<std::shared_ptr<inclusion_mstate>> get_succs(const std::shared_ptr<inclusion_mstate> &src);
 
         /// returns true if a is early simul. less than b
-        bool subsum_less_early(const std::shared_ptr<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b);
+        bool subsum_less_early(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& b);
 
         /// returns true if a is early+1 simul. less than b
-        bool subsum_less_early_plus(const std::shared_ptr<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b);
+        bool subsum_less_early_plus(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& 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);