diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 21b40669c..63e1dc426 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -206,8 +206,25 @@ public: */ Nfa& trim(StateRenaming* state_renaming = nullptr); + /** + * @brief Returns vector ret where ret[q] is the length of the shortest path from any initial state to q + */ std::vector distances_from_initial() const; + /** + * @brief Returns vector ret where ret[q] is the length of the shortest path from q to any final state + */ + std::vector distances_to_final() const; + + /** + * @brief Get some shortest accepting run from state @p q + * + * Assumes that @p q is a state of this automaton and that there is some accepting run from @p q + * + * @param distances_to_final Vector of the lengths of the shortest runs from states (can be computed using distances_to_final()) + */ + Run get_shortest_accepting_run_from_state(State q, const std::vector& distances_to_final) const; + /** * Remove epsilon transitions from the automaton. */ diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index 0358e0c41..245e8a816 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -21,9 +21,21 @@ bool mata::nfa::algorithms::is_included_naive( } else { bigger_cmpl = complement(bigger, *alphabet); } - Nfa nfa_isect = intersection(smaller, bigger_cmpl); - return nfa_isect.is_lang_empty(cex); + std::unordered_map,State> prod_map; + Nfa nfa_isect = intersection(smaller, bigger_cmpl, Limits::max_symbol, &prod_map); + + bool result = nfa_isect.is_lang_empty(cex); + if (cex != nullptr && !result) { + std::unordered_map nfa_isect_state_to_smaller_state; + for (const auto& prod_map_item : prod_map) { + nfa_isect_state_to_smaller_state[prod_map_item.second] = prod_map_item.first.first; + } + for (State& path_state : cex->path) { + path_state = nfa_isect_state_to_smaller_state[path_state]; + } + } + return result; } // is_included_naive }}} @@ -69,8 +81,8 @@ bool mata::nfa::algorithms::is_included_antichains( //Is |S| < |S'| for the inut pairs (q,S) and (q',S')? // auto smaller_set = [](const ProdStateType & a, const ProdStateType & b) { return std::get<1>(a).size() < std::get<1>(b).size(); }; - std::vector distances_smaller = revert(smaller).distances_from_initial(); - std::vector distances_bigger = revert(bigger).distances_from_initial(); + std::vector distances_smaller = smaller.distances_to_final(); + std::vector distances_bigger = bigger.distances_to_final(); // auto closer_dist = [&](const ProdStateType & a, const ProdStateType & b) { // return distances_smaller[a.first] < distances_smaller[b.first]; @@ -118,7 +130,7 @@ bool mata::nfa::algorithms::is_included_antichains( if (smaller.final[state] && are_disjoint(bigger.initial, bigger.final)) { - if (cex != nullptr) { cex->word.clear(); } + if (cex != nullptr) { cex->word.clear(); cex->path = {state}; } return false; } @@ -160,20 +172,27 @@ bool mata::nfa::algorithms::is_included_antichains( for (const State& smaller_succ : smaller_move.targets) { const ProdStateType succ = {smaller_succ, bigger_succ, min_dst(bigger_succ)}; - if (lengths_incompatible(succ) || (smaller.final[smaller_succ] && - !bigger.final.intersects_with(bigger_succ))) + if (lengths_incompatible(succ) || + (smaller.final[smaller_succ] && !bigger.final.intersects_with(bigger_succ))) { if (cex != nullptr) { - cex->word.clear(); cex->word.push_back(smaller_symbol); - ProdStateType trav = prod_state; - while (paths[trav].first != trav) + cex->path.push_back(smaller_state); + auto next_on_path = paths.find(prod_state); + while (next_on_path->second.first != next_on_path->first) { // go back until initial state - cex->word.push_back(paths[trav].second); - trav = paths[trav].first; + cex->word.push_back(next_on_path->second.second); + cex->path.push_back(std::get<0>(next_on_path->second.first)); + next_on_path = paths.find(next_on_path->second.first); } std::reverse(cex->word.begin(), cex->word.end()); + std::reverse(cex->path.begin(), cex->path.end()); + + // it is poosible that lengths_incompatible(succ) was true, which means that cex is not finished, we need to add some shortest accepting run from smaller_suc + Run leftover = smaller.get_shortest_accepting_run_from_state(smaller_succ, distances_smaller); + cex->word.insert(cex->word.end(), leftover.word.begin(), leftover.word.end()); + cex->path.insert(cex->path.end(), leftover.path.begin(), leftover.path.end()); } return false; diff --git a/src/nfa/nfa.cc b/src/nfa/nfa.cc index a94b76605..b544ed830 100644 --- a/src/nfa/nfa.cc +++ b/src/nfa/nfa.cc @@ -117,6 +117,25 @@ std::vector Nfa::distances_from_initial() const { return distances; } +std::vector Nfa::distances_to_final() const { + return revert(*this).distances_from_initial(); +} + +Run Nfa::get_shortest_accepting_run_from_state(State q, const std::vector& distances_to_final) const { + Run result{{}, {q}}; + while (!final[q]) { + for (Move move : delta[q].moves()) { + if (distances_to_final[move.target] < distances_to_final[q]) { + result.word.push_back(move.symbol); + result.path.push_back(move.target); + q = move.target; + break; + } + } + } + return result; +} + Nfa& Nfa::trim(StateRenaming* state_renaming) { #ifdef _STATIC_STRUCTURES_ BoolVector useful_states{ useful_states() }; diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index e45771e13..580a4a150 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -1919,12 +1919,18 @@ TEST_CASE("mata::nfa::is_included()") bigger.final = {1}; for (const auto& algo : ALGORITHMS) { - params["algorithm"] = algo; - bool is_incl = is_included(smaller, bigger, &cex, &alph, params); - CHECK(is_incl); - - is_incl = is_included(bigger, smaller, &cex, &alph, params); - CHECK(!is_incl); + SECTION(algo) + { + params["algorithm"] = algo; + bool is_incl = is_included(smaller, bigger, &cex, &alph, params); + CHECK(is_incl); + + is_incl = is_included(bigger, smaller, &cex, &alph, params); + CHECK(!is_incl); + CHECK(cex.word.empty()); + REQUIRE(cex.path.size() == 1); + CHECK(cex.path[0] == 1); + } } } @@ -1937,12 +1943,15 @@ TEST_CASE("mata::nfa::is_included()") bigger.final = {11}; for (const auto& algo : ALGORITHMS) { - params["algorithm"] = algo; - bool is_incl = is_included(smaller, bigger, &cex, &alph, params); - CHECK(is_incl); - - is_incl = is_included(bigger, smaller, &cex, &alph, params); - CHECK(is_incl); + SECTION(algo) + { + params["algorithm"] = algo; + bool is_incl = is_included(smaller, bigger, &cex, &alph, params); + CHECK(is_incl); + + is_incl = is_included(bigger, smaller, &cex, &alph, params); + CHECK(is_incl); + } } } @@ -1953,15 +1962,20 @@ TEST_CASE("mata::nfa::is_included()") smaller.final = {1}; for (const auto& algo : ALGORITHMS) { - params["algorithm"] = algo; - bool is_incl = is_included(smaller, bigger, &cex, &alph, params); - - REQUIRE(!is_incl); - REQUIRE(cex.word.empty()); - - is_incl = is_included(bigger, smaller, &cex, &alph, params); - REQUIRE(cex.word.empty()); - REQUIRE(is_incl); + SECTION(algo) + { + params["algorithm"] = algo; + bool is_incl = is_included(smaller, bigger, &cex, &alph, params); + + REQUIRE(!is_incl); + REQUIRE(cex.word.empty()); + REQUIRE(cex.path.size() == 1); + CHECK(cex.path[0] == 1); + + is_incl = is_included(bigger, smaller, &cex, &alph, params); + REQUIRE(cex.word.empty()); + REQUIRE(is_incl); + } } } @@ -1979,12 +1993,15 @@ TEST_CASE("mata::nfa::is_included()") bigger.delta.add(11, alph["b"], 11); for (const auto& algo : ALGORITHMS) { - params["algorithm"] = algo; - bool is_incl = is_included(smaller, bigger, &alph, params); - REQUIRE(is_incl); - - is_incl = is_included(bigger, smaller, &alph, params); - REQUIRE(!is_incl); + SECTION(algo) + { + params["algorithm"] = algo; + bool is_incl = is_included(smaller, bigger, &alph, params); + REQUIRE(is_incl); + + is_incl = is_included(bigger, smaller, &alph, params); + REQUIRE(!is_incl); + } } } @@ -2002,20 +2019,25 @@ TEST_CASE("mata::nfa::is_included()") bigger.delta.add(12, alph["b"], 12); for (const auto& algo : ALGORITHMS) { - params["algorithm"] = algo; - - bool is_incl = is_included(smaller, bigger, &cex, &alph, params); - - REQUIRE(!is_incl); - REQUIRE(( - cex.word == Word{alph["a"], alph["b"]} || - cex.word == Word{alph["b"], alph["a"]})); - - is_incl = is_included(bigger, smaller, &cex, &alph, params); - REQUIRE(is_incl); - REQUIRE(( - cex.word == Word{alph["a"], alph["b"]} || - cex.word == Word{alph["b"], alph["a"]})); + SECTION(algo) + { + params["algorithm"] = algo; + + bool is_incl = is_included(smaller, bigger, &cex, &alph, params); + + REQUIRE(!is_incl); + REQUIRE(( + cex.word == Word{alph["a"], alph["b"]} || + cex.word == Word{alph["b"], alph["a"]})); + REQUIRE(cex.path == std::vector{1,1,1}); + + is_incl = is_included(bigger, smaller, &cex, &alph, params); + REQUIRE(is_incl); + REQUIRE(( + cex.word == Word{alph["a"], alph["b"]} || + cex.word == Word{alph["b"], alph["a"]})); + REQUIRE(cex.path == std::vector{1,1,1}); + } } } @@ -2042,26 +2064,142 @@ TEST_CASE("mata::nfa::is_included()") bigger.delta.add(15, alph["b"], 15); for (const auto& algo : ALGORITHMS) { - params["algorithm"] = algo; - bool is_incl = is_included(smaller, bigger, &cex, &alph, params); - REQUIRE(!is_incl); - - REQUIRE(cex.word.size() == 4); - REQUIRE((cex.word[0] == alph["a"] || cex.word[0] == alph["b"])); - REQUIRE((cex.word[1] == alph["a"] || cex.word[1] == alph["b"])); - REQUIRE((cex.word[2] == alph["a"] || cex.word[2] == alph["b"])); - REQUIRE((cex.word[3] == alph["a"] || cex.word[3] == alph["b"])); - REQUIRE(cex.word[2] != cex.word[3]); - - is_incl = is_included(bigger, smaller, &cex, &alph, params); - REQUIRE(is_incl); + SECTION(algo) + { + params["algorithm"] = algo; + bool is_incl = is_included(smaller, bigger, &cex, &alph, params); + REQUIRE(!is_incl); + + REQUIRE(cex.word.size() == 4); + REQUIRE((cex.word[0] == alph["a"] || cex.word[0] == alph["b"])); + REQUIRE((cex.word[1] == alph["a"] || cex.word[1] == alph["b"])); + REQUIRE((cex.word[2] == alph["a"] || cex.word[2] == alph["b"])); + REQUIRE((cex.word[3] == alph["a"] || cex.word[3] == alph["b"])); + REQUIRE(cex.word[2] != cex.word[3]); + REQUIRE(cex.path == std::vector{1,1,1,1,1}); + + is_incl = is_included(bigger, smaller, &cex, &alph, params); + REQUIRE(is_incl); + + REQUIRE(cex.word.size() == 4); + REQUIRE((cex.word[0] == alph["a"] || cex.word[0] == alph["b"])); + REQUIRE((cex.word[1] == alph["a"] || cex.word[1] == alph["b"])); + REQUIRE((cex.word[2] == alph["a"] || cex.word[2] == alph["b"])); + REQUIRE((cex.word[3] == alph["a"] || cex.word[3] == alph["b"])); + REQUIRE(cex.word[2] != cex.word[3]); + REQUIRE(cex.path == std::vector{1,1,1,1,1}); + } + } + } - REQUIRE(cex.word.size() == 4); - REQUIRE((cex.word[0] == alph["a"] || cex.word[0] == alph["b"])); - REQUIRE((cex.word[1] == alph["a"] || cex.word[1] == alph["b"])); - REQUIRE((cex.word[2] == alph["a"] || cex.word[2] == alph["b"])); - REQUIRE((cex.word[3] == alph["a"] || cex.word[3] == alph["b"])); - REQUIRE(cex.word[2] != cex.word[3]); + SECTION("large example") + { + plumbing::construct(&smaller, mata::IntermediateAut::parse_from_mf(parse_mf( +R"(@NFA-explicit +%Alphabet-auto +%Initial q0 +%Final q10 +q0 65 q1 +q0 66 q1 +q0 67 q1 +q0 196608 q1 +q1 65 q2 +q1 66 q2 +q1 67 q2 +q1 196608 q2 +q2 65 q2 +q2 65 q3 +q2 66 q2 +q2 66 q4 +q2 67 q2 +q2 196608 q2 +q4 66 q5 +q5 66 q6 +q6 65 q6 +q6 65 q7 +q6 66 q6 +q6 67 q6 +q6 196608 q6 +q7 67 q8 +q8 67 q9 +q9 67 q10 +q10 65 q10 +q10 66 q10 +q10 67 q10 +q10 196608 q10 +q3 67 q11 +q11 67 q12 +q12 67 q13 +q13 65 q13 +q13 66 q13 +q13 66 q14 +q13 67 q13 +q13 196608 q13 +q14 66 q15 +q15 66 q16 +q16 65 q10 +q16 66 q10 +q16 67 q10 +q16 196608 q10 +)" + ))[0]); + plumbing::construct(&bigger, mata::IntermediateAut::parse_from_mf(parse_mf( +R"(@NFA-explicit +%Alphabet-auto +%Initial q0 q7 +%Final q6 +q0 65 q1 +q0 66 q1 +q0 67 q1 +q0 196608 q1 +q1 65 q2 +q1 66 q2 +q1 67 q2 +q1 196608 q2 +q2 65 q2 +q2 66 q2 +q2 66 q3 +q2 67 q2 +q2 196608 q2 +q3 66 q4 +q4 66 q5 +q5 66 q6 +q6 65 q6 +q6 66 q6 +q6 67 q6 +q6 196608 q6 +q7 65 q8 +q7 66 q8 +q7 67 q8 +q7 196608 q8 +q8 65 q8 +q8 66 q9 +q8 67 q8 +q8 196608 q8 +q9 65 q9 +q9 65 q10 +q9 66 q9 +q9 67 q9 +q9 196608 q9 +q10 67 q5 +)" + ))[0]); + + for (const auto& algo : ALGORITHMS) { + SECTION(algo) + { + params["algorithm"] = algo; + bool is_incl = is_included(smaller, bigger, &cex, nullptr, params); + REQUIRE(!is_incl); + REQUIRE(smaller.is_in_lang(cex.word)); + REQUIRE(!bigger.is_in_lang(cex.word)); + REQUIRE(cex.path.size() == cex.word.size() + 1); + for (size_t i = 0; i < cex.word.size(); ++i) { + const auto& s = smaller.delta[cex.path[i]].find(cex.word[i]); + REQUIRE(s != smaller.delta[cex.path[i]].end()); + CHECK(s->targets.contains(cex.path[i+1])); + } + } } }