Skip to content

Commit

Permalink
Optimization of invert_levels for JumpMode::AppendDontcareSymbols (…
Browse files Browse the repository at this point in the history 
…#486) #patch
  • Loading branch information
@koniksedy
koniksedy authored Feb 14, 2025
1 parent 2622bfa commit 9bc5557
Show file tree
Hide file tree
Showing 2 changed files with 148 additions and 22 deletions.
53 changes: 32 additions & 21 deletions src/nft/operations.cc
View file
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
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

0 comments on commit 9bc5557

Please sign in to comment.