Skip to content

Commit

Permalink
typo and trg -> tgt
Browse files Browse the repository at this point in the history
  • Loading branch information
@koniksedy
koniksedy committed Feb 11, 2025
1 parent cbd59d4 commit 068b731
Showing 1 changed file with 28 additions and 28 deletions.
56 changes: 28 additions & 28 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 @@ -728,44 +728,44 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
auto map_inverted_transitions = [&](const std::vector<Transition>& path, const State head, const State tail) {
// Auxiliary state between two states can be reused for transitions over different symbols.
// The key is a pair of source and target states.
// auxiliar_states map will be used only if the jump_mode is JumpMode::AppendDontCares.
std::unordered_map<std::pair<State, State>, State> auxiliar_states;
auto get_aux_state = [&](const State src, const State trg, const size_t level) {
const std::pair<State, State> key{ src, trg };
if (auxiliar_states.find(key) == auxiliar_states.end()) {
auxiliar_states[key] = aut_inv.add_state_with_level(static_cast<Level>(level));
// 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 size_t 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(static_cast<Level>(level));
}
return auxiliar_states[key];
return auxiliary_states[key];
};
for (const auto &[src, symbol, trg]: path) {
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 = get_aux_state(src, trg, aut.num_of_levels - 1);
const State aux_state = get_aux_state(src, tgt, 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 = get_aux_state(src, trg, 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, 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 = get_aux_state(src, trg, aut_inv.levels[renaming[src]] - 1);
const State aux_state = get_aux_state(src, tgt, 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 @@ -774,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 = get_aux_state(src, trg, 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, 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 @@ -806,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

0 comments on commit 068b731

Please sign in to comment.