diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 8c6ceab2c..1d706bf3b 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -428,31 +428,56 @@ Nft somewhat_simple_revert(const Nft& aut); Nft remove_epsilon(const Nft& aut, Symbol epsilon = EPSILON); /** - * @brief Projects out specified levels in the given automaton. + * @brief Projects out specified levels @p levels_to_project in the given transducer @p nft. * - * The vector levels_to_project must be a non-empty ordered vector - * containing only values that are greater than or equal to 0 and smaller than levels_cnt. + * @param nft The transducer for projection. + * @param levels_to_project A non-empty ordered vector of levels to be projected out from the transducer. It must + * contain only values that are greater than or equal to 0 and smaller than @c levels_cnt. + * @param repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1) + * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence + * of @p DONT_CARE symbols. + * @return A new projected transducer. + */ +Nft project_out(const Nft& nft, const utils::OrdVector& levels_to_project, bool repeat_jump_symbol = true); + +/** + * @brief Projects out specified level @p level_to_project in the given transducer @p nft. * - * @param aut The automaton for projection. - * @param levels_to_project A non-empty ordered vector of levels to be projected out from the automaton. + * @param nft The transducer for projection. + * @param level_to_project A level that is going to be projected out from the transducer. It has to be greater than or + * equal to 0 and smaller than @c levels_cnt. * @param repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1) - * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CAREs. - * @return A new automaton after the projection. + * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence + * of @c DONT_CARE symbols. + * @return A new projected transducer. */ -Nft project_out(const Nft& aut, const utils::OrdVector& levels_to_project, const bool repeat_jump_symbol = true); +Nft project_out(const Nft& nft, Level level_to_project, bool repeat_jump_symbol = true); /** - * @brief Projects out specified level in the given automaton. + * @brief Projects to specified levels @p levels_to_project in the given transducer @p nft. * - * The level level_to_project has to be greater or equal than 0 and smaller than levels_cnt. + * @param nft The transducer for projection. + * @param levels_to_project A non-empty ordered vector of levels the transducer is going to be projected to. + * It must contain only values greater than or equal to 0 and smaller than @c levels_cnt. + * @param repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1) + * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence + * of @c DONT_CARE symbols. + * @return A new projected transducer. + */ +Nft project_to(const Nft& nft, const utils::OrdVector& levels_to_project, bool repeat_jump_symbol = true); + +/** + * @brief Projects to a specified level @p level_to_project in the given transducer @p nft. * - * @param aut The automaton for projection. - * @param level_to_project A level that is going to be projected out from the automaton. + * @param nft The transducer for projection. + * @param level_to_project A level the transducer is going to be projected to. It has to be greater than or equal to 0 + * and smaller than @c levels_cnt. * @param repeat_jump_symbol Specifies if the symbol on a jump transition (a transition with a length greater than 1) - * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CAREs. - * @return A new automaton after the projection. + * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence + * of @c DONT_CARE symbols. + * @return A new projectedtransducer. */ -Nft project_out(const Nft& aut, const Level level_to_project, const bool repeat_jump_symbol = true); +Nft project_to(const Nft& nft, Level level_to_project, bool repeat_jump_symbol = true); /** Encodes a vector of strings (each corresponding to one symbol) into a * @c Word instance diff --git a/src/nft/operations.cc b/src/nft/operations.cc index 790b0958b..3c9c3e704 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -176,20 +176,20 @@ Nft mata::nft::remove_epsilon(const Nft& aut, Symbol epsilon) { return result; } -Nft mata::nft::project_out(const Nft& aut, const utils::OrdVector& levels_to_proj, const bool repeat_jump_symbol) { - assert(!levels_to_proj.empty()); - assert(*std::max_element(levels_to_proj.begin(), levels_to_proj.end()) < aut.levels_cnt); +Nft mata::nft::project_out(const Nft& nft, const utils::OrdVector& levels_to_project, const bool repeat_jump_symbol) { + assert(!levels_to_project.empty()); + assert(*std::max_element(levels_to_project.begin(), levels_to_project.end()) < nft.levels_cnt); - // Checks if a given state is being projected out based on the levels_to_proj vector. + // Checks if a given state is being projected out based on the levels_to_project vector. auto is_projected_out = [&](State s) { - return levels_to_proj.find(aut.levels[s]) != levels_to_proj.end(); + return levels_to_project.find(nft.levels[s]) != levels_to_project.end(); }; // Checks if each level between given states is being projected out. auto is_projected_along_path = [&](State src, State tgt) { - Level stop_lvl = (aut.levels[tgt] == 0) ? aut.levels_cnt : aut.levels[tgt]; - for (Level lvl{ aut.levels[src] }; lvl < stop_lvl; lvl++) { - if (levels_to_proj.find(lvl) == levels_to_proj.end()) { + Level stop_lvl = (nft.levels[tgt] == 0) ? nft.levels_cnt : nft.levels[tgt]; + for (Level lvl{ nft.levels[src] }; lvl < stop_lvl; lvl++) { + if (levels_to_project.find(lvl) == levels_to_project.end()) { return false; } } @@ -198,29 +198,29 @@ Nft mata::nft::project_out(const Nft& aut, const utils::OrdVector& levels // Determines the transition length between two states based on their levels. auto get_trans_len = [&](State src, State tgt) { - return (aut.levels[src] == 0) ? (aut.levels_cnt - aut.levels[src]) : (aut.levels[tgt] - aut.levels[src]); + return (nft.levels[src] == 0) ? (nft.levels_cnt - nft.levels[src]) : (nft.levels[tgt] - nft.levels[src]); }; // Returns one-state automaton it the case of projecting all levels. - if (aut.levels_cnt == levels_to_proj.size()) { - if (aut.is_lang_empty()) { + if (nft.levels_cnt == levels_to_project.size()) { + if (nft.is_lang_empty()) { return Nft(1, {0}, {}, {}, 0); } return Nft(1, {0}, {0}, {}, 0); } // Calculates the smallest level 0 < k < levels_cnt that starts a consecutive ascending sequence - // of levels k, k+1, k+2, ..., levels_cnt-1 in the ordered-vector levels_to_proj. + // of levels k, k+1, k+2, ..., levels_cnt-1 in the ordered-vector levels_to_project. // If there is no such sequence, then k == levels_cnt. - size_t seq_start_idx = aut.levels_cnt; - const std::vector levels_to_proj_v = levels_to_proj.ToVector(); + size_t seq_start_idx = nft.levels_cnt; + const std::vector levels_to_proj_v = levels_to_project.ToVector(); for (auto levels_to_proj_v_revit = levels_to_proj_v.rbegin(); levels_to_proj_v_revit != levels_to_proj_v.rend() && *levels_to_proj_v_revit == seq_start_idx - 1; ++levels_to_proj_v_revit, --seq_start_idx); // Only states whose level is part of the sequence (will have level 0) can additionally be marked as final. auto can_be_final = [&](State s) { - return seq_start_idx <= aut.levels[s]; + return seq_start_idx <= nft.levels[s]; }; // Builds a vector of size levels_cnt. Each index k contains a new level for level k. @@ -229,7 +229,7 @@ Nft mata::nft::project_out(const Nft& aut, const utils::OrdVector& levels // old levels 0 1 2 3 4 5 6 // project out x x x x // new levels 0 0 1 2 2 0 0 - std::vector new_levels(aut.levels_cnt , 0); + std::vector new_levels(nft.levels_cnt , 0); Level lvl_sub{ 0 }; for (Level lvl_old{ 0 }; lvl_old < seq_start_idx; lvl_old++) { new_levels[lvl_old] = static_cast(lvl_old - lvl_sub); @@ -238,7 +238,7 @@ Nft mata::nft::project_out(const Nft& aut, const utils::OrdVector& levels } // cannot use multimap, because it can contain multiple occurrences of (a -> a), (a -> a) - const size_t num_of_states_in_delta{ aut.delta.num_of_states() }; + const size_t num_of_states_in_delta{ nft.delta.num_of_states() }; std::vector closure = std::vector(num_of_states_in_delta, OrdVector());; // TODO: Evaluate efficiency. This might not be as inefficient as the remove_epsilon closure. @@ -249,7 +249,7 @@ Nft mata::nft::project_out(const Nft& aut, const utils::OrdVector& levels if (!is_projected_out(source)) { continue; } - for (const auto& trans: aut.delta[source]) + for (const auto& trans: nft.delta[source]) { for (const auto& target : trans.targets) { if (is_projected_along_path(source, target)) { @@ -282,11 +282,11 @@ Nft mata::nft::project_out(const Nft& aut, const utils::OrdVector& levels } // Construct the automaton with projected levels. - Nft result{ Delta{}, aut.initial, aut.final, aut.levels, aut.levels_cnt, aut.alphabet }; + Nft result{ Delta{}, nft.initial, nft.final, nft.levels, nft.levels_cnt, nft.alphabet }; for (State src_state{ 0 }; src_state < num_of_states_in_delta; src_state++) { // For every state. for (State cls_state : closure[src_state]) { // For every state in its epsilon closure. - if (aut.final[cls_state] && can_be_final(src_state)) result.final.insert(src_state); - for (const SymbolPost& move : aut.delta[cls_state]) { + if (nft.final[cls_state] && can_be_final(src_state)) result.final.insert(src_state); + for (const SymbolPost& move : nft.delta[cls_state]) { // TODO: this could be done more efficiently if we had a better add method for (State tgt_state : move.targets) { bool is_loop_on_target = cls_state == tgt_state; @@ -320,13 +320,26 @@ Nft mata::nft::project_out(const Nft& aut, const utils::OrdVector& levels for (State s{ 0 }; s < result.levels.size(); s++) { result.levels[s] = new_levels[result.levels[s]]; } - result.levels_cnt = static_cast(result.levels_cnt - levels_to_proj.size()); + result.levels_cnt = static_cast(result.levels_cnt - levels_to_project.size()); return result; } -Nft mata::nft::project_out(const Nft& aut, const Level level_to_project, const bool repeat_jump_symbol) { - return project_out(aut, utils::OrdVector{ level_to_project }, repeat_jump_symbol); +Nft mata::nft::project_out(const Nft& nft, const Level level_to_project, const bool repeat_jump_symbol) { + return project_out(nft, utils::OrdVector{ level_to_project }, repeat_jump_symbol); +} + +Nft mata::nft::project_to(const Nft& nft, const OrdVector& levels_to_project, const bool repeat_jump_symbol) { + OrdVector all_levels{ OrdVector::with_reserved(nft.levels_cnt) }; + for (Level level{ 0 }; level < nft.levels_cnt; ++level) { all_levels.push_back(level); } + OrdVector levels_to_project_out{ OrdVector::with_reserved(nft.levels_cnt) }; + std::set_difference(all_levels.begin(), all_levels.end(), levels_to_project.begin(), + levels_to_project.end(), std::back_inserter(levels_to_project_out) ); + return project_out(nft, levels_to_project_out, repeat_jump_symbol); +} + +Nft mata::nft::project_to(const Nft& nft, Level level_to_project, const bool repeat_jump_symbol) { + return project_to(nft, OrdVector{ level_to_project }, repeat_jump_symbol); } Nft mata::nft::fragile_revert(const Nft& aut) { diff --git a/tests/nft/nft.cc b/tests/nft/nft.cc index 01925cf7f..4c5f72c80 100644 --- a/tests/nft/nft.cc +++ b/tests/nft/nft.cc @@ -3157,7 +3157,7 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = false)") { Nft atm(delta, { 0 }, { 3 }, { 0, 1, 2, 0 }, 3); SECTION("project 0") { - Nft proj0 = project_out(atm, 0, false); + Nft proj0 = project_out(atm, OrdVector{ 0 }, false); Nft proj0_expected(3, { 0 }, { 2 }, { 0, 1, 0 }, 2); proj0_expected.delta.add(0, 1, 1); proj0_expected.delta.add(1, 2, 2); @@ -3238,10 +3238,10 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = false)") { delta.add(0, 3, 3); delta.add(3, 4, 2); - Nft atm_complex(delta, { 0 }, { 3 }, { 0, 1, 2, 0 }, 3); + Nft nft_complex(delta, { 0 }, { 3 }, { 0, 1, 2, 0 }, 3); SECTION("project 0") { - Nft proj0_complex = project_out(atm_complex, 0, false); + Nft proj0_complex = project_out(nft_complex, 0, false); Nft proj0_complex_expected(3, { 0 }, { 2 }, { 0, 1, 0 }, 2); proj0_complex_expected.delta.add(0, 1, 1); proj0_complex_expected.delta.add(0, DONT_CARE, 2); @@ -3251,7 +3251,7 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = false)") { } SECTION("project 1") { - Nft proj1_complex = project_out(atm_complex, 1, false); + Nft proj1_complex = project_out(nft_complex, 1, false); Nft proj1_complex_expected(3, { 0 }, { 2 }, { 0, 1, 0 }, 2); proj1_complex_expected.delta.add(0, 0, 1); proj1_complex_expected.delta.add(0, 3, 2); @@ -3261,17 +3261,26 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = false)") { } SECTION("project 2") { - Nft proj2_complex = project_out(atm_complex, 2, false); + Nft proj2_complex = project_out(nft_complex, OrdVector{ 2 }, false); Nft proj2_complex_expected(3, { 0 }, { 2 }, { 0, 1, 0 }, 2); proj2_complex_expected.delta.add(0, 0, 1); proj2_complex_expected.delta.add(0, 3, 2); proj2_complex_expected.delta.add(1, 1, 2); proj2_complex_expected.delta.add(2, 4, 2); CHECK(are_equivalent(proj2_complex, proj2_complex_expected)); + + proj2_complex = project_to(nft_complex, OrdVector{ 2 }); + proj2_complex_expected = Nft(2, { 0 }, { 1 }, { 0, 0 }, 1); + proj2_complex_expected.delta.add(0, 2, 1); + proj2_complex_expected.delta.add(0, 3, 1); + proj2_complex_expected.delta.add(1, 2, 1); + CHECK(are_equivalent(proj2_complex, proj2_complex_expected)); + proj2_complex_expected.delta.add(0, 0, 1); + CHECK(!are_equivalent(proj2_complex, proj2_complex_expected)); } SECTION("project 0, 1") { - Nft proj01_complex = project_out(atm_complex, { 0, 1 }, false); + Nft proj01_complex = project_out(nft_complex, { 0, 1 }, false); Nft proj01_complex_expected(2, { 0 }, { 1 }, { 0, 0 }, 1); proj01_complex_expected.delta.add(0, 2, 1); proj01_complex_expected.delta.add(0, DONT_CARE, 1); @@ -3280,7 +3289,7 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = false)") { } SECTION("project 0, 2") { - Nft proj02_complex = project_out(atm_complex, { 0, 2 }, false); + Nft proj02_complex = project_out(nft_complex, { 0, 2 }, false); Nft proj02_complex_expected(2, { 0 }, { 1 }, { 0, 0 }, 1); proj02_complex_expected.delta.add(0, 1, 1); proj02_complex_expected.delta.add(0, DONT_CARE, 1); @@ -3289,7 +3298,7 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = false)") { } SECTION("project 1, 2") { - Nft proj12_complex = project_out(atm_complex, { 1, 2 }, false); + Nft proj12_complex = project_out(nft_complex, { 1, 2 }, false); Nft proj12_complex_expected(2, { 0 }, { 1 }, { 0, 0 }, 1); proj12_complex_expected.delta.add(0, 0, 1); proj12_complex_expected.delta.add(0, 3, 1); @@ -3298,7 +3307,7 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = false)") { } SECTION("project 0, 1, 2") { - Nft proj012_complex = project_out(atm_complex, { 0, 1, 2 }, false); + Nft proj012_complex = project_out(nft_complex, { 0, 1, 2 }, false); Nft proj012_complex_expected(1, { 0 }, { 0 }, {}, 0); CHECK(are_equivalent(proj012_complex, proj012_complex_expected)); } @@ -3521,3 +3530,130 @@ TEST_CASE("mata::nft::project_out(repeat_jump_symbol = true)") { CHECK(are_equivalent(proj_hard, proj_hard_expected)); } } + +TEST_CASE("mata::nft::project_to()") { + Nft nft; + Nft projection; + Nft expected; + + SECTION("linear") { + nft = Nft{ {}, { 0 }, { 3 }, { 0, 1, 2, 0 }, 3 }; + nft.delta.add(0, 0, 1); + nft.delta.add(1, 1, 2); + nft.delta.add(2, 2, 3); + projection = project_to(nft, 2); + expected = Nft{ 2, { 0 }, { 1 }, { 0, 0 }, 1 }; + expected.delta.add(0, 2, 1); + CHECK(nft::are_equivalent(projection, expected)); + } + + SECTION("linear longer") { + nft = Nft{ {}, { 0 }, { 6 }, { 0, 1, 2, 0, 1, 2, 0 }, 3 }; + nft.delta.add(0, 0, 1); + nft.delta.add(1, 1, 2); + nft.delta.add(2, 2, 3); + nft.delta.add(3, 3, 4); + nft.delta.add(4, 4, 5); + nft.delta.add(5, 5, 6); + projection = project_to(nft, 2); + expected = Nft{ {}, { 0 }, { 2 }, { 0, 0, 0 }, 1 }; + expected.delta.add(0, 2, 1); + expected.delta.add(1, 5, 2); + CHECK(nft::are_equivalent(projection, expected)); + } + + SECTION("linear longer symbol long jump") { + nft = Nft{ {}, { 0 }, { 6 }, { 0, 1, 2, 0, 1, 2, 0 }, 3 }; + nft.delta.add(0, 0, 1); + nft.delta.add(1, 1, 2); + nft.delta.add(2, 2, 3); + nft.delta.add(3, 3, 4); + nft.delta.add(4, 4, 5); + nft.delta.add(5, 5, 6); + nft.delta.add(0, 'j', 6); + projection = project_to(nft, 2); + expected = Nft{ {}, { 0 }, { 2 }, { 0, 0, 0 }, 1 }; + expected.delta.add(0, 2, 1); + expected.delta.add(1, 5, 2); + expected.delta.add(0, 'j', 2); + CHECK(nft::are_equivalent(projection, expected)); + expected.delta.add(0, 'b', 2); + CHECK(!nft::are_equivalent(projection, expected)); + } + + SECTION("cycle longer") { + nft = Nft{ {}, { 0 }, { 6 }, { 0, 1, 2, 0, 1, 2, 0, 1, 2, 1, 2 }, 3 }; + nft.delta.add(0, 0, 1); + nft.delta.add(1, 1, 2); + nft.delta.add(2, 2, 3); + nft.delta.add(3, 3, 4); + nft.delta.add(4, 4, 5); + nft.delta.add(5, 5, 6); + nft.delta.add(3, 6, 7); + nft.delta.add(7, 7, 8); + nft.delta.add(8, 8, 0); + nft.delta.add(6, 9, 9); + nft.delta.add(9, 9, 10); + nft.delta.add(10, 10, 0); + projection = project_to(nft, 2); + expected = Nft{ {}, { 0 }, { 2 }, { 0, 0, 0 }, 1 }; + expected.delta.add(0, 2, 1); + expected.delta.add(1, 8, 0); + expected.delta.add(1, 5, 2); + expected.delta.add(2, 10, 0); + CHECK(nft::are_equivalent(projection, expected)); + } + + SECTION("cycle longer project to { 0, 2 }") { + nft = Nft{ {}, { 0 }, { 6 }, { 0, 1, 2, 0, 1, 2, 0, 1, 2, 1, 2 }, 3 }; + nft.delta.add(0, 0, 1); + nft.delta.add(1, 1, 2); + nft.delta.add(2, 2, 3); + nft.delta.add(3, 3, 4); + nft.delta.add(4, 4, 5); + nft.delta.add(5, 5, 6); + nft.delta.add(3, 6, 7); + nft.delta.add(7, 7, 8); + nft.delta.add(8, 8, 0); + nft.delta.add(6, 9, 9); + nft.delta.add(9, 9, 10); + nft.delta.add(10, 10, 0); + projection = project_to(nft, { 0, 2 }); + expected = Nft{ {}, { 0 }, { 6 }, { 0, 1, 0, 1, 0, 1, 0 }, 2 }; + expected.delta.add(0, 0, 1); + expected.delta.add(1, 2, 3); + expected.delta.add(3, 6, 4); + expected.delta.add(3, 3, 5); + expected.delta.add(4, 8, 0); + expected.delta.add(5, 5, 6); + expected.delta.add(6, 9, 7); + expected.delta.add(7, 10, 0); + CHECK(nft::are_equivalent(projection, expected)); + } + + SECTION("cycle longer project to { 0, 2 } with epsilon and dont care symbols") { + nft = Nft{ {}, { 0 }, { 6 }, { 0, 1, 2, 0, 1, 2, 0, 1, 2, 1, 2 }, 3 }; + nft.delta.add(0, EPSILON, 2); + nft.delta.add(2, 2, 3); + nft.delta.add(3, 3, 4); + nft.delta.add(4, 4, 5); + nft.delta.add(5, 5, 6); + nft.delta.add(3, EPSILON, 7); + nft.delta.add(7, 7, 8); + nft.delta.add(8, DONT_CARE, 0); + nft.delta.add(6, 9, 9); + nft.delta.add(9, 10, 10); + nft.delta.add(10, 11, 0); + projection = project_to(nft, { 0, 2 }); + expected = Nft{ {}, { 0 }, { 6 }, { 0, 1, 0, 0, 1, 1, 0, 1 }, 2 }; + expected.delta.add(0, EPSILON, 1); + expected.delta.add(1, 2, 3); + expected.delta.add(3, EPSILON, 4); + expected.delta.add(3, 3, 5); + expected.delta.add(4, DONT_CARE, 0); + expected.delta.add(5, 5, 6); + expected.delta.add(6, 9, 7); + expected.delta.add(7, 11, 0); + CHECK(nft::are_equivalent(projection, expected)); + } +}