Merge pull request #354 from OnionGrief/bisim

MFA::Bisimilar fixes

apps/MetamorphicTestsApp/src/MetamorphicTests.cpp

@@ -89,7 +89,7 @@ std::string MetamorphicTests::generate_bregex(RegexGenerator& rg, int cells_num)
 				condition = false;
 			}
 		if (condition)
-			condition &= r.check_refs();
+			condition &= r.check_refs_and_memory_writers_usefulness();
 	} while (!condition);
 
 	return rgx_str;
@@ -144,14 +144,23 @@ TEST(TestMFA, Fuzzing) {
 }
 
 // TEST(TestMFA, Fuzz) {
-//	string rgx_str = "(a[[b|]:1|]:2*[[c|]:1|]:2*&1&2)*";
-//	MemoryFiniteAutomaton mfa1 = BackRefRegex(rgx_str).to_mfa();
-//	MemoryFiniteAutomaton mfa2 = BackRefRegex(rgx_str).to_mfa_additional();
+//	BackRefRegex rgx("");
+//	MemoryFiniteAutomaton mfa1 = rgx.to_mfa();
+//	MemoryFiniteAutomaton mfa2 = rgx.to_mfa_additional();
 //
 //	std::cout << mfa1.to_txt() << mfa2.to_txt();
 //
 //	MetamorphicTests::cmp_automatons(mfa1, mfa2);
-//}
+// }
+
+// TEST(TestMFA, Cmp) {
+//	MemoryFiniteAutomaton mfa1 = BackRefRegex().to_mfa_additional();
+//	MemoryFiniteAutomaton mfa2 = BackRefRegex().to_mfa_additional();
+//
+//	std::cout << mfa1.to_txt() << mfa2.to_txt();
+//
+//	MetamorphicTests::cmp_automatons(mfa1, mfa2);
+// }
 
 TEST(TestMFA, ToTxt) {
 	RegexGenerator rg(5, 3, 3, 2);

apps/UnitTestsApp/src/UnitTests.cpp

@@ -49,6 +49,10 @@ TEST(TestParseString, FromString) {
 		{"a|(c^)", false, false, 8}, // a | ( c . ^ eps )
 		{"[b[a]:1&1]:2&2^a", true, true},
 		{"[b[a]:1&1]:2&2^a", true, false},
+		{"[a]:1[]:1&1", false, true, 9},
+		{"[a]:1[(|)]:1&1", true, true},
+		{"O1aC1R1&1", false, false, 9},
+		{"O1aC1X1&1", true, false},
 	};
 
 	for (const auto& t : tests) {
@@ -755,6 +759,27 @@ TEST(TestParsing, MFA_equivalence) {
 	});
 }
 
+TEST(TestBrgexChecker, CheckRefsAndMWs) {
+	using Test = std::tuple<string, bool>;
+	vector<Test> tests = {
+		{"[a]:1&1", true},
+		{"&1[a]:1", false},
+		{"(&1[a]:1)*", true},
+		{"&1[a]:1&1", false},
+		{"[a]:1&1[a]:2", false},
+		{"&2[a]:1&1[a]:2", false},
+		{"(&2[a]:1&1[a]:2)*", true},
+		{"(&1[a]:1[a]:1&1[a]:2)*", false},
+		{"(&2[a]:1&1[a]:2)*[a]:3*", false},
+		{"(&2[a]:1&1[a]:2)*[a]:3*&3", true},
+	};
+	for_each(tests.begin(), tests.end(), [](const Test& test) {
+		auto [rgx, expected_res] = test;
+		SCOPED_TRACE(rgx);
+		ASSERT_EQ(BackRefRegex(rgx).check_refs_and_memory_writers_usefulness(), expected_res);
+	});
+}
+
 TEST(TestReverse, BRegex_Reverse) {
 	ASSERT_TRUE(BackRefRegex::equal(BackRefRegex("([a*b]:1&1|b&1)").reverse(),
 									BackRefRegex("[ba*]:1&1|&1b")));
@@ -772,6 +797,8 @@ TEST(TestBisimilar, MFA_Bisimilar) {
 		{"[a|a]:1*&1", "[a]:1*[a]:1*&1", true},
 		{"[a]:1*&1|[b]:1&1", "[b]:1&1|[a]:1*&1", true},
 		{"[a]:1&1(&1|[b]:1)*", "[a]:1&1(&1|[b]:1)*", true},
+		{"[a|b]:1*&1", "(|[a|b]:1(a|b)*)&1", true},
+		{"[ab*]:1*&1", "[ab*b*]:1*&1", true},
 		// перекрестная бисимуляция
 		{"[a*]:1a*&1", "a*[a*]:1&1", false},
 		{"b[a*]:1a*&1", "ba*[a*]:1&1", false},
@@ -780,6 +807,8 @@ TEST(TestBisimilar, MFA_Bisimilar) {
 		// несовпадение раскрасок
 		{"[a]:1*&1", "[a*]:1*&1", false},
 		{"[a]:1*[a*]:1&1", "[a|]:1*&1", false},
+		{"([a|]:1*&1)*", "([aa*|]:1&1)*", false},
+		{"b*[a*]:1*&1", "b*[a*]:1&1", false},
 		// несовпадение по решающим действиям
 		{"[a|b]:1c(a|b)&1", "(a|b)c[a|b]:1&1", false},
 		// несовпадение CG

libs/AutomatonToImage/src/AutomatonToImage.cpp

@@ -1,17 +1,42 @@
 #include <fstream>
 #include <iostream>
+#include <regex>
 #include <sstream>
+#include <vector>
 
 #include "AutomatonToImage/AutomatonToImage.h"
 
+using std::cout;
 using std::ifstream;
+using std::ofstream;
 using std::string;
 using std::stringstream;
+using std::vector;
 
 AutomatonToImage::AutomatonToImage() {}
 
 AutomatonToImage::~AutomatonToImage() {}
 
+string replace_before_dot2tex(const string& s) {
+	vector<std::pair<string, string>> substrs_to_replace = {{"\\^", "#^ "}, {"&", "#&"}};
+
+	string result = s;
+	for (const auto& [old_substr, new_substr] : substrs_to_replace) {
+		std::regex re(old_substr);
+		result = std::regex_replace(result, re, new_substr);
+	}
+
+	return result;
+}
+
+void write_to_file(const string& file_name, const string& content) {
+	ofstream file;
+	file.open(file_name, ofstream::trunc);
+	if (file.is_open())
+		file << content;
+	file.close();
+}
+
 void remove_file(string dir, string file, bool guarded = false) {
 	stringstream command;
 	command << "cd " << dir;
@@ -32,13 +57,13 @@ void remove_file(string dir, string file, bool guarded = false) {
 string AutomatonToImage::to_image(string automaton) {
 	remove_file("refal", "Meta_log.raux", true);
 	remove_file("refal", "Aux_input.raux", true);
-	FILE* fo;
-	fo = fopen("./refal/input.dot", "wt");
-	fprintf(fo, "%s", automaton.c_str());
-	fclose(fo);
+	ofstream fo;
+	write_to_file("./refal/input.dot", replace_before_dot2tex(automaton));
 	system("cd refal && refgo Preprocess+MathMode+FrameFormatter input.dot > "
 		   "error_Preprocess.raux");
+
 	system("cd refal && dot2tex -ftikz -tmath \"Mod_input.dot\" > input.tex");
+
 	system("cd refal && refgo Postprocess+MathMode+FrameFormatter input.tex > "
 		   "error_Postprocess.raux "
 		   "2>&1");
@@ -67,16 +92,10 @@ string AutomatonToImage::to_image(string automaton) {
 
 string AutomatonToImage::colorize(string automaton, string metadata) {
 
-	FILE* fo;
-	FILE* md;
 	ifstream infile_for_Final;
-	fo = fopen("./refal/Col_input.tex", "wt");
-	fprintf(fo, "%s", automaton.c_str());
-	fclose(fo);
+	write_to_file("./refal/Col_input.tex", automaton);
 	if (metadata != "") {
-		md = fopen("./refal/Meta_input.raux", "wt");
-		fprintf(md, "%s", metadata.c_str());
-		fclose(md);
+		write_to_file("./refal/Meta_input.raux", metadata);
 		system("cd refal && refgo Colorize+MathMode Col_input.tex > "
 			   "error_Colorize.raux");
 		infile_for_Final.open("./refal/Final_input.tex");

libs/Interpreter/src/Interpreter.cpp

@@ -1087,7 +1087,8 @@ optional<Interpreter::Expression> Interpreter::scan_expression(const vector<Lexe
 	if (end > pos && lexems[pos].type == Lexem::regex) {
 		string str = lexems[pos].value;
 		// выбор между backref и regex
-		if (str.find("&") != string::npos || str.find(":") != string::npos) {
+		// TODO: костыль
+		if (str.find('&') != string::npos || str.find("]:") != string::npos) {
 			expr.type = ObjectType::BRefRegex;
 			expr.value = BackRefRegex(str);
 		} else {

libs/Logger/src/LogTemplate.cpp

@@ -145,7 +145,6 @@ string LogTemplate::render() const {
 						automaton = std::get<FiniteAutomaton>(param.value).to_txt();
 					else
 						automaton = std::get<MemoryFiniteAutomaton>(param.value).to_txt();
-					automaton = replace_for_rendering(automaton);
 					size_t hash = hasher(automaton);
 					if (cache_automatons.count(hash) != 0) {
 						c_graph = cache_automatons[hash];
@@ -245,16 +244,11 @@ string LogTemplate::log_table(Table t) {
 	table += "$\\begin{array}{" + format + "}\\rowcolor{HeaderColor}\n";
 	table += cols + "\\hline\n";
 	for (int i = 0; i < t.rows.size(); i++) {
-		string r = t.rows[i] == " " ? "eps" : t.rows[i];
-		row = r + " & ";
+		row = t.rows[i] == " " ? "eps" : t.rows[i];
 		for (int j = 0; j < t.columns.size(); j++) {
-			if (j != t.columns.size() - 1) {
-				row = row + t.data[i * t.columns.size() + j] + " &";
-			} else {
-				row = row + t.data[i * t.columns.size() + j] + "\\\\";
-			}
+			row += " & " + replace_for_rendering(t.data[i * t.columns.size() + j]);
 		}
-		table += row + "\n";
+		table += row + "\\\\\n";
 	}
 	table += "\\end{array}$\n";
 	return table;

libs/Objects/include/Objects/BackRefRegex.h

@@ -51,6 +51,7 @@ class BackRefRegex : public AlgExpression {
 
 	// возвращает вектор листьев дерева
 	// устанавливает для них in_lin_cells, first_in_cells и last_in_cells
+	// линеаризует memoryWriters
 	void preorder_traversal(
 		std::vector<BackRefRegex*>& terms,					// NOLINT(runtime/references)
 		int& lin_counter,									// NOLINT(runtime/references)
@@ -79,15 +80,17 @@ class BackRefRegex : public AlgExpression {
 													   CellSet>>>& // NOLINT(runtime/references)
 	) const;
 
-	// преобразует star в conc (раскрывает каждую итерацию один раз) и линеаризует memoryWriter
+	// преобразует star в conc (раскрывает каждую итерацию один раз) и линеаризует memoryWriters
 	void unfold_iterations(int& number); // NOLINT(runtime/references)
 	// рекурсивно проверяет, является ли регулярное выражение ацикличным
 	bool _is_acreg(
 		std::unordered_set<int>, std::unordered_set<int>,
 		std::unordered_map<int, std::unordered_set<int>>&) const; // NOLINT(runtime/references)
 
 	void linearize_refs(int& number); // NOLINT(runtime/references)
-	void _check_refs(std::unordered_set<int>&, std::unordered_set<int>&) const;
+	void _check_memory_writers(std::unordered_map<int, std::unordered_set<int>>&,
+							   std::unordered_set<int>&,		// NOLINT(runtime/references)
+							   std::unordered_set<int>&) const; // NOLINT(runtime/references)
 
 	// меняет порядок конкатенаций в дереве (swap term_l и term_r)
 	void _reverse(std::unordered_map<int, BackRefRegex*>&); // NOLINT(runtime/references)
@@ -123,6 +126,8 @@ class BackRefRegex : public AlgExpression {
 	// обращение выражения (для СНФ)
 	BackRefRegex reverse(iLogTemplate* log = nullptr) const;
 	// проверяет, что каждая ссылка может следовать за записью в память (соответствующую ячейку)
-	bool check_refs() const;
+	// и что каждый memoryWriter не будет однозначно переинициализирован без возможности
+	// сослаться на него (существует хотя бы один путь, в котором присутствует ссылка на него)
+	bool check_refs_and_memory_writers_usefulness() const;
 	BackRefRegex rewrite_aci() const;
 };

libs/Objects/include/Objects/FiniteAutomaton.h

@@ -73,10 +73,10 @@ class FiniteAutomaton : public AbstractMachine {
 	// eps-переходам (если флаг установлен в 0 - по всем переходам)
 	std::set<int> closure(const std::set<int>&, bool) const;
 
-	std::vector<int> get_bisimilar_classes() const;
+	std::vector<int> get_bisimulation_classes() const;
 	// объединение эквивалентных классов (принимает на вход вектор размера states.size())
 	// на i-й позиции номер класса i-го состояния
-	std::tuple<FiniteAutomaton, std::unordered_map<int, int>> merge_equivalent_classes(
+	std::tuple<FiniteAutomaton, std::unordered_map<int, int>> merge_classes(
 		const std::vector<int>&) const;
 	static bool equality_checker(const FiniteAutomaton& fa1, const FiniteAutomaton& fa2);
 	// дополнительно возвращает в векторах номера классов состояний каждого автомата
@@ -118,8 +118,6 @@ class FiniteAutomaton : public AbstractMachine {
 					std::unordered_map<int, int>& states_mapping, // NOLINT(runtime/references)
 					MFATransition::MemoryActions memory_actions, int from_mfa_state) const;
 
-	FiniteAutomaton get_subautomaton(const CaptureGroup&);
-
   public:
 	FiniteAutomaton();
 	FiniteAutomaton(int initial_state, std::vector<FAState> states,

libs/Objects/include/Objects/MemoryCommon.h

@@ -2,6 +2,7 @@
 #include <iostream>
 #include <optional>
 #include <string>
+#include <tuple>
 #include <unordered_map>
 #include <unordered_set>
 #include <utility>
@@ -66,7 +67,7 @@ struct MFATransition {
 	};
 };
 
-struct CaptureGroup {
+class CaptureGroup {
 	struct State {
 		int index;
 		int class_num;
@@ -82,14 +83,25 @@ struct CaptureGroup {
 	std::unordered_set<std::vector<int>, VectorHasher<int>> paths;
 	std::unordered_set<State, State::Hasher> states;
 	std::unordered_set<int> state_classes;
+	bool is_reset;
 
+  public:
 	CaptureGroup() = default;
 	CaptureGroup(int, const std::vector<std::vector<int>>&, const std::vector<int>&,
-				 bool reset = false);
+				 bool is_reset = false);
 	bool operator==(const CaptureGroup& other) const;
 
-	std::unordered_set<int> get_states_diff(
-		const std::unordered_set<int>& other_state_classes) const;
+	bool get_is_reset() const;
+	bool get_cell_number() const;
+	int get_opening_state_index() const;
+
+	const std::unordered_set<std::vector<int>, VectorHasher<int>>& get_paths() const;
+	const std::unordered_set<State, State::Hasher>& get_states() const;
+
+	std::tuple<std::unordered_set<int>, std::unordered_set<int>> get_states_diff(
+		const CaptureGroup& other) const;
+
+	friend std::ostream& operator<<(std::ostream& os, const CaptureGroup& cg);
 };
 
 std::ostream& operator<<(std::ostream& os, const CaptureGroup& cg);

libs/Objects/include/Objects/MemoryFiniteAutomaton.h

@@ -147,7 +147,7 @@ class MemoryFiniteAutomaton : public AbstractMachine {
 	std::pair<int, bool> _parse_slow(const std::string&, Matcher*) const;
 	std::pair<int, bool> _parse(const std::string&, Matcher*) const;
 
-	// поиск множества состояний НКА,
+	// поиск множества состояний MFA,
 	// достижимых из множества состояний по eps-переходам
 	std::tuple<std::set<int>, std::unordered_set<int>, MFATransition::MemoryActions>
 	get_eps_closure(const std::set<int>& indices) const;
@@ -158,7 +158,7 @@ class MemoryFiniteAutomaton : public AbstractMachine {
 		int state_index,
 		std::vector<bool>& visited, // NOLINT(runtime/references)
 		const MemoryConfiguration& opened_cells,
-		std::unordered_map<int, std::unordered_set<int>>& colors, // NOLINT(runtime/references)
+		std::vector<std::unordered_set<int>>& state_colors, // NOLINT(runtime/references)
 		const std::vector<int>& ab_classes,
 		std::unordered_map<int, int>& ab_class_to_first_state // NOLINT(runtime/references)
 	) const;
@@ -168,21 +168,30 @@ class MemoryFiniteAutomaton : public AbstractMachine {
 	std::vector<MFAState::Transitions> get_reversed_transitions() const;
 
 	std::pair<std::vector<std::vector<int>>, std::vector<std::vector<int>>> find_cg_paths(
-		int state_index, std::unordered_set<int> visited, int cell, int opening_state) const;
+		int state_index, std::unordered_set<int> visited, int cell, int opening_state,
+		bool was_in_opening_state) const;
 	std::vector<CaptureGroup> find_capture_groups_backward(
-		int ref_incoming_state, int cell, const std::vector<int>& fa_classes) const;
+		int ref_incoming_state, int cell,
+		const std::vector<MFAState::Transitions>& reversed_transitions,
+		const std::vector<int>& fa_classes) const;
 
 	bool find_decisions(int state_index,
 						std::vector<int>& visited, // NOLINT(runtime/references)
-						const std::unordered_set<int>& states_to_check) const;
-	bool states_have_decisions(const std::unordered_set<int>& states_to_check) const;
+						const std::unordered_set<int>& states_to_check,
+						const std::unordered_set<int>& following_states,
+						const CaptureGroup& cg) const;
+	bool states_have_decisions(const std::unordered_set<int>& states_to_check,
+							   const std::unordered_set<int>& following_states,
+							   const CaptureGroup& cg) const;
+
+	FiniteAutomaton get_cg_fa(const CaptureGroup& cg) const;
 
 	static std::optional<bool> bisimilarity_checker(const MemoryFiniteAutomaton&,
 													const MemoryFiniteAutomaton&);
 
 	// объединение эквивалентных классов (принимает на вход вектор размера states.size())
 	// на i-й позиции номер класса i-го состояния
-	std::tuple<MemoryFiniteAutomaton, std::unordered_map<int, int>> merge_equivalent_classes(
+	std::tuple<MemoryFiniteAutomaton, std::unordered_map<int, int>> merge_classes(
 		const std::vector<int>&) const;
 
   public:

libs/Objects/include/Objects/Symbol.h

@@ -6,7 +6,7 @@
 #include <vector>
 
 // Символ, по которому осуществляются переходы в автомате.
-// Может быть символом-буквой (и входить в алфавит) или ссылкой (&i)
+// Может быть символом-буквой (и входить ТОЛЬКО в алфавит FA) или ссылкой (&i)
 class Symbol {
   private:
 	std::vector<int> annote_numbers;
@@ -90,4 +90,6 @@ class MemorySymbols {
 	static bool is_open(const Symbol& s);
 
 	static int get_cell_number(const Symbol& s);
-};
+};
+
+bool is_special_symbol(const Symbol& s);

libs/Objects/include/Objects/Tools.h

@@ -33,7 +33,7 @@ struct TupleHasher {
 	size_t operator()(const std::tuple<int, int, int>& p) const;
 };
 
-using IntPairSet = std::unordered_set<std::pair<int, int>, IntPairHasher>;
+using IntPairsSet = std::unordered_set<std::pair<int, int>, IntPairHasher>;
 
 std::ostream& operator<<(std::ostream& os, const std::vector<int>& vec);