diff --git a/src/complement/complement_sync.cpp b/src/complement/complement_sync.cpp index 8d3f0a9..ab03d1b 100644 --- a/src/complement/complement_sync.cpp +++ b/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_; } } diff --git a/src/inclusion/emptiness_check.cpp b/src/inclusion/emptiness_check.cpp index c056601..661e356 100644 --- a/src/inclusion/emptiness_check.cpp +++ b/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 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 src_mstate) { + bool emptiness_check::gs(std::shared_ptr src_mstate, spot::acc_cond::mark_t fin_mark) { #ifdef ENABLE_COUNTER - cnt_ = 1; + cnt_++; #endif // stacks to replace recursion std::stack> 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) { diff --git a/src/inclusion/emptiness_check.hpp b/src/inclusion/emptiness_check.hpp index 2b98aa6..5384229 100644 --- a/src/inclusion/emptiness_check.hpp +++ b/src/inclusion/emptiness_check.hpp @@ -42,15 +42,16 @@ namespace kofola void update_structures(const std::shared_ptr& src_mstate); + + bool gen_rabin(std::shared_ptr 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 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 src_mstate); + bool gs(std::shared_ptr 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, signed, shared_ptr_comparator> dfs_num_; + std::map, signed, shared_ptr_comparator> lowlink_; std::map, bool, shared_ptr_comparator> on_stack_; signed index_ = 0; std::vector> tarjan_stack_; std::stack> SCCs_; /// end of GS algorithm variables + std::unordered_map> infs_pos_; + std::vector fin_pos_; + std::map, spot::acc_cond::mark_t, shared_ptr_comparator> prefix_; + std::vector, 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> entry_states_; /// states to start the search from + /// to know if early(+1) prunning should be used bool early_prune_ = false; diff --git a/src/inclusion/inclusion_check.cpp b/src/inclusion/inclusion_check.cpp index 8d070ad..a5b9a06 100644 --- a/src/inclusion/inclusion_check.cpp +++ b/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; diff --git a/src/inclusion/inclusion_check.hpp b/src/inclusion/inclusion_check.hpp index ebaca0b..1229a29 100644 --- a/src/inclusion/inclusion_check.hpp +++ b/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 a); diff --git a/src/util/helpers.cpp b/src/util/helpers.cpp index 25b1a70..31c3b89 100644 --- a/src/util/helpers.cpp +++ b/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) { diff --git a/src/util/helpers.hpp b/src/util/helpers.hpp index f2b56d9..3a72056 100644 --- a/src/util/helpers.hpp +++ b/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 { // {{{