Skip to content

Commit

Permalink
(#330) fixed decisions detection
Browse files Browse the repository at this point in the history
+ refactoring
  • Loading branch information
xendalm committed Jun 15, 2024
1 parent f482c21 commit 968f233
Show file tree
Hide file tree
Showing 7 changed files with 77 additions and 54 deletions.
4 changes: 2 additions & 2 deletions libs/Objects/include/Objects/FiniteAutomaton.h
Original file line number Diff line number Diff line change
Expand Up @@ -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);
// дополнительно возвращает в векторах номера классов состояний каждого автомата
Expand Down
4 changes: 3 additions & 1 deletion libs/Objects/include/Objects/MemoryCommon.h
Original file line number Diff line number Diff line change
Expand Up @@ -91,12 +91,14 @@ class CaptureGroup {
bool operator==(const CaptureGroup& other) 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::unordered_set<int> get_states_diff(const CaptureGroup& other) 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);
};
Expand Down
12 changes: 8 additions & 4 deletions libs/Objects/include/Objects/MemoryFiniteAutomaton.h
Original file line number Diff line number Diff line change
Expand Up @@ -176,17 +176,21 @@ class MemoryFiniteAutomaton : public AbstractMachine {

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&) 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:
Expand Down
2 changes: 1 addition & 1 deletion libs/Objects/include/Objects/Tools.h
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down
26 changes: 13 additions & 13 deletions libs/Objects/src/FiniteAutomaton.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -383,7 +383,7 @@ FiniteAutomaton FiniteAutomaton::minimize(bool is_trim, iLogTemplate* log) const
classes[groups[i][j]] = i;
}
}
auto [minimized_dfa, class_to_index] = dfa.merge_equivalent_classes(classes);
auto [minimized_dfa, class_to_index] = dfa.merge_classes(classes);

// кэширование
language->set_min_dfa(minimized_dfa);
Expand Down Expand Up @@ -1361,7 +1361,7 @@ bool FiniteAutomaton::is_one_unambiguous(iLogTemplate* log) const {
return true;
}

tuple<FiniteAutomaton, unordered_map<int, int>> FiniteAutomaton::merge_equivalent_classes(
tuple<FiniteAutomaton, unordered_map<int, int>> FiniteAutomaton::merge_classes(
const vector<int>& classes) const {
map<int, vector<int>> class_to_indexes;
for (int i = 0; i < classes.size(); i++)
Expand Down Expand Up @@ -1398,7 +1398,7 @@ tuple<FiniteAutomaton, unordered_map<int, int>> FiniteAutomaton::merge_equivalen
return {{class_to_index.at(classes[initial_state]), new_states, language}, class_to_index};
}

vector<int> FiniteAutomaton::get_bisimilar_classes() const {
vector<int> FiniteAutomaton::get_bisimulation_classes() const {
vector<RLGrammar::Item> fa_items;
vector<RLGrammar::Item*> nonterminals;
vector<RLGrammar::Item*> terminals;
Expand All @@ -1418,8 +1418,8 @@ vector<int> FiniteAutomaton::get_bisimilar_classes() const {

FiniteAutomaton FiniteAutomaton::merge_bisimilar(iLogTemplate* log) const {
MetaInfo old_meta, new_meta;
vector<int> classes = get_bisimilar_classes();
auto [result, class_to_index] = merge_equivalent_classes(classes);
vector<int> classes = get_bisimulation_classes();
auto [result, class_to_index] = merge_classes(classes);

for (int i = 0; i < classes.size(); i++) {
for (int j = 0; j < classes.size(); j++)
Expand Down Expand Up @@ -1602,9 +1602,9 @@ bool FiniteAutomaton::equality_checker(const FiniteAutomaton& fa1, const FiniteA
if (t != 0)
return false;

vector<int> bisimilar_classes(nonterminals.size());
vector<int> bisimulation_classes(nonterminals.size());
for (int i = 0; i < nonterminals.size(); i++)
bisimilar_classes[i] = nonterminals[i]->class_number;
bisimulation_classes[i] = nonterminals[i]->class_number;

// биективная бисимуляция обратных грамматик
vector<vector<vector<RLGrammar::Item*>>> fa1_reverse_rules = RLGrammar::get_reverse_grammar(
Expand All @@ -1623,22 +1623,22 @@ bool FiniteAutomaton::equality_checker(const FiniteAutomaton& fa1, const FiniteA
RLGrammar::get_bisimilar_grammar(
reverse_rules, nonterminals, reverse_bisimilar_nonterminals, class_to_nonterminals);
// сопоставление состояний 1 к 1
vector<int> reverse_bisimilar_classes;
vector<int> reverse_bisimulation_classes;
for (RLGrammar::Item* nont : nonterminals) {
reverse_bisimilar_classes.push_back(nont->class_number);
reverse_bisimulation_classes.push_back(nont->class_number);
nont->class_number = -1;
}

// устанавливаем классы нетерминалов-состояний (1 к 1), чтобы после сопоставить переходы
int new_class = 0;
for (int i = 0; i < bisimilar_classes.size(); i++) {
for (int i = 0; i < bisimulation_classes.size(); i++) {
if (nonterminals[i]->class_number != -1)
continue;
nonterminals[i]->class_number = new_class;
// поиск нетерминалов с классом, как у i-го
for (int j = i + 1; j < bisimilar_classes.size(); j++) {
if (bisimilar_classes[j] == bisimilar_classes[i])
if (reverse_bisimilar_classes[j] == reverse_bisimilar_classes[i])
for (int j = i + 1; j < bisimulation_classes.size(); j++) {
if (bisimulation_classes[j] == bisimulation_classes[i])
if (reverse_bisimulation_classes[j] == reverse_bisimulation_classes[i])
nonterminals[j]->class_number = new_class;
}
new_class++;
Expand Down
16 changes: 11 additions & 5 deletions libs/Objects/src/MemoryCommon.cpp
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
#include "Objects/MemoryCommon.h"

using std::tuple;
using std::unordered_set;
using std::vector;

Expand Down Expand Up @@ -60,6 +61,10 @@ bool CaptureGroup::get_is_reset() const {
return is_reset;
}

bool CaptureGroup::get_cell_number() const {
return cell;
}

int CaptureGroup::get_opening_state_index() const {
return (*paths.begin())[0];
}
Expand All @@ -73,18 +78,19 @@ const unordered_set<CaptureGroup::State, CaptureGroup::State::Hasher>& CaptureGr
return states;
}

unordered_set<int> CaptureGroup::get_states_diff(const CaptureGroup& other) const {
tuple<unordered_set<int>, unordered_set<int>> CaptureGroup::get_states_diff(
const CaptureGroup& other) const {
unordered_set<int> diff;
for (auto st : states)
if (st.class_num != State::reset_class && !other.state_classes.count(st.class_num))
diff.insert(st.index);

unordered_set<int> res(diff);
unordered_set<int> following(diff);
for (const auto& path : paths)
for (size_t i = path.size() - 1; i > 0; i--)
if (diff.count(path[i - 1]))
res.insert(path[i]);
return res;
following.insert(path[i]);
return {diff, following};
}

std::ostream& operator<<(std::ostream& os, const CaptureGroup& cg) {
Expand All @@ -95,4 +101,4 @@ std::ostream& operator<<(std::ostream& os, const CaptureGroup& cg) {
for (const auto& i : cg.states)
os << "{" << i.index << ": " << i.class_num << "} ";
return os << "]\n";
}
}
67 changes: 39 additions & 28 deletions libs/Objects/src/MemoryFiniteAutomaton.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1062,7 +1062,7 @@ size_t TraversalState::Hasher::operator()(const TraversalState& s) const {
pair<unordered_set<string>, unordered_set<string>> MemoryFiniteAutomaton::generate_test_set(
int max_len) const {
unordered_set<string> words_in_language;
unordered_map<string, IntPairSet> words_to_mutate;
unordered_map<string, IntPairsSet> words_to_mutate;

unordered_set<TraversalState, TraversalState::Hasher> current_states;
current_states.insert(TraversalState(&states[initial_state]));
Expand Down Expand Up @@ -1383,6 +1383,11 @@ void find_opening_states_dfs(int state_index,
}
}

bool is_valid_transition(bool is_opening_state, optional<MFATransition::MemoryAction> action) {
bool is_open_action = action && action == MFATransition::open;
return is_opening_state == is_open_action;
}

pair<vector<vector<int>>, vector<vector<int>>> MemoryFiniteAutomaton::find_cg_paths(
int state_index, std::unordered_set<int> visited, int cell, int opening_state) const {
vector<vector<int>> paths;
Expand All @@ -1392,22 +1397,19 @@ pair<vector<vector<int>>, vector<vector<int>>> MemoryFiniteAutomaton::find_cg_pa
for (const auto& [symbol, symbol_transitions] : states[state_index].transitions)
for (const auto& tr : symbol_transitions) {
optional<MFATransition::MemoryAction> action;
if (tr.memory_actions.count(cell))
action = tr.memory_actions.at(cell);
if (auto it = tr.memory_actions.find(cell); it != tr.memory_actions.end())
action = it->second;
if (action && action == MFATransition::close) {
paths.push_back({state_index});
} else if (action && action == MFATransition::reset) {
reset_paths.push_back({state_index});
} else {
bool is_open_action = action && action == MFATransition::open;
bool is_opening_state = state_index == opening_state;
bool should_process = !visited.count(tr.to) ||
// чтобы обработать случай, когда открывающее совпадает с
// закрывающим, e.g. [a*a]:1*&1
(!is_opening_state && tr.to == opening_state);
bool is_valid_transition =
is_opening_state ? action && is_open_action : !is_open_action;
if (should_process && is_valid_transition) {
if (should_process && is_valid_transition(is_opening_state, action)) {
auto [t, _] = find_cg_paths(tr.to, visited, cell, opening_state);
for (auto& i : t) {
i.insert(i.begin(), state_index);
Expand Down Expand Up @@ -1440,15 +1442,24 @@ vector<CaptureGroup> MemoryFiniteAutomaton::find_capture_groups_backward(
return res;
}

bool MemoryFiniteAutomaton::find_decisions(int state_index, std::vector<int>& visited,
const std::unordered_set<int>& states_to_check) const {
bool MemoryFiniteAutomaton::find_decisions(int state_index, vector<int>& visited,
const unordered_set<int>& states_to_check,
const unordered_set<int>& following_states,
const CaptureGroup& cg) const {
visited[state_index] = 1;

optional<MFATransition> single_tr;
int count = 0;
for (const auto& [symbol, symbol_transitions] : states[state_index].transitions)
for (const auto& tr : symbol_transitions)
if (states_to_check.count(tr.to)) {
for (const auto& tr : symbol_transitions) {
optional<MFATransition::MemoryAction> action;
if (auto it = tr.memory_actions.find(cg.get_cell_number());
it != tr.memory_actions.end())
action = it->second;

if (is_valid_transition(state_index == cg.get_opening_state_index(), action) &&
(states_to_check.count(tr.to) || following_states.count(tr.to)) &&
!(following_states.count(state_index) && !states_to_check.count(tr.to))) {
if (visited[tr.to] == 0) {
if (++count > 1)
return true;
Expand All @@ -1457,22 +1468,24 @@ bool MemoryFiniteAutomaton::find_decisions(int state_index, std::vector<int>& vi
return true;
}
}
}

bool found = false;
if (single_tr)
found = find_decisions(single_tr->to, visited, states_to_check);
found = find_decisions(single_tr->to, visited, states_to_check, following_states, cg);

visited[state_index] = 2;
return found;
}

bool MemoryFiniteAutomaton::states_have_decisions(
const std::unordered_set<int>& states_to_check) const {
bool MemoryFiniteAutomaton::states_have_decisions(const unordered_set<int>& states_to_check,
const unordered_set<int>& following_states,
const CaptureGroup& cg) const {
vector<int> visited(size(), 0);
for (auto start : states_to_check) {
if (visited[start] != 0)
continue;
if (find_decisions(start, visited, states_to_check))
if (find_decisions(start, visited, states_to_check, following_states, cg))
return true;
}
return false;
Expand Down Expand Up @@ -1612,9 +1625,7 @@ optional<bool> MemoryFiniteAutomaton::bisimilarity_checker(const MemoryFiniteAut
for (auto color : mfa_colors[i][j])
if (!colors_to_ignore.count(color))
j_colors.insert(color);
if (!j_colors.empty())
colored_SCC.insert(
{ab_classes[i][j], set<int>(j_colors.begin(), j_colors.end())});
colored_SCC.insert({ab_classes[i][j], set<int>(j_colors.begin(), j_colors.end())});
}
if (!colored_SCC.empty())
colored_SCCs[i].insert(colored_SCC);
Expand Down Expand Up @@ -1647,8 +1658,8 @@ optional<bool> MemoryFiniteAutomaton::bisimilarity_checker(const MemoryFiniteAut
in_SCCs[i].insert(j);

vector<FiniteAutomaton> symbolic_fas({mfas[0]->to_symbolic_fa(), mfas[1]->to_symbolic_fa()});
vector<vector<int>> symbolic_classes = {symbolic_fas[0].get_bisimilar_classes(),
symbolic_fas[1].get_bisimilar_classes()};
vector<vector<int>> symbolic_classes = {symbolic_fas[0].get_bisimulation_classes(),
symbolic_fas[1].get_bisimulation_classes()};
#ifdef DEBUG
cout << ab_classes[0] << ab_classes[1];
cout << FiniteAutomaton::bisimilar(symbolic_fas[0], symbolic_fas[1]) << "\n";
Expand Down Expand Up @@ -1744,11 +1755,11 @@ optional<bool> MemoryFiniteAutomaton::bisimilarity_checker(const MemoryFiniteAut
for (int i = 0; i < CGs_0.size(); i++)
for (int j = 0; j < CGs_1.size(); j++) {
const auto &cg0 = CGs_0[i], cg1 = CGs_1[j];
unordered_set<int> states_to_check_0 = cg0.get_states_diff(cg1),
states_to_check_1 = cg1.get_states_diff(cg0);
auto [diff0, following0] = cg0.get_states_diff(cg1);
auto [diff1, following1] = cg1.get_states_diff(cg0);

if (!mfa1.states_have_decisions(states_to_check_0) &&
!mfa2.states_have_decisions(states_to_check_1)) {
if (!mfa1.states_have_decisions(diff0, following0, cg0) &&
!mfa2.states_have_decisions(diff1, following1, cg1)) {
check_set_0.insert(i);
check_set_1.insert(j);
}
Expand Down Expand Up @@ -1793,8 +1804,8 @@ optional<bool> MemoryFiniteAutomaton::bisimilar(const MemoryFiniteAutomaton& mfa
return result;
}

tuple<MemoryFiniteAutomaton, unordered_map<int, int>> MemoryFiniteAutomaton::
merge_equivalent_classes(const vector<int>& classes) const {
tuple<MemoryFiniteAutomaton, unordered_map<int, int>> MemoryFiniteAutomaton::merge_classes(
const vector<int>& classes) const {
map<int, vector<int>> class_to_indexes;
for (int i = 0; i < classes.size(); i++)
class_to_indexes[classes[i]].push_back(i);
Expand Down Expand Up @@ -1832,9 +1843,9 @@ tuple<MemoryFiniteAutomaton, unordered_map<int, int>> MemoryFiniteAutomaton::

MemoryFiniteAutomaton MemoryFiniteAutomaton::merge_bisimilar(iLogTemplate* log) const {
MetaInfo old_meta, new_meta;
vector<int> classes = to_symbolic_fa().get_bisimilar_classes();
vector<int> classes = to_symbolic_fa().get_bisimulation_classes();
classes.resize(size()); // в symbolic_fa первые size() состояний - состояния исходного mfa
auto [result, class_to_index] = merge_equivalent_classes(classes);
auto [result, class_to_index] = merge_classes(classes);

for (int i = 0; i < classes.size(); i++) {
for (int j = 0; j < classes.size(); j++)
Expand Down

0 comments on commit 968f233

Please sign in to comment.