Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Optimization of invert_levels for JumpMode::AppendDontcareSymbols #486

Merged
merged 3 commits into from
Feb 14, 2025
Merged

Optimization of invert_levels for JumpMode::AppendDontcareSymbols #486

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
cbd59d4
optimization for JumpMode::AppendDontcareSymbols
koniksedy Feb 11, 2025
068b731
typo and trg -> tgt
koniksedy Feb 11, 2025
368d195
add static_cast<Level>
koniksedy Feb 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 32 additions & 21 deletions src/nft/operations.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -715,8 +715,8 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
std::vector<Transition> path_transitions;
for (size_t i = 0; i < path_states.size() - 1; ++i) {
const State src = path_states[i];
const State trg = path_states[i + 1];
std::vector<Transition> transitions_between = aut.delta.get_transitions_between(src, trg);
const State tgt = path_states[i + 1];
std::vector<Transition> transitions_between = aut.delta.get_transitions_between(src, tgt);
path_transitions.insert(path_transitions.end(), transitions_between.begin(), transitions_between.end());
}

Expand All @@ -726,35 +726,46 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
// Creates inverted transitions for each transition in the path.
// Can work with different jump modes.
auto map_inverted_transitions = [&](const std::vector<Transition>& path, const State head, const State tail) {
for (const auto &[src, symbol, trg]: path) {
// Auxiliary state between two states can be reused for transitions over different symbols.
// The key is a pair of source and target states.
// auxiliary_states map will be used only if the jump_mode is JumpMode::AppendDontCares.
std::unordered_map<std::pair<State, State>, State> auxiliary_states;
auto get_aux_state = [&](const State src, const State tgt, const Level level) {
const std::pair<State, State> key{ src, tgt };
if (auxiliary_states.find(key) == auxiliary_states.end()) {
auxiliary_states[key] = aut_inv.add_state_with_level(level);
}
return auxiliary_states[key];
};
for (const auto &[src, symbol, tgt]: path) {
const bool is_src_head = src == head;
const bool is_trg_tail = trg == tail;
if (is_src_head && is_trg_tail) {
const bool is_tgt_tail = tgt == tail;
if (is_src_head && is_tgt_tail) {
// It is a direct transition between two zero-states (the head and the tail).
// Just copy it.
if (jump_mode == JumpMode::AppendDontCares && aut.num_of_levels > 1) {
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut.num_of_levels - 1));
const State aux_state = get_aux_state(src, tgt, static_cast<Level>(aut.num_of_levels - 1));
aut_inv.delta.add(renaming[src], DONT_CARE, aux_state);
aut_inv.delta.add(aux_state, symbol, renaming[trg]);
aut_inv.delta.add(aux_state, symbol, renaming[tgt]);
} else {
aut_inv.delta.add(renaming[src], symbol, renaming[trg]);
aut_inv.delta.add(renaming[src], symbol, renaming[tgt]);
}
} else if (is_src_head) {
// It is a transition from a zero-state (head) to a nonzero-state (inner state).
// Map it as transition from that nonzero-state (inner state) to the tail (zero-states).
if (jump_mode == JumpMode::AppendDontCares && aut.levels[trg] > 1) {
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut.num_of_levels - 1));
aut_inv.delta.add(renaming[trg], DONT_CARE, aux_state);
if (jump_mode == JumpMode::AppendDontCares && aut.levels[tgt] > 1) {
const State aux_state = get_aux_state(src, tgt, static_cast<Level>(aut.num_of_levels - 1));
aut_inv.delta.add(renaming[tgt], DONT_CARE, aux_state);
aut_inv.delta.add(aux_state, symbol, renaming[tail]);
} else {
aut_inv.delta.add(renaming[trg], symbol, renaming[tail]);
aut_inv.delta.add(renaming[tgt], symbol, renaming[tail]);
}

} else if (is_trg_tail) {
} else if (is_tgt_tail) {
// It is a transition from a nonzero-state (inner state) to a zero-state (tail).
// Map it as transition from the zero-state (head) to that nonzero-state (inner state).
if (jump_mode == JumpMode::AppendDontCares && (aut.num_of_levels - aut.levels[src]) > 1) {
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
const State aux_state = get_aux_state(src, tgt, static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
aut_inv.delta.add(renaming[head], DONT_CARE, aux_state);
aut_inv.delta.add(aux_state, symbol, renaming[src]);
} else {
Expand All @@ -763,12 +774,12 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
} else {
// It is a transition between two nonzero-states (inner states).
// Just swap the source and target.
if (jump_mode == JumpMode::AppendDontCares && (aut.levels[trg] - aut.levels[src]) > 1) {
const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
aut_inv.delta.add(renaming[trg], DONT_CARE, aux_state);
if (jump_mode == JumpMode::AppendDontCares && (aut.levels[tgt] - aut.levels[src]) > 1) {
const State aux_state = get_aux_state(src, tgt, static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
aut_inv.delta.add(renaming[tgt], DONT_CARE, aux_state);
aut_inv.delta.add(aux_state, symbol, renaming[src]);
} else {
aut_inv.delta.add(renaming[trg], symbol, renaming[src]);
aut_inv.delta.add(renaming[tgt], symbol, renaming[src]);
}
}
}
Expand All @@ -795,11 +806,11 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
continue;
}

for (const State trg: aut.delta[src].get_successors()) {
for (const State tgt: aut.delta[src].get_successors()) {
// Extend the path.
std::vector<State> new_path = path;
new_path.push_back(trg);
stack.push({ trg, std::move(new_path) });
new_path.push_back(tgt);
stack.push({ tgt, std::move(new_path) });
}
}
}
Expand Down
117 changes: 116 additions & 1 deletion tests/nft/nft.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1853,7 +1853,93 @@ TEST_CASE("mata::nft::Levels") {
}

TEST_CASE("mata::nft::Nft::invert_levels()") {
SECTION("jump_mpde == RepeatSymbol") {
SECTION("Simple 2 level tests") {
SECTION("Linear") {
Nft aut(3);
aut.initial.insert(0);
aut.final.insert(2);
aut.num_of_levels = 2;
aut.levels = { 0, 1, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(0, 'b', 1);
aut.delta.add(1, 'c', 2);
aut.delta.add(1, 'd', 2);
Nft aut_new = invert_levels(aut);

Nft expected = Nft(3);
expected.initial.insert(0);
expected.final.insert(2);
expected.num_of_levels = 2;
expected.levels = { 0, 1, 0 };
expected.delta.add(0, 'c', 1);
expected.delta.add(0, 'd', 1);
expected.delta.add(1, 'a', 2);
expected.delta.add(1, 'b', 2);

CHECK(aut_new.num_of_states() <= 3);
CHECK(aut_new.delta.num_of_transitions() <= 4);
CHECK(are_equivalent(aut_new, expected));
CHECK(are_equivalent(invert_levels(aut_new), aut));
}

SECTION("Diamond") {
Nft aut(4);
aut.initial.insert(0);
aut.final.insert(3);
aut.num_of_levels = 2;
aut.levels = { 0, 1, 1, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(0, 'b', 2);
aut.delta.add(1, 'c', 3);
aut.delta.add(2, 'd', 3);
Nft aut_new = invert_levels(aut);

Nft expected = Nft(4);
expected.initial.insert(0);
expected.final.insert(3);
expected.num_of_levels = 2;
expected.levels = { 0, 1, 1, 0 };
expected.delta.add(0, 'c', 1);
expected.delta.add(0, 'd', 2);
expected.delta.add(1, 'a', 3);
expected.delta.add(2, 'b', 3);

CHECK(aut_new.num_of_states() <= 4);
CHECK(aut_new.delta.num_of_transitions() <= 4);
CHECK(are_equivalent(aut_new, expected));
CHECK(are_equivalent(invert_levels(aut_new), aut));
}

SECTION("Branching") {
Nft aut(4);
aut.initial.insert(0);
aut.final.insert(3);
aut.num_of_levels = 2;
aut.levels = { 0, 1, 0, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(1, 'b', 2);
aut.delta.add(1, 'c', 3);
Nft aut_new = invert_levels(aut);

Nft expected = Nft(5);
expected.initial.insert(0);
expected.final.insert(4);
expected.final.insert(5);
expected.num_of_levels = 2;
expected.levels = { 0, 1, 1, 0, 0 };
expected.delta.add(0, 'b', 1);
expected.delta.add(0, 'c', 2);
expected.delta.add(1, 'a', 3);
expected.delta.add(2, 'a', 4);

CHECK(aut_new.num_of_states() <= 5);
CHECK(aut_new.delta.num_of_transitions() <= 4);
CHECK(are_equivalent(aut_new, expected));
CHECK(are_equivalent(invert_levels(aut_new), aut));
}
}

SECTION("jump_mode == RepeatSymbol") {
SECTION("empty automaton") {
Nft aut;
Nft aut_new = invert_levels(aut);
Expand Down Expand Up @@ -2151,6 +2237,35 @@ TEST_CASE("mata::nft::Nft::invert_levels()") {
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Linear + long jump - 4 levels, multiple symbols") {
Nft aut(2);
aut.initial.insert(0);
aut.final.insert(1);
aut.num_of_levels = 4;
aut.levels = { 0, 0 };
aut.delta.add(0, 'a', 1);
aut.delta.add(0, 'b', 1);
aut.delta.add(0, 'c', 1);
aut.delta.add(0, 'd', 1);
Nft aut_new = invert_levels(aut, JumpMode::AppendDontCares);

Nft expected = Nft(3);
expected.initial.insert(0);
expected.final.insert(2);
expected.num_of_levels = 4;
expected.levels = { 0, 3, 0 };
expected.delta.add(0, DONT_CARE, 1);
expected.delta.add(1, 'a', 2);
expected.delta.add(1, 'b', 2);
expected.delta.add(1, 'c', 2);
expected.delta.add(1, 'd', 2);

CHECK(aut_new.num_of_states() <= 3);
CHECK(aut_new.delta.num_of_transitions() <= 5);
CHECK(are_equivalent(aut_new, expected, JumpMode::AppendDontCares));
CHECK(are_equivalent(invert_levels(aut_new, JumpMode::AppendDontCares), aut, JumpMode::AppendDontCares));
}

SECTION("Linear + long jump - 3 levels") {
Nft aut(4);
aut.initial.insert(0);
Expand Down
Loading