diff --git a/src/nft/operations.cc b/src/nft/operations.cc index f5b8fe93..15ce1ca4 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -715,8 +715,8 @@ Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) { std::vector 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 transitions_between = aut.delta.get_transitions_between(src, trg); + const State tgt = path_states[i + 1]; + std::vector transitions_between = aut.delta.get_transitions_between(src, tgt); path_transitions.insert(path_transitions.end(), transitions_between.begin(), transitions_between.end()); } @@ -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& 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, State> auxiliary_states; + auto get_aux_state = [&](const State src, const State tgt, const Level level) { + const std::pair 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(aut.num_of_levels - 1)); + const State aux_state = get_aux_state(src, tgt, static_cast(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(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(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(aut_inv.levels[renaming[src]] - 1)); + const State aux_state = get_aux_state(src, tgt, static_cast(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 { @@ -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(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(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]); } } } @@ -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 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) }); } } } diff --git a/tests/nft/nft.cc b/tests/nft/nft.cc index c637e495..5c160c16 100644 --- a/tests/nft/nft.cc +++ b/tests/nft/nft.cc @@ -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); @@ -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);