diff --git a/apps/UnitTestsApp/src/UnitTests.cpp b/apps/UnitTestsApp/src/UnitTests.cpp index 0192ec4b..8ddb1a0b 100644 --- a/apps/UnitTestsApp/src/UnitTests.cpp +++ b/apps/UnitTestsApp/src/UnitTests.cpp @@ -795,6 +795,7 @@ TEST(TestBisimilar, MFA_Bisimilar) { {"[a*]:1&1", "[a*]:1a*&1", false}, {"[a*a*|]:1&1", "[a*]:1&1", true}, {"[a|a]:1*&1", "[a]:1*[a]:1*&1", true}, + {"[a]:1*[a*]:1&1", "[a|]:1*&1", false}, }; for_each(tests.begin(), tests.end(), [](const Test& test) { diff --git a/libs/Objects/include/Objects/FiniteAutomaton.h b/libs/Objects/include/Objects/FiniteAutomaton.h index abb4494e..1b43c5fc 100644 --- a/libs/Objects/include/Objects/FiniteAutomaton.h +++ b/libs/Objects/include/Objects/FiniteAutomaton.h @@ -99,7 +99,7 @@ class FiniteAutomaton : public AbstractMachine { std::stack& order // NOLINT(runtime/references) ); // возвращает компоненты сильной связности - std::vector> get_SCCs(); + std::vector> get_SCCs(); FiniteAutomaton get_subautomaton(const CaptureGroup&); diff --git a/libs/Objects/src/FiniteAutomaton.cpp b/libs/Objects/src/FiniteAutomaton.cpp index af22355d..25451ddc 100644 --- a/libs/Objects/src/FiniteAutomaton.cpp +++ b/libs/Objects/src/FiniteAutomaton.cpp @@ -2658,9 +2658,10 @@ void FiniteAutomaton::fill_order(int state_index, vector& visited, stack& reversed_transitions, - vector& visited, vector& component) { // NOLINT(runtime/references) + vector& visited, // NOLINT(runtime/references) + unordered_set& component) { // NOLINT(runtime/references) visited[state_index] = true; - component.push_back(state_index); + component.insert(state_index); for (const auto& [symbol, symbol_transitions] : reversed_transitions[state_index]) for (const auto& to : symbol_transitions) @@ -2668,8 +2669,8 @@ void find_scc_dfs(int state_index, const vector& reversed_ find_scc_dfs(to, reversed_transitions, visited, component); } -std::vector> FiniteAutomaton::get_SCCs() { - vector> SCCs; +std::vector> FiniteAutomaton::get_SCCs() { + vector> SCCs; stack order; vector visited(size(), false); @@ -2685,13 +2686,13 @@ std::vector> FiniteAutomaton::get_SCCs() { order.pop(); if (!visited[state_index]) { - vector component; + unordered_set component; find_scc_dfs(state_index, reversed_transitions, visited, component); bool has_internal_transitions = false; for (int state : component) { for (const auto& [symbol, symbol_transitions] : states[state].transitions) for (int to : symbol_transitions) - if (find(component.begin(), component.end(), to) != component.end()) { + if (component.count(to)) { has_internal_transitions = true; break; } diff --git a/libs/Objects/src/MemoryFiniteAutomaton.cpp b/libs/Objects/src/MemoryFiniteAutomaton.cpp index fa296927..99881493 100644 --- a/libs/Objects/src/MemoryFiniteAutomaton.cpp +++ b/libs/Objects/src/MemoryFiniteAutomaton.cpp @@ -1415,12 +1415,13 @@ bool MemoryFiniteAutomaton::states_have_decisions( optional MemoryFiniteAutomaton::bisimilarity_checker(const MemoryFiniteAutomaton& mfa1, const MemoryFiniteAutomaton& mfa2) { const int N = 2; + vector mfas({&mfa1, &mfa2}); // раскрашиваем состояния vector>> mfa_colors(N); - vector visited(mfa1.size(), false); - mfa1.color_mem_dfs(mfa1.get_initial(), visited, {}, mfa_colors[0]); - visited.assign(mfa2.size(), false); - mfa2.color_mem_dfs(mfa2.get_initial(), visited, {}, mfa_colors[1]); + for (int i = 0; i < N; i++) { + vector visited(mfas[i]->size(), false); + mfas[i]->color_mem_dfs(mfas[i]->get_initial(), visited, {}, mfa_colors[i]); + } // using std::cout; // cout << mfa1.to_txt() << mfa2.to_txt(); for (const auto& mfa_colors_i : mfa_colors) @@ -1436,15 +1437,40 @@ optional MemoryFiniteAutomaton::bisimilarity_checker(const MemoryFiniteAut if (!res) return false; // проверяем совпадение раскраски эквивалентных состояний в КСС - vector>> SCCs({fas[0].get_SCCs(), fas[1].get_SCCs()}); + vector>> SCCs({fas[0].get_SCCs(), fas[1].get_SCCs()}); vector>>>> colored_SCCs(N); for (int i = 0; i < N; i++) { for (const auto& SCC : SCCs[i]) { + unordered_set colors_to_ignore; + for (auto state : SCC) { + unordered_set state_colors_to_ignore; + bool has_transitions_without_actions = false; + for (const auto& [symbol, symbol_transitions] : + mfas[i]->states[state].transitions) { + for (const auto& tr : symbol_transitions) { + if (SCC.count(tr.to)) { + if (tr.memory_actions.empty()) { + state_colors_to_ignore.clear(); + has_transitions_without_actions = true; + break; + } + for (const auto& [cell, action] : tr.memory_actions) + state_colors_to_ignore.insert(cell); + } + } + if (has_transitions_without_actions) + break; + } + colors_to_ignore.insert(state_colors_to_ignore.begin(), + state_colors_to_ignore.end()); + } + set>> colored_SCC; for (auto j : SCC) { unordered_set j_colors; - if (!mfa_colors[i].at(j).empty()) - j_colors = mfa_colors[i].at(j); + for (auto color : mfa_colors[i].at(j)) + if (!colors_to_ignore.count(color)) + j_colors.insert(color); colored_SCC.insert({fa_classes[i][j], set(j_colors.begin(), j_colors.end())}); } if (!colored_SCC.empty())