(#330) SCCs coloring fix

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) {

libs/Objects/include/Objects/FiniteAutomaton.h

@@ -99,7 +99,7 @@ class FiniteAutomaton : public AbstractMachine {
 					std::stack<int>& order						 // NOLINT(runtime/references)
 	);
 	// возвращает компоненты сильной связности
-	std::vector<std::vector<int>> get_SCCs();
+	std::vector<std::unordered_set<int>> get_SCCs();
 
 	FiniteAutomaton get_subautomaton(const CaptureGroup&);
 

libs/Objects/src/FiniteAutomaton.cpp

@@ -2658,18 +2658,19 @@ void FiniteAutomaton::fill_order(int state_index, vector<bool>& visited, stack<i
 }
 
 void find_scc_dfs(int state_index, const vector<FAState::Transitions>& reversed_transitions,
-				  vector<bool>& visited, vector<int>& component) { // NOLINT(runtime/references)
+				  vector<bool>& visited,		   // NOLINT(runtime/references)
+				  unordered_set<int>& 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)
 			if (!visited[to])
 				find_scc_dfs(to, reversed_transitions, visited, component);
 }
 
-std::vector<std::vector<int>> FiniteAutomaton::get_SCCs() {
-	vector<vector<int>> SCCs;
+std::vector<std::unordered_set<int>> FiniteAutomaton::get_SCCs() {
+	vector<unordered_set<int>> SCCs;
 	stack<int> order;
 
 	vector<bool> visited(size(), false);
@@ -2685,13 +2686,13 @@ std::vector<std::vector<int>> FiniteAutomaton::get_SCCs() {
 		order.pop();
 
 		if (!visited[state_index]) {
-			vector<int> component;
+			unordered_set<int> 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;
 						}

libs/Objects/src/MemoryFiniteAutomaton.cpp

@@ -1415,12 +1415,13 @@ bool MemoryFiniteAutomaton::states_have_decisions(
 optional<bool> MemoryFiniteAutomaton::bisimilarity_checker(const MemoryFiniteAutomaton& mfa1,
 														   const MemoryFiniteAutomaton& mfa2) {
 	const int N = 2;
+	vector<const MemoryFiniteAutomaton*> mfas({&mfa1, &mfa2});
 	// раскрашиваем состояния
 	vector<unordered_map<int, unordered_set<int>>> mfa_colors(N);
-	vector<bool> 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<bool> 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<bool> MemoryFiniteAutomaton::bisimilarity_checker(const MemoryFiniteAut
 	if (!res)
 		return false;
 	// проверяем совпадение раскраски эквивалентных состояний в КСС
-	vector<vector<vector<int>>> SCCs({fas[0].get_SCCs(), fas[1].get_SCCs()});
+	vector<vector<unordered_set<int>>> SCCs({fas[0].get_SCCs(), fas[1].get_SCCs()});
 	vector<set<set<pair<int, set<int>>>>> colored_SCCs(N);
 	for (int i = 0; i < N; i++) {
 		for (const auto& SCC : SCCs[i]) {
+			unordered_set<int> colors_to_ignore;
+			for (auto state : SCC) {
+				unordered_set<int> 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<pair<int, set<int>>> colored_SCC;
 			for (auto j : SCC) {
 				unordered_set<int> 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<int>(j_colors.begin(), j_colors.end())});
 			}
 			if (!colored_SCC.empty())