Sgra emptiness

src/complement/complement_sync.cpp

@@ -1504,7 +1504,6 @@ namespace helpers {
 
         final_code_ = alg_acc_code;
         DEBUG_PRINT_LN("final code: " + std::to_string(final_code_));
-        // std::cout << std::to_string(final_code_) << "\n";
         return used_infs_;
     }
 }

src/inclusion/emptiness_check.cpp

@@ -47,30 +47,37 @@ namespace kofola {
     }
 
     bool emptiness_check::empty() {
-        auto init_states = incl_checker_->get_initial_states();
-        for (const auto& state: init_states) {
+        entry_states_ = incl_checker_->get_initial_states();
+        for (const auto& state: entry_states_) {
             dfs_num_.insert({state, UNDEFINED});
             on_stack_.insert({state, false});
         }
 
-        for(const auto& init: init_states) {
-            if (dfs_num_.at(init) == UNDEFINED) {
+        // Allow entry_states_ to be enriched by gs()/gs_edited
+        size_t i = 0;
+        auto intersect_aut_acc_cond = incl_checker_->get_acc_cond();
+        auto fin_mark = intersect_aut_acc_cond.fin_unit();
+
+        while (i < entry_states_.size()) {
+            const auto& entry = entry_states_[i];
+            if (dfs_num_.at(entry) == UNDEFINED) {
                 bool empty;
                 if(kofola::OPTIONS.params.count("gfee") != 0 && kofola::OPTIONS.params["gfee"] == "yes")
-                    empty = gs_edited(init);
+                    empty = gs_edited(entry);
                 else
-                    empty = gs(init);
+                    empty = gs(entry, fin_mark);
                 if(!empty){
                     #ifdef ENABLE_COUNTER
-                        std::cout << cnt_ << "\n";
+                        std::cout << "States: " << cnt_ << "\n";
                     #endif
                     return false;
                 }
             }
+            ++i;
         }
 
         #ifdef ENABLE_COUNTER
-            std::cout << cnt_ << "\n";
+            std::cout << "States: " << cnt_ << "\n";
         #endif
         return true;
     }
@@ -99,7 +106,7 @@ namespace kofola {
 
     bool emptiness_check::gs_edited(std::shared_ptr<inclusion_mstate> src_mstate) {
         #ifdef ENABLE_COUNTER
-            cnt_ = 1;
+            cnt_++;
         #endif
 
         // stacks to replace recursion
@@ -221,9 +228,9 @@ namespace kofola {
         on_stack_[src_mstate] = true;
     }
 
-    bool emptiness_check::gs(std::shared_ptr<inclusion_mstate> src_mstate) {
+    bool emptiness_check::gs(std::shared_ptr<inclusion_mstate> src_mstate, spot::acc_cond::mark_t fin_mark) {
         #ifdef ENABLE_COUNTER
-            cnt_ = 1;
+            cnt_++;
         #endif
         // stacks to replace recursion
         std::stack<std::shared_ptr<inclusion_mstate>> src_mstates;
@@ -258,6 +265,11 @@ namespace kofola {
                     on_stack_.insert({dst_mstate, false});
                 }
                 // dfs_num_ initialised for dst_mstate
+                if(fin_mark & dst_mstate->get_acc()) {
+                    entry_states_.push_back(dst_mstate);
+                    continue;
+                }
+
 
                 if (dfs_num_[dst_mstate] == UNDEFINED)
                 {

src/inclusion/emptiness_check.hpp

@@ -42,15 +42,16 @@ namespace kofola
 
         void update_structures(const std::shared_ptr<inclusion_mstate>& src_mstate);
 
+
+        bool gen_rabin(std::shared_ptr<inclusion_mstate> src_mstate, spot::acc_cond::mark_t fin_mark);
+
         /// implements the edited Gaiser and Schwoon algorithm suggested in the thesis
         /// path_cond can be omitted
-        /// TODO too deep of a recursion can cause mem. problems, rewrite to iteration
         bool gs_edited(std::shared_ptr<inclusion_mstate> src_mstate);
 
         /// implements Gaiser and Schwoon algorithm, with the possibility of subsumptions usage
         /// path_cond can be omitted
-        /// TODO too deep of a recursion can cause mem. problems, rewrite to iteration
-        bool gs(std::shared_ptr<inclusion_mstate> src_mstate);
+        bool gs(std::shared_ptr<inclusion_mstate> src_mstate, spot::acc_cond::mark_t fin_mark);
 
         /// decides whether there is a state p on the searchpath such that src_mstate is simul. (early or +1) less than p,
         /// without seeing acc. trans. if yes => true
@@ -83,12 +84,17 @@ namespace kofola
 
         /// GS algorithm variables
         std::map<std::shared_ptr<inclusion_mstate>, signed, shared_ptr_comparator> dfs_num_;
+        std::map<std::shared_ptr<inclusion_mstate>, signed, shared_ptr_comparator> lowlink_;
         std::map<std::shared_ptr<inclusion_mstate>, bool, shared_ptr_comparator> on_stack_;
         signed index_ = 0;
         std::vector<std::shared_ptr<inclusion_mstate>> tarjan_stack_;
         std::stack<std::shared_ptr<inclusion_mstate>> SCCs_;
         /// end of GS algorithm variables
 
+        std::unordered_map<unsigned int, std::vector<unsigned int>> infs_pos_; 
+        std::vector<unsigned int> fin_pos_;
+        std::map<std::shared_ptr<inclusion_mstate>, spot::acc_cond::mark_t, shared_ptr_comparator> prefix_;
+
         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
 
         /// stores states from non-trivial SCCs with empty language. Indexed by the states of the first automaton
@@ -98,6 +104,8 @@ namespace kofola
         bool decided_ = false;
         bool empty_ = true;
 
+        std::vector<std::shared_ptr<inclusion_mstate>> entry_states_; /// states to start the search from
+
         /// to know if early(+1) prunning should be used
         bool early_prune_ = false;
 

src/inclusion/inclusion_check.cpp

@@ -88,12 +88,17 @@ namespace kofola {
             }
         }
 
-        // setting accepting cond to acc of complement & Inf(the first unused color by aut_B_compl)
-        infs_from_compl_ = (aut_B_compl_.set_acc_cond());
-        first_col_to_use_ = infs_from_compl_.size() + 1;
+        // setting accepting cond to acc of complement & Inf (the first unused color by aut_B_compl)
+        aut_B_compl_.set_acc_cond();
         acc_cond_ = aut_B_compl_.get_final_acc_code();
+        spot::acc_cond cond(acc_cond_);
+        auto infs = cond.inf_unit().sets();
+        for(const auto& inf_set : infs) {
+            infs_from_compl_.insert(inf_set);
+        }
+        first_col_to_use_ = cond.all_sets().max_set();
+
         acc_cond_ &= spot::acc_cond::acc_code::inf({first_col_to_use_});
-
         initialized_ = true;
     }
 
@@ -143,7 +148,7 @@ namespace kofola {
         }
 
 
-    kofola::OPTIONS.output_type = "tgba";
+    // kofola::OPTIONS.output_type = "tgba";
     // Build SCC info for the exact automaton we are going to complement.
     // Using a different automaton here (e.g., the un-preprocessed aut_B)
     // leads to mismatched state indices and scc_of() returning (unsigned)-1.
@@ -184,9 +189,10 @@ namespace kofola {
         }
 
         // creating initial state such that it has transitions to both initial states of A and B respectively
+        // FIXME: should not go to init states but to their successors
         new_st = res->new_state();
         res->new_edge(new_st, init_a, bdd_true());
-        res->new_edge(new_st, init_b, bdd_true());
+        res->new_edge(new_st, init_b, bdd_true()); 
         res->set_init_state(new_st);
 
         return res;

src/inclusion/inclusion_check.hpp

@@ -117,6 +117,9 @@ namespace kofola {
         /// decide which states from aut_B simulate states in aut_A
         void compute_simulation(const spot::twa_graph_ptr &aut_A, const spot::const_twa_graph_ptr &aut_B);
 
+        /// get acc cond for the intersection automaton
+        spot::acc_cond::acc_code get_acc_cond() const { return acc_cond_; }
+
         /// for debugging purposes only
         void print_mstate(const std::shared_ptr<inclusion_mstate> a);
 

src/util/helpers.cpp

@@ -318,6 +318,10 @@ namespace helpers
     return (scc_types[scc] & SCC_ACC) > 0 && (scc_types[scc] & SCC_INITIAL_ALMOST_DETERMINISTIC_TYPE) > 0;
   }
 
+  bool is_accepting_almost_initial_detscc(const std::string& scc_types, unsigned scc) {
+    return (scc_types[scc] & SCC_ACC) > 0 && (scc_types[scc] & SCC_ALMOST_INITIAL_DET_TYPE) > 0;
+  }
+
   bool
   is_accepting_weakscc(const std::string& scc_types, unsigned scc)
   {

src/util/helpers.hpp

@@ -32,6 +32,7 @@ static const char SCC_DET_TYPE = 4;
 static const char SCC_ACC = 8;
 static const char SCC_INITIAL_ALMOST_DETERMINISTIC_TYPE = 16;
 static const char SCC_DET_BORDER_NONDET_TYPE = 32;
+static const char SCC_ALMOST_INITIAL_DET_TYPE = 64;
 
 namespace kofola
 { // {{{