diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 32f0d431f..1d706bf3b 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -428,34 +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 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 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 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 @p DONT_CARE symbols. + * @return A new projected transducer. */ -Nft project_out(const Nft& aut, const utils::OrdVector& levels_to_project, bool repeat_jump_symbol = true); +Nft project_out(const Nft& nft, const utils::OrdVector& levels_to_project, bool repeat_jump_symbol = true); /** - * @brief Projects out specified level in the given automaton. + * @brief Projects out specified level @p level_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 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 @c DONT_CARE symbols. + * @return A new projected transducer. + */ +Nft project_out(const Nft& nft, Level level_to_project, bool repeat_jump_symbol = true); + +/** + * @brief Projects to specified levels @p levels_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 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 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, Level level_to_project, bool repeat_jump_symbol = true); +Nft project_to(const Nft& nft, const utils::OrdVector& levels_to_project, bool repeat_jump_symbol = true); -Nft project_to(const Nft& nft, const utils::OrdVector& levels_to_project_to, bool repeat_jump_symbol = true); -Nft project_to(const Nft& nft, Level level_to_project_to, bool repeat_jump_symbol = true); +/** + * @brief Projects to a specified level @p level_to_project in the given transducer @p nft. + * + * @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 @c DONT_CARE symbols. + * @return A new projectedtransducer. + */ +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 b8db0b8a4..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,26 +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_to, const bool 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{ OrdVector::with_reserved(nft.levels_cnt) }; - std::set_difference(all_levels.begin(), all_levels.end(), levels_to_project_to.begin(), - levels_to_project_to.end(), std::back_inserter(levels_to_project) ); - return project_out(nft, levels_to_project, repeat_jump_symbol); + 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_to, const bool repeat_jump_symbol) { - return project_to(nft, OrdVector{ level_to_project_to }, 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) {