From a18580b06ac0efcffeb4b0e5c525495595b32266 Mon Sep 17 00:00:00 2001 From: Lukas Holik Date: Sat, 7 Oct 2023 13:22:35 +0200 Subject: [PATCH 1/6] bullshit zmeny --- src/nfa/inclusion.cc | 80 +++++++++++++++++++++++++++++++------------- 1 file changed, 56 insertions(+), 24 deletions(-) diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index 07e602103..f4bf9672e 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -44,17 +44,21 @@ bool mata::nfa::algorithms::is_included_naive( /// language inclusion check using Antichains // TODO, what about to construct the separator from this? bool mata::nfa::algorithms::is_included_antichains( - const Nfa& smaller, - const Nfa& bigger, + const Nfa& smaller_nfa, + const Nfa& bigger_nfa, const Alphabet* const alphabet, //TODO: this parameter is not used Run* cex) { // {{{ //TODO: what does this do? (void)alphabet; + long new_subsumed = 0; + long old_subsumed = 0; + long generated = 0; + using ProdStateType = std::pair; using WorklistType = std::deque; - // ProcessedType is indexed by states of the smaller nfa + // ProcessedType is indexed by states of the smaller_nfa nfa // tailored for pure antichain approach ... the simulation-based antichain will not work (without changes). using ProcessedType = std::vector>; @@ -65,7 +69,7 @@ bool mata::nfa::algorithms::is_included_antichains( const StateSet& lhs_bigger = lhs.second; const StateSet& rhs_bigger = rhs.second; - if (lhs_bigger.size() > rhs_bigger.size()) { // bigger set cannot be subset + if (lhs_bigger.size() > rhs_bigger.size()) { // bigger_nfa set cannot be subset return false; } @@ -74,25 +78,34 @@ bool mata::nfa::algorithms::is_included_antichains( return lhs_bigger.IsSubsetOf(rhs_bigger); }; + // initialize WorklistType worklist = { }; - ProcessedType processed(smaller.num_of_states()); // allocate to the number of states of the smaller nfa + ProcessedType processed(smaller_nfa.num_of_states()); // allocate to the number of states of the smaller_nfa nfa + + auto smaller_set = [](const ProdStateType & a, const ProdStateType & b) { return a.second.size() < b.second.size(); }; + + auto insert_to_pairs = [&](std::deque & pairs,const ProdStateType & pair) { + auto it = std::lower_bound(pairs.begin(), pairs.end(), pair, smaller_set); + pairs.insert(it,pair); + }; // 'paths[s] == t' denotes that state 's' was accessed from state 't', // 'paths[s] == s' means that 's' is an initial state std::map> paths; // check initial states first // TODO: this would be done in the main loop as the first thing anyway? - for (const auto& state : smaller.initial) { - if (smaller.final[state] && - are_disjoint(bigger.initial, bigger.final)) + for (const auto& state : smaller_nfa.initial) { + if (smaller_nfa.final[state] && + are_disjoint(bigger_nfa.initial, bigger_nfa.final)) { if (cex != nullptr) { cex->word.clear(); } return false; } - const ProdStateType st = std::make_pair(state, StateSet(bigger.initial)); - worklist.push_back(st); + const ProdStateType st = std::make_pair(state, StateSet(bigger_nfa.initial)); + //worklist.push_back(st); + insert_to_pairs(worklist,st); processed[state].push_back(st); if (cex != nullptr) @@ -113,11 +126,11 @@ bool mata::nfa::algorithms::is_included_antichains( sync_iterator.reset(); for (State q: bigger_set) { - mata::utils::push_back(sync_iterator, bigger.delta[q]); + mata::utils::push_back(sync_iterator, bigger_nfa.delta[q]); } // process transitions leaving smaller_state - for (const auto& smaller_move : smaller.delta[smaller_state]) { + for (const auto& smaller_move : smaller_nfa.delta[smaller_state]) { const Symbol& smaller_symbol = smaller_move.symbol; StateSet bigger_succ = {}; @@ -128,8 +141,8 @@ bool mata::nfa::algorithms::is_included_antichains( for (const State& smaller_succ : smaller_move.targets) { const ProdStateType succ = {smaller_succ, bigger_succ}; - if (smaller.final[smaller_succ] && - !bigger.final.intersects_with(bigger_succ)) + if (smaller_nfa.final[smaller_succ] && + !bigger_nfa.final.intersects_with(bigger_succ)) { if (cex != nullptr) { cex->word.clear(); @@ -149,29 +162,45 @@ bool mata::nfa::algorithms::is_included_antichains( bool is_subsumed = false; for (const auto& anti_state : processed[smaller_succ]) - { // trying to find a smaller state in processed + { // trying to find a smaller_nfa state in processed if (subsumes(anti_state, succ)) { is_subsumed = true; break; } } - if (is_subsumed) { continue; } + if (is_subsumed) { + new_subsumed++; + continue; + } for (std::deque* ds : {&processed[smaller_succ], &worklist}) { - for (size_t it = 0; it < ds->size(); ++it) { - if (subsumes(succ, ds->at(it))) { + //for (size_t it = 0; it < ds->size(); ++it) { + // if (subsumes(succ, ds->at(it))) { + // old_subsumed++; + // //Removal though replacement by the last element and removal pob_back. + // //Because calling erase would invalidate iterator it (in deque). + // ds->at(it) = ds->back(); //does it coppy stuff? + // ds->pop_back(); + // } //else { + // //++it; + // //} + //} + for (auto it = 0;itsize();++it) { + if (subsumes(succ, (*ds)[it])) { + old_subsumed++; //Removal though replacement by the last element and removal pob_back. //Because calling erase would invalidate iterator it (in deque). - ds->at(it) = ds->back(); //does it coppy stuff? - ds->pop_back(); - } else { - ++it; + //(*ds)[it] = ds->back(); //does it coppy stuff? + //ds->pop_back(); + ds->erase(ds->begin() + it); } } // TODO: set pushing strategy - ds->push_back(succ); + generated++; + //ds->push_back(succ); + insert_to_pairs(*ds,succ); } if(cex != nullptr) { @@ -181,7 +210,10 @@ bool mata::nfa::algorithms::is_included_antichains( } } } - + std::cout<<"new_subsumed: "< Date: Sat, 7 Oct 2023 14:31:19 +0200 Subject: [PATCH 2/6] Some polishing. --- src/nfa/inclusion.cc | 73 ++++++++++++++++++++------------------------ 1 file changed, 33 insertions(+), 40 deletions(-) diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index f4bf9672e..caedd14b7 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -44,8 +44,8 @@ bool mata::nfa::algorithms::is_included_naive( /// language inclusion check using Antichains // TODO, what about to construct the separator from this? bool mata::nfa::algorithms::is_included_antichains( - const Nfa& smaller_nfa, - const Nfa& bigger_nfa, + const Nfa& smaller, + const Nfa& bigger, const Alphabet* const alphabet, //TODO: this parameter is not used Run* cex) { // {{{ @@ -57,10 +57,10 @@ bool mata::nfa::algorithms::is_included_antichains( long generated = 0; using ProdStateType = std::pair; - using WorklistType = std::deque; - // ProcessedType is indexed by states of the smaller_nfa nfa + using ProdStatesType = std::deque; + // ProcessedType is indexed by states of the smaller nfa // tailored for pure antichain approach ... the simulation-based antichain will not work (without changes). - using ProcessedType = std::vector>; + using ProcessedType = std::vector; auto subsumes = [](const ProdStateType& lhs, const ProdStateType& rhs) { if (lhs.first != rhs.first) { @@ -69,9 +69,6 @@ bool mata::nfa::algorithms::is_included_antichains( const StateSet& lhs_bigger = lhs.second; const StateSet& rhs_bigger = rhs.second; - if (lhs_bigger.size() > rhs_bigger.size()) { // bigger_nfa set cannot be subset - return false; - } //TODO: Can this be done faster using more heuristics? E.g., compare the last elements first ... //TODO: Try BDDs! What about some abstractions? @@ -80,12 +77,16 @@ bool mata::nfa::algorithms::is_included_antichains( // initialize - WorklistType worklist = { }; - ProcessedType processed(smaller_nfa.num_of_states()); // allocate to the number of states of the smaller_nfa nfa + ProdStatesType worklist = { };//Pairs (q,S) to be processed. It sometimes gives a huge speed-up when they are kept sorted by the size of S, + // so those with smaller popped for processing first. + ProcessedType processed(smaller.num_of_states()); // Allocate to the number of states of the smaller nfa. + // The pairs of each state are also kept sorted. It allows slightly faster antichain pruning - no need to test inclusion in sets that have less elements. + //Is |S| < |S'| for the inut pairs (q,S) and (q',S')? auto smaller_set = [](const ProdStateType & a, const ProdStateType & b) { return a.second.size() < b.second.size(); }; - auto insert_to_pairs = [&](std::deque & pairs,const ProdStateType & pair) { + //Inserting the pairs (q,S) into a sequence of pairs in order defined by the size of the sets S. + auto insert_to_pairs = [&](ProdStatesType & pairs,const ProdStateType & pair) { auto it = std::lower_bound(pairs.begin(), pairs.end(), pair, smaller_set); pairs.insert(it,pair); }; @@ -95,18 +96,17 @@ bool mata::nfa::algorithms::is_included_antichains( std::map> paths; // check initial states first // TODO: this would be done in the main loop as the first thing anyway? - for (const auto& state : smaller_nfa.initial) { - if (smaller_nfa.final[state] && - are_disjoint(bigger_nfa.initial, bigger_nfa.final)) + for (const auto& state : smaller.initial) { + if (smaller.final[state] && + are_disjoint(bigger.initial, bigger.final)) { if (cex != nullptr) { cex->word.clear(); } return false; } - const ProdStateType st = std::make_pair(state, StateSet(bigger_nfa.initial)); - //worklist.push_back(st); + const ProdStateType st = std::make_pair(state, StateSet(bigger.initial)); insert_to_pairs(worklist,st); - processed[state].push_back(st); + insert_to_pairs(processed[state],st); if (cex != nullptr) paths.insert({ st, {st, 0}}); @@ -126,11 +126,11 @@ bool mata::nfa::algorithms::is_included_antichains( sync_iterator.reset(); for (State q: bigger_set) { - mata::utils::push_back(sync_iterator, bigger_nfa.delta[q]); + mata::utils::push_back(sync_iterator, bigger.delta[q]); } // process transitions leaving smaller_state - for (const auto& smaller_move : smaller_nfa.delta[smaller_state]) { + for (const auto& smaller_move : smaller.delta[smaller_state]) { const Symbol& smaller_symbol = smaller_move.symbol; StateSet bigger_succ = {}; @@ -141,8 +141,8 @@ bool mata::nfa::algorithms::is_included_antichains( for (const State& smaller_succ : smaller_move.targets) { const ProdStateType succ = {smaller_succ, bigger_succ}; - if (smaller_nfa.final[smaller_succ] && - !bigger_nfa.final.intersects_with(bigger_succ)) + if (smaller.final[smaller_succ] && + !bigger.final.intersects_with(bigger_succ)) { if (cex != nullptr) { cex->word.clear(); @@ -162,7 +162,10 @@ bool mata::nfa::algorithms::is_included_antichains( bool is_subsumed = false; for (const auto& anti_state : processed[smaller_succ]) - { // trying to find a smaller_nfa state in processed + { // trying to find in processed a smaller state that the newly created succ + if (smaller_set(succ,anti_state)) { + break; + } if (subsumes(anti_state, succ)) { is_subsumed = true; break; @@ -174,32 +177,22 @@ bool mata::nfa::algorithms::is_included_antichains( continue; } - for (std::deque* ds : {&processed[smaller_succ], &worklist}) { - //for (size_t it = 0; it < ds->size(); ++it) { - // if (subsumes(succ, ds->at(it))) { - // old_subsumed++; - // //Removal though replacement by the last element and removal pob_back. - // //Because calling erase would invalidate iterator it (in deque). - // ds->at(it) = ds->back(); //does it coppy stuff? - // ds->pop_back(); - // } //else { - // //++it; - // //} - //} - for (auto it = 0;itsize();++it) { + for (ProdStatesType* ds : {&processed[smaller_succ], &worklist}) { + //Pruning of processed and the worklist. + //Since they are ordered by the size of the sets, we can iterate from back, + //and as soon as we get to sets larger than succ, we can stop (larger sets cannot be subsets). + for (long it = ds->size()-1;it>=0;--it) { + if (smaller_set((*ds)[it],succ)) + break; if (subsumes(succ, (*ds)[it])) { old_subsumed++; - //Removal though replacement by the last element and removal pob_back. - //Because calling erase would invalidate iterator it (in deque). - //(*ds)[it] = ds->back(); //does it coppy stuff? - //ds->pop_back(); + //Using index it instead of an iterator since erase could invalidate it (?) ds->erase(ds->begin() + it); } } // TODO: set pushing strategy generated++; - //ds->push_back(succ); insert_to_pairs(*ds,succ); } From 491aad7452554c72049b213f9cbc64575eb667b2 Mon Sep 17 00:00:00 2001 From: Lukas Holik Date: Sat, 7 Oct 2023 14:32:25 +0200 Subject: [PATCH 3/6] Some polishing. --- src/nfa/inclusion.cc | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index caedd14b7..dd69f68bd 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -52,10 +52,6 @@ bool mata::nfa::algorithms::is_included_antichains( //TODO: what does this do? (void)alphabet; - long new_subsumed = 0; - long old_subsumed = 0; - long generated = 0; - using ProdStateType = std::pair; using ProdStatesType = std::deque; // ProcessedType is indexed by states of the smaller nfa @@ -173,7 +169,6 @@ bool mata::nfa::algorithms::is_included_antichains( } if (is_subsumed) { - new_subsumed++; continue; } @@ -185,14 +180,12 @@ bool mata::nfa::algorithms::is_included_antichains( if (smaller_set((*ds)[it],succ)) break; if (subsumes(succ, (*ds)[it])) { - old_subsumed++; //Using index it instead of an iterator since erase could invalidate it (?) ds->erase(ds->begin() + it); } } // TODO: set pushing strategy - generated++; insert_to_pairs(*ds,succ); } @@ -203,10 +196,6 @@ bool mata::nfa::algorithms::is_included_antichains( } } } - std::cout<<"new_subsumed: "< Date: Sat, 7 Oct 2023 14:39:05 +0200 Subject: [PATCH 4/6] Remove some static cast warnings. --- src/nfa/inclusion.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index dd69f68bd..c858dea84 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -176,10 +176,10 @@ bool mata::nfa::algorithms::is_included_antichains( //Pruning of processed and the worklist. //Since they are ordered by the size of the sets, we can iterate from back, //and as soon as we get to sets larger than succ, we can stop (larger sets cannot be subsets). - for (long it = ds->size()-1;it>=0;--it) { - if (smaller_set((*ds)[it],succ)) + for (long it = static_cast(ds->size()-1);it>=0;--it) { + if (smaller_set((*ds)[static_cast(it)],succ)) break; - if (subsumes(succ, (*ds)[it])) { + if (subsumes(succ, (*ds)[static_cast(it)])) { //Using index it instead of an iterator since erase could invalidate it (?) ds->erase(ds->begin() + it); } From c902043559ad32af24c88283e2e44164e3b4e008 Mon Sep 17 00:00:00 2001 From: Lukas Holik Date: Sat, 7 Oct 2023 14:41:28 +0200 Subject: [PATCH 5/6] Remove outdated comment. --- src/nfa/inclusion.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index c858dea84..76cae3839 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -185,7 +185,6 @@ bool mata::nfa::algorithms::is_included_antichains( } } - // TODO: set pushing strategy insert_to_pairs(*ds,succ); } From ead8c28a75adf601afaa8b07068af42fa3167015 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Sat, 7 Oct 2023 18:40:52 +0200 Subject: [PATCH 6/6] Use vector instead of deque for worklist We insert to the vector using iterators which is not ideal. But it seems to work better than deque. --- src/nfa/inclusion.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index 76cae3839..e001f76db 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -53,7 +53,7 @@ bool mata::nfa::algorithms::is_included_antichains( (void)alphabet; using ProdStateType = std::pair; - using ProdStatesType = std::deque; + using ProdStatesType = std::vector; // ProcessedType is indexed by states of the smaller nfa // tailored for pure antichain approach ... the simulation-based antichain will not work (without changes). using ProcessedType = std::vector;