From b984372c8c2ea01583586c34bf035c7037e5c89a Mon Sep 17 00:00:00 2001 From: koniksedy Date: Wed, 15 Jul 2026 10:36:28 +0200 Subject: [PATCH 01/10] nft::is_in_lang using post --- include/mata/nft/nft.hh | 161 +++++++++++++++++++- src/nft/nft.cc | 230 +++++++++++++++++++++++++++++ src/nft/operations.cc | 121 +-------------- tests/nft/nft-post.cc | 316 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 714 insertions(+), 114 deletions(-) create mode 100644 tests/nft/nft-post.cc diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 7d1145df4..b0af86990 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -649,6 +649,7 @@ public: /** * @brief Get the set of states reachable from the given state over the given symbol. + * Note: It treats the transitions as NFA transitions, i.e. it does not take into account levels and jump transitions. * * @warning If @p epsilon_closure_opt is set, computes epsilon closures over multiple levels. * That is, the result might contain states of different levels. @@ -664,8 +665,9 @@ public: /** * @brief Returns a reference to targets (states) reachable from the given state over the given symbol. + * Note: It treats the transitions as NFA transitions, i.e. it does not take into account levels and jump transitions. * - * This is an optimized shortcut for post(state, symbol, EpsilonClosureOpt::NONE). + * This is an optimized shortcut for post(state, symbol, EpsilonClosureOpt::None). * * @param state A state to compute the post set from. * @param symbol Symbol to compute the post set for. @@ -675,6 +677,153 @@ public: return delta.get_successors(state, symbol); } + /** + * @brief Get the set of zero-level states reachable from the given set of zero-level @p states, + * over the @p symbol on a given @p symbol_level. It does not care about symbols on other levels. + * + * This is an optimized version of post methods for words. + * + * @param states Set of zero-level states to compute the post set from. + * @param symbol Symbol to match on the given level. + * @param symbol_level Level on which the symbol has to be matched. + * @param epsilon_closure_opt Epsilon closure option. Perform epsilon closure before and/or after the post operation. + * @param jump_mode 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 Set of zero-level states reachable from the given set of states over the given symbol on the given level. + */ + StateSet post(const StateSet& states, Symbol symbol, Level symbol_level, EpsilonClosureOpt epsilon_closure_opt = EpsilonClosureOpt::None, JumpMode jump_mode = JumpMode::RepeatSymbol) const; + + /** + * @brief Get the set of zero-level states reachable from the given zero-level @p state, + * over the @p symbol on a given @p symbol_level. It does not care about symbols on other levels. + * + * This is an optimized version of post for words. + * + * @param state A zero-level state to compute the post set from. + * @param symbol Symbol to match on the given level. + * @param symbol_level Level on which the symbol has to be matched. + * @param epsilon_closure_opt Epsilon closure option. Perform epsilon closure before and/or after the post operation. + * @param jump_mode 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 Set of zero-level states reachable from the given state over the given symbol on the given level. + */ + StateSet post(const State state, const Symbol symbol, const Level symbol_level, const EpsilonClosureOpt epsilon_closure_opt = EpsilonClosureOpt::None, const JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return post(StateSet{ state }, symbol, symbol_level, epsilon_closure_opt, jump_mode); + } + + /** + * @brief Get the set of states reachable from the given set of @p states over the given vector of @p words + * (index corresponds to the level). Levels with the corresponding @p use_level set to false will be ignored. + * + * This post uses a bitmask @p use_level to determine which levels to use. + * Node: Use of @p use_level si similar to applying a projection of levels whose entries are set to true. + * It is a general post method that is used by all of its overloads. + * + * @param states Set of states to compute the post set from. + * @param words Vector of words (w_1, w_2, ..., w_num_of_levels) to compute the post set for. + * The index of the word in the vector corresponds to the level (tape) on which the word is used. + * The length of the vector must be equal to the number of levels in the NFT. + * @param use_level Bitmask indicating which levels and their corresponding words to use. + * @param visited_zero_level_states Pointer to a set of states that will be filled with the zero-level states that were + * visited during the post operation. If nullptr, this set will not be filled. + * @param epsilon_closure_after Whether to perform epsilon closure after the post operation. + * @param jump_mode 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 Set of states reachable from the given set of states over the given words. + */ + StateSet post(const StateSet& states, const std::vector& words, const BoolVector& use_level, StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const; + + /** + * @brief Get the set of zero-level states reachable from the given set of zero-level @p states over the given + * vector of @p words (index corresponds to the level). All words on all levels are used and have to be specified. + * + * This post uses all words on all levels. + * + * @param states Set of zero-level states to compute the post set from. + * @param words Vector of words (w_1, w_2, ..., w_num_of_levels) to compute the post set for. + * The index of the word in the vector corresponds to the level (tape) on which the word is used. + * The length of the vector must be equal to the number of levels in the NFT. + * @param visited_zero_level_states Pointer to a set of states that will be filled with the zero-level states that were + * visited during the post operation. If nullptr, this set will not be filled. + * @param epsilon_closure_after Whether to perform epsilon closure after the post operation.ignored. + * @param jump_mode 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 Set of states reachable from the given set of states over the given words. + */ + StateSet post(const StateSet& states, const std::vector& words, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return post(states, words, BoolVector(words.size(), true), visited_zero_level_states, epsilon_closure_after, jump_mode); + } + + /** + * @brief Get the set of zero-level states reachable from the given zero-level @p state over the given + * vector of @p words (index corresponds to the level). All words on all levels are used and have to be specified. + * + * This post uses all words on all levels. + * + * @param state Zero-level state to compute the post set from. + * @param words Vector of words (w_1, w_2, ..., w_num_of_levels) to compute the post set for. + * The index of the word in the vector corresponds to the level (tape) on which the word is used. + * The length of the vector must be equal to the number of levels in the NFT. + * @param visited_zero_level_states Pointer to a set of states that will be filled with the zero-level states that were + * visited during the post operation. If nullptr, this set will not be filled. + * @param epsilon_closure_after Whether to perform epsilon closure after the post operation. + * @param jump_mode 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 Set of states reachable from the given set of states over the given words. + */ + StateSet post(const State state, const std::vector& words, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return post(StateSet{ state }, words, BoolVector(words.size(), true), visited_zero_level_states, epsilon_closure_after, jump_mode); + } + + /** + * @brief Get the set of zero-level states reachable from the given set of @p states over the given + * vector of @p words. The levels of the words are specified in @p word_levels vector. The post is computed only + * for the words that have a level corresponding to the level of the state. Levels not specified in @p word_levels + * are ignored (projected-out) + * + * This post uses a vector @p word_levels to specify levels of used words. + * Note: Use of @p word_levels is similar to applying a projection of levels from the vector @p word_levels. + * + * @param states Set of zero-level states to compute the post set from. + * @param words Vector of words to compute the post set for. + * @param word_levels Vector of levels corresponding to the words in @p words (has to be the same size as @p words). + * Levels not specified in @p word_levels are ignored/projected-out (any transition on such a level is taken). + * @param visited_zero_level_states Pointer to a set of states that will be filled with the zero-level states that were + * visited during the post operation. If nullptr, this set will not be filled. + * @param epsilon_closure_after Whether to perform epsilon closure after the post operation. + * @param jump_mode 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 Set of states reachable from the given set of states over the given words. + */ + StateSet post(const StateSet& states, const std::vector& words, const std::vector& word_levels, StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const; + + /** + * @brief Get the set of zero-level states reachable from the given zero-level @p state over the given + * vector of @p words. The levels of the words are specified in @p word_levels vector. The post is computed only + * for the words that have a level corresponding to the level of the state. Levels not specified in @p word_levels + * are ignored (projected-out). + * + * This post uses a vector @p word_levels to specify levels of used words. + * Note: Use of @p word_levels is similar to applying a projection of levels from the vector @p word_levels. + * + * @param state Zero-level state to compute the post set from. + * @param words Vector of words to compute the post set for. + * @param word_levels Vector of levels corresponding to the words in @p words (has to be the same size as @p words). + * Levels not specified in @p word_levels are ignored/projected-out (any transition on such a level is taken). + * @param visited_zero_level_states Pointer to a set of states that will be filled with the zero-level states that were + * visited during the post operation. If nullptr, this set will not be filled. + * @param epsilon_closure_after Whether to perform epsilon closure after the post operation. + * @param jump_mode 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 Set of states reachable from the given set of states over the given words. + */ + StateSet post(const State state, const std::vector& words, const std::vector& word_levels, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return post(StateSet{ state }, words, word_levels, visited_zero_level_states, epsilon_closure_after, jump_mode); + } /// Is the language of the automaton universal? bool is_universal(const Alphabet& alphabet, Run* cex = nullptr, @@ -1374,6 +1523,16 @@ bool symbols_match(Symbol a, Symbol b); namespace std { std::ostream& operator<<(std::ostream& os, const mata::nft::Nft& nft); +template<> +struct hash, mata::nfa::State>> { + size_t operator()(const std::pair, mata::nfa::State>& p) const { + size_t h = std::hash{}(p.second); + for (auto v : p.first) { + h ^= std::hash{}(v) + 0x9e3779b9 + (h << 6) + (h >> 2); + } + return h; + } +}; } // namespace std. #endif /* MATA_NFT_HH_ */ diff --git a/src/nft/nft.cc b/src/nft/nft.cc index 7d8253be9..a257df157 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -524,6 +524,236 @@ void Nft::unwind_jumps( result = unwind_jumps(dont_care_symbol_replacements, jump_mode); } +StateSet Nft::post(const StateSet& states, const Symbol symbol, const Level symbol_level, const EpsilonClosureOpt epsilon_closure_opt, const JumpMode jump_mode) const { + assert(std::all_of(states.begin(), states.end(), [&](State state) {return levels[state] == 0;})); + + // Computes the epsilon closure of a set of states. + auto get_epsilon_closure = [&](const StateSet& states) { + StateSet closure{ states }; + std::queue worklist; + for (const State state: states) { + worklist.push(state); + } + while (!worklist.empty()) { + const State state = worklist.front(); + worklist.pop(); + for (const State target: post(state, EPSILON, symbol_level, EpsilonClosureOpt::None, jump_mode)) { + if (!closure.contains(target)) { + closure.insert(target); + worklist.push(target); + } + } + } + return closure; + }; + + StateSet result{}; + // If we want to compute the epsilon cosure and the symbol is EPSILON, we can stay in the same zero states. + if (symbol == EPSILON && epsilon_closure_opt != EpsilonClosureOpt::None) { + result = states; + } + if (delta.empty()) { + return result; + } + + StateSet from_states = states; + if (epsilon_closure_opt == EpsilonClosureOpt::Before) { + // Before making the step using the symbol, we compute the epsilon closure. + from_states = get_epsilon_closure(states); + } + + StateSet used_nonzero_states; // To avoid cycling. + std::stack stack; + for (const State state : from_states) { + stack.push(state); + } + + // Adds states (with zero level) to the result or enqueues them for further processing. + auto add_to_result_or_enqueue = [&](const StateSet& targets) { + for (const State target : targets) { + if (levels[target] == 0) { + result.insert(target); + } else if (!used_nonzero_states.contains(target)) { + used_nonzero_states.insert(target); + stack.push(target); + } + } + }; + + // The main loop. + while (!stack.empty()) { + const State current_state = stack.top(); + const Level current_level = levels[current_state]; + stack.pop(); + + for (const SymbolPost &symbol_post : delta[current_state]) { + // DONT_CARE does not match EPSILON. + const Symbol transition_symbol = symbol_post.symbol; + const bool is_one_of_symbols_epsilon = (symbol == EPSILON || transition_symbol == EPSILON); + const bool is_one_of_symbols_dont_care = (symbol == DONT_CARE || transition_symbol == DONT_CARE); + const bool is_symbol_match = (transition_symbol == symbol || (is_one_of_symbols_dont_care && !is_one_of_symbols_epsilon)); + if (current_level > symbol_level) { + // The transiton is behind us. Just go forward until next zero level state. + add_to_result_or_enqueue(symbol_post.targets); + } else if (current_level == symbol_level && is_symbol_match) { + // We are exactly at the symbol_level and the symbol matches. Proceed. + add_to_result_or_enqueue(symbol_post.targets); + } else if (current_level < symbol_level) { + // We are before the symbol_level. We need to check if we are jumping over the symbol_level or not. + for (const State target : symbol_post.targets) { + const Level target_level = levels[target]; + const bool are_we_jumping_over_the_symbol_level = (target_level > symbol_level || target_level == 0); + if (are_we_jumping_over_the_symbol_level) { + // We need to match the symbol based on the jump_mode. + // DONT_CARE does not match EPSILON. + if ((jump_mode == JumpMode::AppendDontCares && symbol != EPSILON) || + (jump_mode == JumpMode::RepeatSymbol && is_symbol_match)) { + if (target_level == 0) { + result.insert(target); + } else if (!used_nonzero_states.contains(target)) { + used_nonzero_states.insert(target); + stack.push(target); + } + } + } else { + // We are not jumping over the symbol_level, just go forward. + if (!used_nonzero_states.contains(target)) { + used_nonzero_states.insert(target); + stack.push(target); + } + } + } + } + } + } + + if (epsilon_closure_opt == EpsilonClosureOpt::After) { + // We need to compute the epsilon closure of the resulting states. + return get_epsilon_closure(result); + } + + return result; +} + +StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols, const BoolVector& use_tape, StateSet* const visited_zero_level_states, const bool epsilon_closure_after, const JumpMode jump_mode) const { + assert(std::all_of(states.begin(), states.end(), [&](State state) {return levels[state] == 0;})); + if (delta.empty()) { + if (visited_zero_level_states != nullptr) { + // Keep track of visited zero level states. + // This is usefull for is_prefix_in_lang function. + visited_zero_level_states->insert(states); + } + if (std::all_of(tape_symbols.begin(), tape_symbols.end(), [](const Word& word) { return word.empty(); })) { + // If all tape symbols are empty (all words are epsilon), we can return existing zero level states. + return states; + } + return {}; + } + + StateSet result{}; + // visited contains visited configuration pairs of (positions, state). + // positions is a vector of reading head positions for each of n words in the input vector, + // where n is the number of levels in the NFT. + std::unordered_set, State>> visited; + std::stack, State>> stack; + for (const State state : states) { + const std::pair, State> initial_config{ std::vector(tape_symbols.size(), 0), state }; + stack.push({ initial_config }); + visited.insert(std::move(initial_config)); + + } + // End positions of reading heads after processing all symbols on each word. + std::vector end_positions(tape_symbols.size(), 0); + for (size_t i = 0; i < tape_symbols.size(); ++i) { + end_positions[i] = tape_symbols[i].size(); + } + + // Two symbols match iff they are equal, or one is DONT_CARE and neither is EPSILON. + // EPSILON matches only EPSILON. (The same relation as nft::symbols_match.) + auto symbols_match = [](const Symbol a, const Symbol b) { + return (a == EPSILON || b == EPSILON) ? (a == EPSILON && b == EPSILON) + : (a == b || a == DONT_CARE || b == DONT_CARE); + }; + // Enqueue a configuration (reading-head positions + state) unless already visited. + auto enqueue = [&](std::vector next_positions, const State target) { + auto next_config = std::make_pair(std::move(next_positions), target); + if (!visited.contains(next_config)) { + visited.insert(next_config); + stack.push(std::move(next_config)); + } + }; + + // The main loop. + while (!stack.empty()) { + const auto [current_positions, current_state] = stack.top(); + const Level current_level = levels[current_state]; + stack.pop(); + + if (current_level == 0) { + if (visited_zero_level_states != nullptr) { + // Keep track of visited zero level states. + // This is usefull for is_prefix_in_lang function. + visited_zero_level_states->insert(current_state); + } + if(current_positions == end_positions) { + // We reached a zero level state with all tape symbols processed. + result.insert(current_state); + if (!epsilon_closure_after) { + continue; // No need to explore further if we are not looking for epsilon closure. + } + } + } + + for (const SymbolPost &symbol_post: delta[current_state]) { + const Symbol transition_symbol = symbol_post.symbol; + for (const State target: symbol_post.targets) { + const Level target_level = levels[target]; + // The (possibly jumping) transition reads one symbol on each level it spans: + // [current_level, stop_level_idx). On a jump the symbol is repeated, or replaced by + // DONT_CARE for the trailing levels in JumpMode::AppendDontCares. + const size_t stop_level_idx = target_level == 0 ? levels.num_of_levels : target_level; + + // Consuming step: read (and advance past) one input symbol on each used level of the span. + // A level with no input left cannot be read, so the step fails. Because exhaustion is + // detected by the reading-head position (not by an EPSILON sentinel), a literal EPSILON + // symbol in an input word is matched and consumed here by an EPSILON transition. + std::vector next_positions{ current_positions }; + bool consumed = true; + for (size_t level = current_level; level < stop_level_idx; ++level) { + if (!use_tape[level]) { continue; } // Projected-out level: take the transition, read nothing. + const Symbol expected = (level == current_level || jump_mode != JumpMode::AppendDontCares) + ? transition_symbol : DONT_CARE; + if (current_positions[level] >= end_positions[level] || + !symbols_match(expected, tape_symbols[level][current_positions[level]])) { + consumed = false; + break; + } + ++next_positions[level]; + } + if (consumed) { enqueue(std::move(next_positions), target); } + + // Non-consuming step: an EPSILON transition may change state without reading any input. + // This is what lets it be taken when a tape is exhausted; kept separate from the consuming + // step above so that a literal EPSILON in an input word can still be read there. + if (transition_symbol == EPSILON) { enqueue(current_positions, target); } + } + } + } + + return result; +} + +StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols, const std::vector& tape_levels, StateSet* visited_zero_level_states, const bool epsilon_closure_after, JumpMode jump_mode) const { + assert(tape_symbols.size() == tape_levels.size()); + std::vector word_per_level(levels.num_of_levels); + BoolVector use_level(levels.num_of_levels, false); + for (size_t i = 0; i < tape_symbols.size(); ++i) { + use_level[tape_levels[i]] = true; + word_per_level[tape_levels[i]] = tape_symbols[i]; + } + return post(states, word_per_level, use_level, visited_zero_level_states, epsilon_closure_after, jump_mode); +} + Nft& Nft::operator=(Nft&& other) noexcept { if (this != &other) { Nfa::operator=(other); diff --git a/src/nft/operations.cc b/src/nft/operations.cc index baf7db568..cc944af2c 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -1202,117 +1202,12 @@ bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool if (level_words.size() != levels.num_of_levels) { throw std::invalid_argument("Invalid number of tracks. Expected " + std::to_string(levels.num_of_levels) + "."); } - std::vector track_words_begins(levels.num_of_levels); - for (size_t track{ 0 }; track < levels.num_of_levels; ++track) { - track_words_begins[track] = level_words[track].begin(); - } - - const std::vector track_words_ends{ - [&]() { - std::vector val(levels.num_of_levels); - for (size_t track{ 0 }; track < levels.num_of_levels; ++track) { val[track] = level_words[track].end(); } - return val; - }() - }; - - auto are_all_track_words_read = [&](const std::vector& word_begins) { - for (Level i{ 0 }; i < levels.num_of_levels; ++i) { - if (word_begins[i] != track_words_ends[i]) { return false; } - } - return true; - }; - - auto words_match = [&](const std::vector& word_its) { - return match_prefix || are_all_track_words_read(word_its); - }; - - if (final.intersects_with(initial) && words_match(track_words_begins)) { return true; } - - using StateWordBeginsPair = std::pair>; - std::deque worklist{}; - for (const State state : initial) { worklist.emplace_back(state, track_words_begins); } - while (!worklist.empty()) { - const auto [state, words_its]{ std::move(worklist.front()) }; - worklist.pop_front(); - const Level level = levels[state]; - const StatePost& state_post{ delta[state] }; - const auto state_post_end{ state_post.end() }; - const auto word_symbol_it{ words_its[level] }; - - // Try epsilon transitions without reading input words. - // Allows moving between states even when no input symbols are left to read. - // This works for both jumps and single-level transitions. - // If all levels contain epsilon, we eventually achieve a simple change of state. - auto symbol_post_it{ state_post.find(EPSILON) }; - if (symbol_post_it != state_post_end) { - for (State target : symbol_post_it->targets) { - if (levels[target] == 0 && final.contains(target) && words_match(words_its)) { return true; } - worklist.emplace_back(target, words_its); - } - } - - // No input words left to read at this level, and no epsilon transitions available. - // Thus, cannot proceed further from this state. - if (word_symbol_it == track_words_ends[level]) { continue; } - - auto handle_symbol_it{ - [&] { - for (State target : symbol_post_it->targets) { - bool jump_failed{ false }; - const Level level_target{ levels[target] }; - auto next_words_its{ words_its }; - if (level == 0 && level_target == 0) { - for (Level level_loop{ level }; level_loop < levels.num_of_levels; ++level_loop) { - if (next_words_its[level_loop] == track_words_ends[level_loop] || - not symbols_match(symbol_post_it->symbol, *next_words_its[level_loop])) { - jump_failed = true; - break; - } - ++next_words_its[level_loop]; - } - } else { - for (Level level_loop{ level }; level_loop != level_target; - level_loop = levels.next_level_after(level_loop)) { - if (next_words_its[level_loop] == track_words_ends[level_loop] || - not symbols_match(symbol_post_it->symbol, *next_words_its[level_loop])) { - jump_failed = true; - break; - } - ++next_words_its[level_loop]; - } - } - if (jump_failed) { continue; } - if (levels[target] == 0 && final.contains(target) && words_match(next_words_its)) { return true; } - worklist.emplace_back(target, next_words_its); - } - return false; - } - }; - - // Try all normal symbol transitions when the current input symbol is DONT_CARE. - // They allow proceeding without exactly matching the current input symbol, otherwise behaving like normal - // non-epsilon transitions. - if (*word_symbol_it == DONT_CARE) { - symbol_post_it = state_post.begin(); - for (; symbol_post_it != state_post_end; ++symbol_post_it) { - if (symbol_post_it->symbol == EPSILON) { continue; } - if (handle_symbol_it()) { return true; } - } - } - - // Try DONT_CARE transitions. - // They allow proceeding without matching the current input symbol, otherwise behaving like normal non-epsilon - // transitions. - // Read the current input symbol on all levels involved in the transition (multiple if it is a jump). - symbol_post_it = state_post.find(DONT_CARE); - if (*word_symbol_it != EPSILON && symbol_post_it != state_post_end && handle_symbol_it()) { return true; } - - // Try normal transitions with the current input symbol. - // They allow proceeding only after matching the current input symbol. - // Read the current input symbol on all levels involved in the transition (multiple if it is a jump). - // Note: EPSILON symbols behave like normal symbols here, but do not match with DONT_CARE. - symbol_post_it = state_post.find(*word_symbol_it); - if (symbol_post_it != state_post_end && handle_symbol_it()) { return true; } - } - return false; + // Membership is a thin consumer of the reachability primitive post(): the level words are in the + // language iff a final state is reachable after consuming all of them; for a prefix query it suffices + // to reach a final zero-level state after consuming any prefix (tracked via the visited states). + StateSet visited_zero_level_states{}; + StateSet* const visited_ptr = match_prefix ? &visited_zero_level_states : nullptr; + const StateSet reached{ post(StateSet{ initial.begin(), initial.end() }, level_words, visited_ptr, true) }; + return final.intersects_with(reached) + || (match_prefix && final.intersects_with(visited_zero_level_states)); } diff --git a/tests/nft/nft-post.cc b/tests/nft/nft-post.cc new file mode 100644 index 000000000..86693d9dc --- /dev/null +++ b/tests/nft/nft-post.cc @@ -0,0 +1,316 @@ +// Tests for the tuple-oriented Nft::post(...) family and the Nft::is_in_lang(...) / +// Nft::is_prefix_in_lang(...) methods built on top of them. +// +// These methods interpret an NFT as a k-tape machine (k = num_of_levels): a single +// "transducer step" walks a path of zero-level -> level 1 -> ... -> level k-1 -> zero-level +// states, reading one symbol per level from the corresponding tape (word). An EPSILON +// transition on a level consumes nothing on that tape, a DONT_CARE transition matches any +// single real input symbol (but not epsilon), and a jump transition (target skipping levels) +// reads the same symbol on every skipped level (JumpMode::RepeatSymbol) or the symbol on the +// first level and DONT_CARE on the rest (JumpMode::AppendDontCares). + +#include + +#include "mata/nft/nft.hh" + +using namespace mata; +using namespace mata::nft; +using mata::Symbol; +using mata::Word; + +namespace { + +// Readable symbol names. Note: nft::EPSILON is the max symbol and nft::DONT_CARE == EPSILON - 1. +constexpr Symbol a{ 0 }; +constexpr Symbol b{ 1 }; +constexpr Symbol c{ 2 }; +constexpr Symbol d{ 3 }; +constexpr Symbol x{ 10 }; +constexpr Symbol y{ 11 }; +constexpr Symbol z{ 12 }; + +// A 2-level NFT accepting exactly the relation { ("ab", "c") }. +// Path: 0 --a(lvl0)--> 2 --c(lvl1)--> 3 --b(lvl0)--> 4 --eps(lvl1)--> 1(final). +Nft make_ab_c() { + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State qf{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(qf); + n.insert_word_by_levels(q0, { Word{ a, b }, Word{ c } }, qf); + return n; +} + +} // namespace + +TEST_CASE("mata::nft::Nft::post(symbol, level) — basic matching and other-level indifference") { + // 0 --a(lvl0)--> 1 --c(lvl1)--> 2(final). + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q2); + n.delta.add(q0, a, q1); + n.delta.add(q1, c, q2); + + SECTION("match on level 0, indifferent to level 1") { + // 'a' matches on level 0; the level-1 symbol 'c' is walked over to the next zero-level state. + CHECK(n.post(StateSet{ q0 }, a, 0) == StateSet{ q2 }); + CHECK(n.post(q0, a, 0) == StateSet{ q2 }); // single-state overload + } + + SECTION("no match on level 0") { + CHECK(n.post(StateSet{ q0 }, b, 0) == StateSet{}); + } + + SECTION("match on level 1, indifferent to level 0") { + // The level-0 transition 'a' is walked over; 'c' must match on level 1. + CHECK(n.post(StateSet{ q0 }, c, 1) == StateSet{ q2 }); + CHECK(n.post(StateSet{ q0 }, d, 1) == StateSet{}); + } + + SECTION("empty NFT (empty delta)") { + Nft empty{ Nft::with_levels(2) }; + const State s{ empty.add_state_with_level(0) }; + CHECK(empty.post(StateSet{ s }, a, 0) == StateSet{}); + // With an epsilon closure requested and EPSILON symbol, the source state stays reachable. + CHECK(empty.post(StateSet{ s }, EPSILON, 0, EpsilonClosureOpt::Before) == StateSet{ s }); + } +} + +TEST_CASE("mata::nft::Nft::post(symbol, level) — DONT_CARE") { + // 0 --DONT_CARE(lvl0)--> 1 --c(lvl1)--> 2(final). + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q2); + n.delta.add(q0, DONT_CARE, q1); + n.delta.add(q1, c, q2); + + // DONT_CARE transition is matched by any real symbol. + CHECK(n.post(StateSet{ q0 }, a, 0) == StateSet{ q2 }); + CHECK(n.post(StateSet{ q0 }, b, 0) == StateSet{ q2 }); + // ... but a DONT_CARE transition is not matched by an EPSILON query. + CHECK(n.post(StateSet{ q0 }, EPSILON, 0) == StateSet{}); +} + +TEST_CASE("mata::nft::Nft::post(symbol, level) — epsilon closure") { + // 0 --eps--> 1 (both zero-level), 1 --a(lvl0)--> 2 --c(lvl1)--> 3(final). + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(0) }; + const State q2{ n.add_state_with_level(1) }; + const State q3{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q3); + n.delta.add(q0, EPSILON, q1); + n.delta.add(q1, a, q2); + n.delta.add(q2, c, q3); + + SECTION("NONE: the epsilon move is not taken") { + CHECK(n.post(StateSet{ q0 }, a, 0, EpsilonClosureOpt::None) == StateSet{}); + } + + SECTION("BEFORE: epsilon closure then the symbol step") { + CHECK(n.post(StateSet{ q0 }, a, 0, EpsilonClosureOpt::Before) == StateSet{ q3 }); + } + + SECTION("EPSILON query: closure includes the source, NONE is a single epsilon step") { + CHECK(n.post(StateSet{ q0 }, EPSILON, 0, EpsilonClosureOpt::Before) == StateSet{ q0, q1 }); + CHECK(n.post(StateSet{ q0 }, EPSILON, 0, EpsilonClosureOpt::None) == StateSet{ q1 }); + } + + SECTION("AFTER: symbol step then epsilon closure") { + // 0 --a(lvl0)--> 1 --c(lvl1)--> 2(zero-level), and 2 --eps--> 3(final zero-level). + Nft m{ Nft::with_levels(2) }; + const State s0{ m.add_state_with_level(0) }; + const State s1{ m.add_state_with_level(1) }; + const State s2{ m.add_state_with_level(0) }; + const State s3{ m.add_state_with_level(0) }; + m.initial.insert(s0); + m.final.insert(s3); + m.delta.add(s0, a, s1); + m.delta.add(s1, c, s2); + m.delta.add(s2, EPSILON, s3); + CHECK(m.post(StateSet{ s0 }, a, 0, EpsilonClosureOpt::None) == StateSet{ s2 }); + CHECK(m.post(StateSet{ s0 }, a, 0, EpsilonClosureOpt::After) == StateSet{ s2, s3 }); + } +} + +TEST_CASE("mata::nft::Nft::post(symbol, level) — jump transitions crossing the level") { + SECTION("whole-cycle jump (level 0 -> level 0)") { + // 0 --a(jump lvl0->lvl0)--> 1(final): consumes 'a' on level 0 and 'a' on level 1. + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q1); + n.delta.add(q0, a, q1); + + // Query for a symbol on level 1 which the jump crosses. + CHECK(n.post(StateSet{ q0 }, a, 1, EpsilonClosureOpt::None, JumpMode::RepeatSymbol) == StateSet{ q1 }); + CHECK(n.post(StateSet{ q0 }, b, 1, EpsilonClosureOpt::None, JumpMode::RepeatSymbol) == StateSet{}); + // AppendDontCares: the crossed level is a DONT_CARE, matched by any real symbol. + CHECK(n.post(StateSet{ q0 }, b, 1, EpsilonClosureOpt::None, JumpMode::AppendDontCares) == StateSet{ q1 }); + } + + SECTION("3-level, not jumping over the queried level") { + // 0 --a(lvl0)--> 1(lvl1) --b(lvl1)--> 2(lvl2): query on level 2 walks levels 0 and 1. + Nft n{ Nft::with_levels(3) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(2) }; + const State q3{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q3); + n.delta.add(q0, a, q1); + n.delta.add(q1, b, q2); + n.delta.add(q2, c, q3); + CHECK(n.post(StateSet{ q0 }, c, 2) == StateSet{ q3 }); + CHECK(n.post(StateSet{ q0 }, d, 2) == StateSet{}); + } +} + +TEST_CASE("mata::nft::Nft::post(words) — exact tuple matching") { + Nft n{ make_ab_c() }; + const State q0{ *n.initial.begin() }; + const State qf{ *n.final.begin() }; + + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a, b }, Word{ c } }) == StateSet{ qf }); + CHECK(n.post(q0, std::vector{ Word{ a, b }, Word{ c } }) == StateSet{ qf }); // single-state overload + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a, b }, Word{ d } }) == StateSet{}); + // ("a","c") is a proper prefix: it reaches an intermediate zero-level state but not the final one. + CHECK_FALSE(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ c } }).contains(qf)); + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a, b }, Word{ c, d } }) == StateSet{}); +} + +TEST_CASE("mata::nft::Nft::post(words) — epsilon track consumes nothing") { + // Relation ("a", ""): 0 --a(lvl0)--> 1 --eps(lvl1)--> 2(final). + // Regression: an EPSILON transition must never advance a (possibly already exhausted) tape head. + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q2); + n.delta.add(q0, a, q1); + n.delta.add(q1, EPSILON, q2); + + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{} }) == StateSet{ q2 }); + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ c } }) == StateSet{}); + // Empty words consume nothing, so only the source zero-level state is reached. + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{}, Word{} }) == StateSet{ q0 }); +} + +TEST_CASE("mata::nft::Nft::post(words) — DONT_CARE track") { + // Relation (x, "c") for any single symbol x: 0 --DONT_CARE(lvl0)--> 1 --c(lvl1)--> 2(final). + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q2); + n.delta.add(q0, DONT_CARE, q1); + n.delta.add(q1, c, q2); + + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ c } }) == StateSet{ q2 }); + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ b }, Word{ c } }) == StateSet{ q2 }); + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ d } }) == StateSet{}); + // DONT_CARE requires a real input symbol; it does not match an empty (epsilon) tape. + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{}, Word{ c } }) == StateSet{}); +} + +TEST_CASE("mata::nft::Nft::post(words) — jump transition and jump modes") { + // 0 --a(jump lvl0->lvl0)--> 1(final). + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q1); + n.delta.add(q0, a, q1); + + SECTION("RepeatSymbol: same symbol on every crossed level") { + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ a } }, nullptr, true, JumpMode::RepeatSymbol) == StateSet{ q1 }); + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ b } }, nullptr, true, JumpMode::RepeatSymbol) == StateSet{}); + } + SECTION("AppendDontCares: DONT_CARE on the crossed levels") { + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ a } }, nullptr, true, JumpMode::AppendDontCares) == StateSet{ q1 }); + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ b } }, nullptr, true, JumpMode::AppendDontCares) == StateSet{ q1 }); + // The appended DONT_CARE still needs a real symbol on level 1. + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{} }, nullptr, true, JumpMode::AppendDontCares) == StateSet{}); + } +} + +TEST_CASE("mata::nft::Nft::post(words) — projection (use_level bitmask and word_levels)") { + Nft n{ make_ab_c() }; // relation ("ab", "c") + const State q0{ *n.initial.begin() }; + const State qf{ *n.final.begin() }; + + SECTION("word_levels projection ignores the unspecified level") { + // Project onto level 0: level 1 ("c") is ignored, so "ab" is enough to reach the final state. + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a, b } }, std::vector{ 0 }).contains(qf)); + // Project onto level 1: level 0 ("ab") is ignored. + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ c } }, std::vector{ 1 }).contains(qf)); + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ d } }, std::vector{ 1 }) == StateSet{}); + } + + SECTION("use_level bitmask overload matches word_levels projection") { + BoolVector use_level_0{ true, false }; + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a, b }, Word{} }, use_level_0).contains(qf)); + BoolVector use_level_1{ false, true }; + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{}, Word{ c } }, use_level_1).contains(qf)); + } +} + +TEST_CASE("mata::nft::Nft::post(words) — empty delta, empty words, and visited states") { + SECTION("empty delta: all-empty words keep the source states, otherwise empty") { + Nft n{ Nft::with_levels(2) }; + const State s{ n.add_state_with_level(0) }; + CHECK(n.post(StateSet{ s }, std::vector{ Word{}, Word{} }) == StateSet{ s }); + CHECK(n.post(StateSet{ s }, std::vector{ Word{ a }, Word{} }) == StateSet{}); + } + + SECTION("visited_zero_level_states is populated") { + // Relation ("a","x") then ("b","y") chained through zero-level state qmid. + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State qmid{ n.add_state_with_level(0) }; + const State qend{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(qend); + n.insert_word_by_levels(q0, { Word{ a }, Word{ x } }, qmid); + n.insert_word_by_levels(qmid, { Word{ b }, Word{ y } }, qend); + + StateSet visited{}; + const StateSet targets{ n.post(StateSet{ q0 }, std::vector{ Word{ a, b }, Word{ x, y } }, &visited) }; + CHECK(targets == StateSet{ qend }); + // Both the intermediate and final zero-level states are visited while consuming the tuple. + CHECK(visited.contains(q0)); + CHECK(visited.contains(qmid)); + CHECK(visited.contains(qend)); + } +} + +TEST_CASE("mata::nft::Nft::post(words) — epsilon_closure_after flag") { + // Consuming ("a","c") reaches zero-level state q2, and q2 --eps--> q3 (final zero-level). + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(0) }; + const State q3{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q3); + n.delta.add(q0, a, q1); + n.delta.add(q1, c, q2); + n.delta.add(q2, EPSILON, q3); + + // With the closure (default) the trailing epsilon move to q3 is followed. + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ c } }, nullptr, /*epsilon_closure_after=*/true) == StateSet{ q2, q3 }); + // Without it, exploration stops at the first zero-level state reached at the end position. + CHECK(n.post(StateSet{ q0 }, std::vector{ Word{ a }, Word{ c } }, nullptr, /*epsilon_closure_after=*/false) == StateSet{ q2 }); + // is_in_lang_by_levels always closes after, so it still reaches the final state. + CHECK(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ c } })); +} From 5a7b8017f50c7eb6dad4ab673e99d3beb6066751 Mon Sep 17 00:00:00 2001 From: koniksedy Date: Wed, 15 Jul 2026 13:14:44 +0200 Subject: [PATCH 02/10] 2 implementations of the Nft::is_in_lang --- include/mata/nft/nft.hh | 43 +++++++++-- src/nft/operations.cc | 159 ++++++++++++++++++++++++++++++++++++---- 2 files changed, 178 insertions(+), 24 deletions(-) diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index b0af86990..9a5b06503 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -836,9 +836,13 @@ public: * * @param run The run to check. * @param match_prefix Whether to also match the prefix of the word. + * @param jump_mode 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. Dispatches to the dedicated fast algorithm for @c JumpMode::RepeatSymbol and + * to the general @c post()-based algorithm otherwise. * @return @c true if @p run is in the language of the automaton, @c false otherwise. */ - bool is_in_lang(const Run& run, bool match_prefix = false) const; + bool is_in_lang(const Run& run, bool match_prefix = false, JumpMode jump_mode = JumpMode::RepeatSymbol) const; bool is_in_lang(const Run&, bool, bool) const = delete; /** @@ -846,10 +850,13 @@ public: * * @param word The word to check. * @param match_prefix Whether to also match the prefix of the word. + * @param jump_mode 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 @c true if @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang(const Word& word, const bool match_prefix = false) const { - return is_in_lang(Run{ word, {} }, match_prefix); + bool is_in_lang(const Word& word, const bool match_prefix = false, const JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return is_in_lang(Run{ word, {} }, match_prefix, jump_mode); } bool is_in_lang(const Word& word, bool, bool) const = delete; @@ -857,9 +864,14 @@ public: * @brief Check whether a prefix of a @p run is in the language of an automaton. * * @param run The run to check. + * @param jump_mode 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 @c true if the prefix of @p run is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_prefix(const Run& run) const { return is_in_lang(run, true); } + bool is_in_lang_prefix(const Run& run, JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return is_in_lang(run, true, jump_mode); + } bool is_in_lang_prefix(const Run&, bool) const = delete; @@ -867,9 +879,14 @@ public: * @brief Check whether a prefix of a @p word is in the language of an automaton. * * @param word The word to check. + * @param jump_mode 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 @c true if the prefix of @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_prefix(const Word& word) const { return is_in_lang_prefix(Run{ word, {} }); } + bool is_in_lang_prefix(const Word& word, JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return is_in_lang_prefix(Run{ word, {} }, jump_mode); + } bool is_in_lang_prefix(const Word&, bool) const = delete; /** @@ -878,11 +895,18 @@ public: * That is, the function checks whether a tuple @p level_words (word1, word2, word3, ..., wordn) is in the regular * relation accepted by the transducer with 'n' levels (tracks). * + * For @c JumpMode::RepeatSymbol (the default), a dedicated worklist algorithm is used which is considerably + * faster than the general algorithm. For @c JumpMode::AppendDontCares, the check is delegated to the general + * @c post()-based implementation, which is the only one able to correctly interpret @c DONT_CARE-padded jumps. + * * @param level_words The words to check. * @param match_prefix Whether to also match the prefix of the word. + * @param jump_mode 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 @c true if @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_by_levels(const std::vector& level_words, bool match_prefix = false) const; + bool is_in_lang_by_levels(const std::vector& level_words, bool match_prefix = false, JumpMode jump_mode = JumpMode::RepeatSymbol) const; /** * @brief Checks whether the prefix of @p level_words is in the language of the transducer. @@ -891,10 +915,13 @@ public: * regular relation accepted by the transducer with 'n' levels (tracks). * * @param level_words The words to check. + * @param jump_mode 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 @c true if the prefix of @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_prefix_by_levels(const std::vector& level_words) const { - return is_in_lang_by_levels(level_words, true); + bool is_in_lang_prefix_by_levels(const std::vector& level_words, JumpMode jump_mode = JumpMode::RepeatSymbol) const { + return is_in_lang_by_levels(level_words, true, jump_mode); } /** diff --git a/src/nft/operations.cc b/src/nft/operations.cc index cc944af2c..3c0d8be8a 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -3,6 +3,7 @@ */ #include +#include #include #include #include @@ -118,6 +119,126 @@ Nft reduce_size_by_simulation(const Nft& aut, StateRenaming& state_renaming) { return result; } + +/// Dedicated worklist algorithm for Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol (a jump transition +/// reads the same symbol on every level it spans). Kept as a separate, hand-rolled implementation because it is +/// considerably faster in this common case than the general post()-based algorithm, which additionally has to +/// support JumpMode::AppendDontCares. +bool is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, const bool match_prefix) { + std::vector track_words_begins(aut.levels.num_of_levels); + for (size_t track{ 0 }; track < aut.levels.num_of_levels; ++track) { + track_words_begins[track] = level_words[track].begin(); + } + + const std::vector track_words_ends{ + [&]() { + std::vector val(aut.levels.num_of_levels); + for (size_t track{ 0 }; track < aut.levels.num_of_levels; ++track) { val[track] = level_words[track].end(); } + return val; + }() + }; + + auto are_all_track_words_read = [&](const std::vector& word_begins) { + for (Level i{ 0 }; i < aut.levels.num_of_levels; ++i) { + if (word_begins[i] != track_words_ends[i]) { return false; } + } + return true; + }; + + auto words_match = [&](const std::vector& word_its) { + return match_prefix || are_all_track_words_read(word_its); + }; + + if (aut.final.intersects_with(aut.initial) && words_match(track_words_begins)) { return true; } + + using StateWordBeginsPair = std::pair>; + std::deque worklist{}; + for (const State state : aut.initial) { worklist.emplace_back(state, track_words_begins); } + while (!worklist.empty()) { + const auto [state, words_its]{ std::move(worklist.front()) }; + worklist.pop_front(); + const Level level = aut.levels[state]; + const StatePost& state_post{ aut.delta[state] }; + const auto state_post_end{ state_post.end() }; + const auto word_symbol_it{ words_its[level] }; + + // Try epsilon transitions without reading input words. + // Allows moving between states even when no input symbols are left to read. + // This works for both jumps and single-level transitions. + // If all levels contain epsilon, we eventually achieve a simple change of state. + auto symbol_post_it{ state_post.find(nft::EPSILON) }; + if (symbol_post_it != state_post_end) { + for (State target : symbol_post_it->targets) { + if (aut.levels[target] == 0 && aut.final.contains(target) && words_match(words_its)) { return true; } + worklist.emplace_back(target, words_its); + } + } + + // No input words left to read at this level, and no epsilon transitions available. + // Thus, cannot proceed further from this state. + if (word_symbol_it == track_words_ends[level]) { continue; } + + auto handle_symbol_it{ + [&] { + for (State target : symbol_post_it->targets) { + bool jump_failed{ false }; + const Level level_target{ aut.levels[target] }; + auto next_words_its{ words_its }; + if (level == 0 && level_target == 0) { + for (Level level_loop{ level }; level_loop < aut.levels.num_of_levels; ++level_loop) { + if (next_words_its[level_loop] == track_words_ends[level_loop] || + not symbols_match(symbol_post_it->symbol, *next_words_its[level_loop])) { + jump_failed = true; + break; + } + ++next_words_its[level_loop]; + } + } else { + for (Level level_loop{ level }; level_loop != level_target; + level_loop = aut.levels.next_level_after(level_loop)) { + if (next_words_its[level_loop] == track_words_ends[level_loop] || + not symbols_match(symbol_post_it->symbol, *next_words_its[level_loop])) { + jump_failed = true; + break; + } + ++next_words_its[level_loop]; + } + } + if (jump_failed) { continue; } + if (aut.levels[target] == 0 && aut.final.contains(target) && words_match(next_words_its)) { return true; } + worklist.emplace_back(target, next_words_its); + } + return false; + } + }; + + // Try all normal symbol transitions when the current input symbol is DONT_CARE. + // They allow proceeding without exactly matching the current input symbol, otherwise behaving like normal + // non-epsilon transitions. + if (*word_symbol_it == DONT_CARE) { + symbol_post_it = state_post.begin(); + for (; symbol_post_it != state_post_end; ++symbol_post_it) { + if (symbol_post_it->symbol == nft::EPSILON) { continue; } + if (handle_symbol_it()) { return true; } + } + } + + // Try DONT_CARE transitions. + // They allow proceeding without matching the current input symbol, otherwise behaving like normal non-epsilon + // transitions. + // Read the current input symbol on all levels involved in the transition (multiple if it is a jump). + symbol_post_it = state_post.find(DONT_CARE); + if (*word_symbol_it != nft::EPSILON && symbol_post_it != state_post_end && handle_symbol_it()) { return true; } + + // Try normal transitions with the current input symbol. + // They allow proceeding only after matching the current input symbol. + // Read the current input symbol on all levels involved in the transition (multiple if it is a jump). + // Note: EPSILON symbols behave like normal symbols here, but do not match with DONT_CARE. + symbol_post_it = state_post.find(*word_symbol_it); + if (symbol_post_it != state_post_end && handle_symbol_it()) { return true; } + } + return false; +} } Nft mata::nft::remove_epsilon(const Nft& aut, Symbol epsilon) { @@ -828,8 +949,28 @@ Nft nft::invert_levels(const Nft& aut, const JumpMode jump_mode) { return aut_inv; } -bool Nft::is_in_lang(const Run& run, const bool match_prefix) const { - return is_in_lang_by_levels(mk_level_word_from_word(run.word), match_prefix); +bool Nft::is_in_lang(const Run& run, const bool match_prefix, const JumpMode jump_mode) const { + return is_in_lang_by_levels(mk_level_word_from_word(run.word), match_prefix, jump_mode); +} + +bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool match_prefix, const JumpMode jump_mode) const { + if (level_words.size() != levels.num_of_levels) { + throw std::invalid_argument("Invalid number of tracks. Expected " + std::to_string(levels.num_of_levels) + "."); + } + + if (jump_mode != JumpMode::AppendDontCares) { + // Dedicated worklist algorithm, considerably faster than the general post()-based algorithm below. + return is_in_lang_by_levels_repeat_symbol(*this, level_words, match_prefix); + } + + // General post()-based algorithm: the only one able to correctly interpret DONT_CARE-padded jumps + // (JumpMode::AppendDontCares). Membership is a thin consumer of the reachability primitive post(): the level + // words are in the language iff a final state is reachable after consuming all of them; for a prefix query it + // suffices to reach a final zero-level state after consuming any prefix (tracked via the visited states). + StateSet visited_zero_level_states{}; + StateSet* const visited_ptr = match_prefix ? &visited_zero_level_states : nullptr; + const StateSet reached{ post(StateSet{ initial.begin(), initial.end() }, level_words, visited_ptr, true, jump_mode) }; + return final.intersects_with(reached) || (match_prefix && final.intersects_with(visited_zero_level_states)); } std::pair Nft::get_word_for_path(const Run& run) const { @@ -1197,17 +1338,3 @@ std::set Nft::get_words(const size_t max_length, const JumpMode jump_mode) return result; } - -bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool match_prefix) const { - if (level_words.size() != levels.num_of_levels) { - throw std::invalid_argument("Invalid number of tracks. Expected " + std::to_string(levels.num_of_levels) + "."); - } - // Membership is a thin consumer of the reachability primitive post(): the level words are in the - // language iff a final state is reachable after consuming all of them; for a prefix query it suffices - // to reach a final zero-level state after consuming any prefix (tracked via the visited states). - StateSet visited_zero_level_states{}; - StateSet* const visited_ptr = match_prefix ? &visited_zero_level_states : nullptr; - const StateSet reached{ post(StateSet{ initial.begin(), initial.end() }, level_words, visited_ptr, true) }; - return final.intersects_with(reached) - || (match_prefix && final.intersects_with(visited_zero_level_states)); -} From c2eaa7788ad4599e8b689aa43c0cd96cf74c6e7f Mon Sep 17 00:00:00 2001 From: koniksedy Date: Thu, 16 Jul 2026 13:37:34 +0200 Subject: [PATCH 03/10] Nft::post optimized --- src/nft/nft.cc | 59 +++++++++++++++++++++++++------------------ src/nft/operations.cc | 8 ++++++ 2 files changed, 43 insertions(+), 24 deletions(-) diff --git a/src/nft/nft.cc b/src/nft/nft.cc index a257df157..cf994e658 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -651,17 +651,14 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols } StateSet result{}; - // visited contains visited configuration pairs of (positions, state). - // positions is a vector of reading head positions for each of n words in the input vector, - // where n is the number of levels in the NFT. - std::unordered_set, State>> visited; - std::stack, State>> stack; - for (const State state : states) { - const std::pair, State> initial_config{ std::vector(tape_symbols.size(), 0), state }; - stack.push({ initial_config }); - visited.insert(std::move(initial_config)); + // A search node is a full configuration: the reading-head position on each of the n input words (n = number + // of levels) plus the current state. `visited` deduplicates configurations so the search terminates even on + // cyclic inputs. Because unordered_set is node-based, pointers to its elements stay valid across further + // insertions, so the worklist carries plain pointers into `visited` instead of a second copy of each config. + using Config = std::pair, State>; + std::unordered_set visited; + std::stack stack; - } // End positions of reading heads after processing all symbols on each word. std::vector end_positions(tape_symbols.size(), 0); for (size_t i = 0; i < tape_symbols.size(); ++i) { @@ -674,20 +671,26 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols return (a == EPSILON || b == EPSILON) ? (a == EPSILON && b == EPSILON) : (a == b || a == DONT_CARE || b == DONT_CARE); }; - // Enqueue a configuration (reading-head positions + state) unless already visited. + // Enqueue a configuration (reading-head positions + state) unless already visited. The positions are moved + // straight into `visited` with a single hash lookup (emplace), and the worklist gets a pointer to the stored + // element, so the position vector is neither hashed twice nor copied into a separate worklist entry. auto enqueue = [&](std::vector next_positions, const State target) { - auto next_config = std::make_pair(std::move(next_positions), target); - if (!visited.contains(next_config)) { - visited.insert(next_config); - stack.push(std::move(next_config)); - } + const auto [it, inserted] = visited.emplace(std::move(next_positions), target); + if (inserted) { stack.push(&*it); } }; - // The main loop. + for (const State state : states) { enqueue(std::vector(tape_symbols.size(), 0), state); } + + // The main loop. post() is a pure reachability primitive with no notion of final states, so it cannot + // short-circuit on acceptance: it always explores the entire reachable configuration space and returns the + // full reached set, leaving any accept/prefix decision to the caller. This inability to stop early is the + // main reason the post()-based Nft::is_in_lang_by_levels is slower than is_in_lang_by_levels_repeat_symbol(). while (!stack.empty()) { - const auto [current_positions, current_state] = stack.top(); - const Level current_level = levels[current_state]; + const Config& current = *stack.top(); stack.pop(); + const std::vector& current_positions = current.first; + const State current_state = current.second; + const Level current_level = levels[current_state]; if (current_level == 0) { if (visited_zero_level_states != nullptr) { @@ -713,11 +716,13 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols // DONT_CARE for the trailing levels in JumpMode::AppendDontCares. const size_t stop_level_idx = target_level == 0 ? levels.num_of_levels : target_level; - // Consuming step: read (and advance past) one input symbol on each used level of the span. + // Consuming step: check that one input symbol can be read on each used level of the span. // A level with no input left cannot be read, so the step fails. Because exhaustion is // detected by the reading-head position (not by an EPSILON sentinel), a literal EPSILON - // symbol in an input word is matched and consumed here by an EPSILON transition. - std::vector next_positions{ current_positions }; + // symbol in an input word is matched and consumed here by an EPSILON transition. The + // position vector is copied only once the whole span is known to be readable, so a + // mismatching transition (the common case when scanning a state's outgoing symbols) costs + // no allocation. bool consumed = true; for (size_t level = current_level; level < stop_level_idx; ++level) { if (!use_tape[level]) { continue; } // Projected-out level: take the transition, read nothing. @@ -728,9 +733,15 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols consumed = false; break; } - ++next_positions[level]; } - if (consumed) { enqueue(std::move(next_positions), target); } + if (consumed) { + // Advance one reading head on each used level of the span. + std::vector next_positions{ current_positions }; + for (size_t level = current_level; level < stop_level_idx; ++level) { + if (use_tape[level]) { ++next_positions[level]; } + } + enqueue(std::move(next_positions), target); + } // Non-consuming step: an EPSILON transition may change state without reading any input. // This is what lets it be taken when a tape is exhausted; kept separate from the consuming diff --git a/src/nft/operations.cc b/src/nft/operations.cc index 3c0d8be8a..a5add4b37 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -967,6 +967,14 @@ bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool // (JumpMode::AppendDontCares). Membership is a thin consumer of the reachability primitive post(): the level // words are in the language iff a final state is reachable after consuming all of them; for a prefix query it // suffices to reach a final zero-level state after consuming any prefix (tracked via the visited states). + // + // This is inherently slower than is_in_lang_by_levels_repeat_symbol() above, and not just by a constant + // factor. post() is a pure reachability primitive with no notion of final states, so it cannot short-circuit + // on acceptance: it always explores the whole reachable configuration space, and only afterwards is the result + // intersected with `final` below. The dedicated algorithm returns the moment it reaches an accepting + // configuration. post() also has to deduplicate full (head-positions, state) configurations in a hash set to + // stay terminating on cyclic inputs, whereas the dedicated algorithm carries cheap word iterators in a plain + // worklist and needs no such set. StateSet visited_zero_level_states{}; StateSet* const visited_ptr = match_prefix ? &visited_zero_level_states : nullptr; const StateSet reached{ post(StateSet{ initial.begin(), initial.end() }, level_words, visited_ptr, true, jump_mode) }; From 20d0763d35911c3c244899fb5653bd52b59429a3 Mon Sep 17 00:00:00 2001 From: koniksedy Date: Thu, 16 Jul 2026 14:34:39 +0200 Subject: [PATCH 04/10] post shortcircuiting --- include/mata/nft/nft.hh | 12 +++++-- src/nft/nft.cc | 26 ++++++++++---- src/nft/operations.cc | 31 +++++++++------- tests/nft/nft-post.cc | 79 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 127 insertions(+), 21 deletions(-) diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 9a5b06503..3e6c14f3c 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -93,6 +93,7 @@ #include #include +#include #include #include #include @@ -731,9 +732,14 @@ public: * @param epsilon_closure_after Whether to perform epsilon closure after the post operation. * @param jump_mode 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. + * @param should_stop Optional early-exit hook, called as @c should_stop(state, reading_head_positions) for each + * reached configuration (a state together with the per-level reading-head positions) just before it is expanded. + * Returning true halts the search immediately and post() returns the states reached so far. This is a general + * stop condition: the caller decides what it means and captures whatever it needs in the closure. Leave empty + * for a full post. * @return Set of states reachable from the given set of states over the given words. */ - StateSet post(const StateSet& states, const std::vector& words, const BoolVector& use_level, StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const; + StateSet post(const StateSet& states, const std::vector& words, const BoolVector& use_level, StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol, const std::function&)>& should_stop = {}) const; /** * @brief Get the set of zero-level states reachable from the given set of zero-level @p states over the given @@ -752,8 +758,8 @@ public: * 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 Set of states reachable from the given set of states over the given words. */ - StateSet post(const StateSet& states, const std::vector& words, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol) const { - return post(states, words, BoolVector(words.size(), true), visited_zero_level_states, epsilon_closure_after, jump_mode); + StateSet post(const StateSet& states, const std::vector& words, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol, const std::function&)>& should_stop = {}) const { + return post(states, words, BoolVector(words.size(), true), visited_zero_level_states, epsilon_closure_after, jump_mode, should_stop); } /** diff --git a/src/nft/nft.cc b/src/nft/nft.cc index cf994e658..e883f0cff 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -635,19 +635,28 @@ StateSet Nft::post(const StateSet& states, const Symbol symbol, const Level symb return result; } -StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols, const BoolVector& use_tape, StateSet* const visited_zero_level_states, const bool epsilon_closure_after, const JumpMode jump_mode) const { +StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols, const BoolVector& use_tape, StateSet* const visited_zero_level_states, const bool epsilon_closure_after, const JumpMode jump_mode, const std::function&)>& should_stop) const { assert(std::all_of(states.begin(), states.end(), [&](State state) {return levels[state] == 0;})); if (delta.empty()) { + // With no transitions the only reachable configurations are the initial states with their reading heads + // still at the start, so the input is fully consumed iff every word is empty. + const bool all_input_consumed = + std::all_of(tape_symbols.begin(), tape_symbols.end(), [](const Word& word) { return word.empty(); }); + if (should_stop) { + // Honor the stop condition here too: with no transitions the only reachable configurations are the + // initial states with their reading heads still at the start. + const std::vector start_positions(tape_symbols.size(), 0); + for (const State state : states) { + if (should_stop(state, start_positions)) { return StateSet{ state }; } + } + } if (visited_zero_level_states != nullptr) { // Keep track of visited zero level states. // This is usefull for is_prefix_in_lang function. visited_zero_level_states->insert(states); } - if (std::all_of(tape_symbols.begin(), tape_symbols.end(), [](const Word& word) { return word.empty(); })) { - // If all tape symbols are empty (all words are epsilon), we can return existing zero level states. - return states; - } - return {}; + // If all tape symbols are empty (all words are epsilon), we can return existing zero level states. + return all_input_consumed ? states : StateSet{}; } StateSet result{}; @@ -692,6 +701,11 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols const State current_state = current.second; const Level current_level = levels[current_state]; + // Optional early-exit hook: a caller-supplied stop condition, evaluated for every reached configuration + // (state + reading-head positions) before it is expanded. Returning true halts the search and returns the + // states reached so far; the caller captures whatever it needs. A plain post (empty hook) skips this. + if (should_stop && should_stop(current_state, current_positions)) { return result; } + if (current_level == 0) { if (visited_zero_level_states != nullptr) { // Keep track of visited zero level states. diff --git a/src/nft/operations.cc b/src/nft/operations.cc index a5add4b37..ea3dd760e 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -966,19 +966,26 @@ bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool // General post()-based algorithm: the only one able to correctly interpret DONT_CARE-padded jumps // (JumpMode::AppendDontCares). Membership is a thin consumer of the reachability primitive post(): the level // words are in the language iff a final state is reachable after consuming all of them; for a prefix query it - // suffices to reach a final zero-level state after consuming any prefix (tracked via the visited states). + // suffices to reach a final zero-level state after consuming any prefix. // - // This is inherently slower than is_in_lang_by_levels_repeat_symbol() above, and not just by a constant - // factor. post() is a pure reachability primitive with no notion of final states, so it cannot short-circuit - // on acceptance: it always explores the whole reachable configuration space, and only afterwards is the result - // intersected with `final` below. The dedicated algorithm returns the moment it reaches an accepting - // configuration. post() also has to deduplicate full (head-positions, state) configurations in a hash set to - // stay terminating on cyclic inputs, whereas the dedicated algorithm carries cheap word iterators in a plain - // worklist and needs no such set. - StateSet visited_zero_level_states{}; - StateSet* const visited_ptr = match_prefix ? &visited_zero_level_states : nullptr; - const StateSet reached{ post(StateSet{ initial.begin(), initial.end() }, level_words, visited_ptr, true, jump_mode) }; - return final.intersects_with(reached) || (match_prefix && final.intersects_with(visited_zero_level_states)); + // post() has no notion of final states, so on its own it would explore the whole reachable configuration space. + // We give it a stop condition that fires the moment a final zero-level state is reached (with all input + // consumed, unless this is a prefix query) and records the hit in `accepted`; post() then stops at the first + // accepting configuration, just like is_in_lang_by_levels_repeat_symbol() above. A non-accepting query still has + // to exhaust the space (and dedup full (head-positions, state) configurations to stay terminating on cycles), + // which is the residual reason this path is slower than the dedicated one. + std::vector end_positions(level_words.size()); + for (size_t i{ 0 }; i < level_words.size(); ++i) { end_positions[i] = level_words[i].size(); } + bool accepted{ false }; + const auto stop_at_final = [&](const State state, const std::vector& reading_head_positions) { + if (levels[state] == 0 && (match_prefix || reading_head_positions == end_positions) && final.contains(state)) { + accepted = true; + return true; + } + return false; + }; + post(StateSet{ initial.begin(), initial.end() }, level_words, nullptr, true, jump_mode, stop_at_final); + return accepted; } std::pair Nft::get_word_for_path(const Run& run) const { diff --git a/tests/nft/nft-post.cc b/tests/nft/nft-post.cc index 86693d9dc..d5903a4e7 100644 --- a/tests/nft/nft-post.cc +++ b/tests/nft/nft-post.cc @@ -314,3 +314,82 @@ TEST_CASE("mata::nft::Nft::post(words) — epsilon_closure_after flag") { // is_in_lang_by_levels always closes after, so it still reaches the final state. CHECK(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ c } })); } + +// Exercises the post()-based, short-circuiting membership path taken by is_in_lang_by_levels() under +// JumpMode::AppendDontCares (the RepeatSymbol default uses the dedicated worklist algorithm instead). +TEST_CASE("mata::nft::Nft::is_in_lang_by_levels — post-based JumpMode::AppendDontCares path") { + SECTION("a DONT_CARE-padded jump accepts where RepeatSymbol would not") { + // A single jump q0 --a--> qf: both endpoints are level 0, so it spans (reads) both levels. + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State qf{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(qf); + n.delta.add(q0, a, qf); + + const std::vector a_a{ Word{ a }, Word{ a } }; + const std::vector a_b{ Word{ a }, Word{ b } }; + // Level 0 reads 'a'; level 1 reads 'a' under RepeatSymbol but DONT_CARE (any symbol) under AppendDontCares. + CHECK(n.is_in_lang_by_levels(a_a, false, JumpMode::RepeatSymbol)); + CHECK(n.is_in_lang_by_levels(a_a, false, JumpMode::AppendDontCares)); + CHECK_FALSE(n.is_in_lang_by_levels(a_b, false, JumpMode::RepeatSymbol)); + CHECK(n.is_in_lang_by_levels(a_b, false, JumpMode::AppendDontCares)); // DONT_CARE matches 'b'. + // The first (non-padded) level must still match exactly. + CHECK_FALSE(n.is_in_lang_by_levels(std::vector{ Word{ b }, Word{ a } }, false, JumpMode::AppendDontCares)); + } + + SECTION("short-circuit still follows a trailing epsilon to a final zero-level state") { + // ("a","c") lands on the non-final zero-level q2, which epsilon-moves to the final zero-level q3. + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(0) }; + const State q3{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q3); + n.delta.add(q0, a, q1); + n.delta.add(q1, c, q2); + n.delta.add(q2, EPSILON, q3); + + CHECK(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ c } }, false, JumpMode::AppendDontCares)); + CHECK_FALSE(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ d } }, false, JumpMode::AppendDontCares)); + } + + SECTION("prefix membership short-circuits on a final state before all input is consumed") { + // ("a","c") reaches the final zero-level q2; consuming further ("ab","cd") ends in the non-final q4. + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State q1{ n.add_state_with_level(1) }; + const State q2{ n.add_state_with_level(0) }; + const State q3{ n.add_state_with_level(1) }; + const State q4{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q2); + n.delta.add(q0, a, q1); + n.delta.add(q1, c, q2); + n.delta.add(q2, b, q3); + n.delta.add(q3, d, q4); + + const std::vector ab_cd{ Word{ a, b }, Word{ c, d } }; + // Full membership: ("ab","cd") ends in the non-final q4, only ("a","c") is accepted outright. + CHECK_FALSE(n.is_in_lang_by_levels(ab_cd, false, JumpMode::AppendDontCares)); + CHECK(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ c } }, false, JumpMode::AppendDontCares)); + // Prefix membership accepts because ("a","c") is an accepted prefix of ("ab","cd"). + CHECK(n.is_in_lang_prefix_by_levels(ab_cd, JumpMode::AppendDontCares)); + } + + SECTION("empty delta: an initial final state accepts the empty prefix (regression guard)") { + // No transitions => empty delta; q0 is both initial and final, so the language is { ("","") }. + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(q0); + + const std::vector empty_tuple{ Word{}, Word{} }; + const std::vector a_b{ Word{ a }, Word{ b } }; + CHECK(n.is_in_lang_by_levels(empty_tuple, false, JumpMode::AppendDontCares)); + CHECK_FALSE(n.is_in_lang_by_levels(a_b, false, JumpMode::AppendDontCares)); + // The empty prefix is always accepted by an initial final state, even with input still unconsumed. + CHECK(n.is_in_lang_prefix_by_levels(a_b, JumpMode::AppendDontCares)); + } +} From 93e237adc2d5b47bdae48ce5a0643f4179fa2860 Mon Sep 17 00:00:00 2001 From: koniksedy Date: Fri, 17 Jul 2026 10:08:30 +0200 Subject: [PATCH 05/10] Nft::post optimization + is_in_lang_by_levels dispatch --- examples/CMakeLists.txt | 3 + examples/bench_is_in_lang_by_levels.cc | 298 +++++++++++++++++++++++++ include/mata/nft/nft.hh | 33 +-- src/nft/nft.cc | 210 +++++++++++------ src/nft/operations.cc | 35 +-- tests/nft/nft-post.cc | 40 ++++ 6 files changed, 525 insertions(+), 94 deletions(-) create mode 100644 examples/bench_is_in_lang_by_levels.cc diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index e0d790343..2cb28b5e7 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -5,4 +5,7 @@ foreach(MATA_EXAMPLE ${MATA_EXAMPLES}) string(REPLACE ".cc" "" MATA_EXAMPLE_NAME "${MATA_EXAMPLE_NAME}") add_executable(${MATA_EXAMPLE_NAME} ${MATA_EXAMPLE}) target_link_libraries(${MATA_EXAMPLE_NAME} PRIVATE libmata) + if (${MATA_EXAMPLE_NAME} STREQUAL "bench_is_in_lang_by_levels") + target_compile_definitions(${MATA_EXAMPLE_NAME} PRIVATE MATA_BENCH_HAS_REPEAT_SYMBOL) + endif () endforeach() diff --git a/examples/bench_is_in_lang_by_levels.cc b/examples/bench_is_in_lang_by_levels.cc new file mode 100644 index 000000000..1ac3ad38e --- /dev/null +++ b/examples/bench_is_in_lang_by_levels.cc @@ -0,0 +1,298 @@ +// Benchmark harness for mata::nft::Nft::is_in_lang_by_levels(). +// +// Generates synthetic layered transducers with controllable word length (number of layers), +// branching factor (fan-out per layer), epsilon-closure chain depth (length of an epsilon-only +// detour inserted at each layer boundary), number of levels (tapes), and alphabet size. +// Then times is_in_lang_by_levels() on a handful of representative queries per scenario and +// prints one CSV row per (scenario, query, match_prefix) combination to stdout. +// +// This file is identical across the branches being compared (built independently against each +// branch's library) so the exact same automata and queries (same PRNG, same seed) are used on +// both sides, making the CSV outputs directly diffable. +// +// If MATA_BENCH_HAS_REPEAT_SYMBOL is defined (only true on the nft_post branch, which keeps the +// old hand-rolled worklist around as the free function mata::nft::is_in_lang_by_levels_repeat_symbol +// specifically for this kind of benchmarking), each query is additionally timed against that +// implementation in the same process, so the two can be compared without cross-run noise. + +#include "mata/nft/nft.hh" + +#include +#include +#include +#include +#include +#include +#include + +using namespace mata; +using namespace mata::nft; + +namespace { + +struct ScenarioParams { + std::string name; + size_t num_layers; + size_t branching; + size_t eps_chain_len; + size_t num_levels; + size_t alphabet_size; + unsigned seed; +}; + +struct GeneratedCase { + Nft nft; + std::vector accept_words; // accept_words[level] = symbols along the designated accepting path +}; + +GeneratedCase generate(const ScenarioParams& p) { + std::mt19937 rng(p.seed); + std::uniform_int_distribution sym_dist(0, static_cast(p.alphabet_size - 1)); + + Nft nft{ Nft::with_levels(p.num_levels) }; + const State start = nft.add_state(); + nft.initial.insert(start); + + std::vector accept_words(p.num_levels); + + std::vector frontier{ start }; + size_t designated_idx = 0; + + for (size_t layer = 0; layer < p.num_layers; ++layer) { + std::vector next_frontier; + next_frontier.reserve(p.branching); + for (size_t i = 0; i < p.branching; ++i) { next_frontier.push_back(nft.add_state()); } + + std::vector correct_symbols(p.num_levels); + for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { correct_symbols[lvl] = sym_dist(rng); } + const size_t next_designated_idx = std::uniform_int_distribution(0, next_frontier.size() - 1)(rng); + + for (size_t fi = 0; fi < frontier.size(); ++fi) { + for (size_t ti = 0; ti < next_frontier.size(); ++ti) { + std::vector word_parts(p.num_levels); + if (fi == designated_idx && ti == next_designated_idx) { + for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { word_parts[lvl] = { correct_symbols[lvl] }; } + } else { + for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { word_parts[lvl] = { sym_dist(rng) }; } + } + nft.insert_word_by_levels(frontier[fi], word_parts, next_frontier[ti]); + } + } + + if (p.eps_chain_len > 0) { + State prev = frontier[designated_idx]; + for (size_t k = 0; k < p.eps_chain_len; ++k) { + const State mid = nft.add_state(); + nft.delta.add(prev, EPSILON, mid); + prev = mid; + } + nft.delta.add(prev, EPSILON, next_frontier[next_designated_idx]); + } + + for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { accept_words[lvl].push_back(correct_symbols[lvl]); } + + frontier = std::move(next_frontier); + designated_idx = next_designated_idx; + } + + nft.final.insert(frontier[designated_idx]); + + return { std::move(nft), std::move(accept_words) }; +} + +struct Query { + std::string type; + std::vector level_words; +}; + +std::vector make_queries(const ScenarioParams& p, const std::vector& accept_words, std::mt19937& rng) { + std::vector queries; + std::uniform_int_distribution sym_dist(0, static_cast(p.alphabet_size - 1)); + + queries.push_back({ "exact", accept_words }); + + { + std::vector prefix(p.num_levels); + const size_t half = p.num_layers / 2; + for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { + prefix[lvl] = Word(accept_words[lvl].begin(), accept_words[lvl].begin() + half); + } + queries.push_back({ "prefix_half", prefix }); + } + + if (p.num_layers > 0) { + std::vector mutated = accept_words; + const size_t pos = p.num_layers / 2; + const size_t lvl = 0; + Symbol orig = mutated[lvl][pos]; + Symbol replacement; + do { replacement = sym_dist(rng); } while (replacement == orig); + mutated[lvl][pos] = replacement; + queries.push_back({ "mutate_middle", mutated }); + } + + { + std::vector empty(p.num_levels); + queries.push_back({ "empty", empty }); + } + + { + std::vector too_long = accept_words; + for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { too_long[lvl].push_back(sym_dist(rng)); } + queries.push_back({ "too_long", too_long }); + } + + return queries; +} + +std::vector make_scenarios() { + std::vector scenarios; + unsigned seed_counter = 1000; + + const ScenarioParams base{ "base", 30, 4, 0, 2, 64, 0 }; + auto add = [&](ScenarioParams s) { + s.seed = seed_counter++; + scenarios.push_back(std::move(s)); + }; + + add(base); + + for (size_t v : { (size_t)5, (size_t)30, (size_t)150, (size_t)600 }) { + ScenarioParams s = base; + s.num_layers = v; + s.name = "word_len_" + std::to_string(v); + add(s); + } + + for (size_t v : { (size_t)1, (size_t)2, (size_t)4, (size_t)8, (size_t)16 }) { + ScenarioParams s = base; + s.branching = v; + s.alphabet_size = std::max(64, v * 4); + s.name = "branching_" + std::to_string(v); + add(s); + } + + for (size_t v : { (size_t)0, (size_t)1, (size_t)5, (size_t)20, (size_t)100 }) { + ScenarioParams s = base; + s.eps_chain_len = v; + s.name = "eps_len_" + std::to_string(v); + add(s); + } + + for (size_t v : { (size_t)1, (size_t)2, (size_t)3, (size_t)5 }) { + ScenarioParams s = base; + s.num_levels = v; + s.name = "num_levels_" + std::to_string(v); + add(s); + } + + for (size_t v : { (size_t)4, (size_t)16, (size_t)64, (size_t)256 }) { + ScenarioParams s = base; + s.alphabet_size = v; + s.name = "alphabet_" + std::to_string(v); + add(s); + } + + { + ScenarioParams s{ "combined_large", 100, 8, 10, 2, 128, 0 }; + add(s); + } + { + ScenarioParams s{ "combined_heavy_branch_eps", 50, 20, 50, 3, 256, 0 }; + add(s); + } + { + ScenarioParams s{ "combined_long_thin", 800, 2, 3, 2, 32, 0 }; + add(s); + } + + return scenarios; +} + +// Adaptively picks a repeat count so the timed loop takes roughly target_ns. +struct TimingResult { + double avg_ns; + uint64_t repeats; + bool result; +}; + +template +TimingResult time_call(Fn&& fn) { + using clock = std::chrono::steady_clock; + constexpr double target_ns = 100'000'000.0; // ~100ms per measurement + constexpr uint64_t max_repeats = 2'000'000; + + const bool result = fn(); + + uint64_t repeats = 1; + double elapsed_ns = 0.0; + while (true) { + const auto t0 = clock::now(); + for (uint64_t i = 0; i < repeats; ++i) { + volatile bool r = fn(); + (void)r; + } + const auto t1 = clock::now(); + elapsed_ns = std::chrono::duration(t1 - t0).count(); + if (elapsed_ns >= target_ns || repeats >= max_repeats) { break; } + const double scale = target_ns / std::max(elapsed_ns, 1.0); + uint64_t next_repeats = static_cast(static_cast(repeats) * std::min(scale, 64.0)); + if (next_repeats <= repeats) { next_repeats = repeats * 2; } + repeats = std::min(next_repeats, max_repeats); + } + + return { elapsed_ns / static_cast(repeats), repeats, result }; +} + +} // namespace + +int main() { +#ifdef MATA_BENCH_HAS_REPEAT_SYMBOL + std::cout << "scenario,num_layers,branching,eps_chain_len,num_levels,alphabet_size," + "num_states,num_transitions,query_type,match_prefix," + "result_post,repeats_post,avg_ns_post," + "result_repeat,repeats_repeat,avg_ns_repeat\n"; +#else + std::cout << "scenario,num_layers,branching,eps_chain_len,num_levels,alphabet_size," + "num_states,num_transitions,query_type,match_prefix,result,repeats,avg_ns\n"; +#endif + + for (const ScenarioParams& p : make_scenarios()) { + GeneratedCase gc = generate(p); + std::mt19937 query_rng(p.seed * 7919u + 17); + std::vector queries = make_queries(p, gc.accept_words, query_rng); + const size_t num_states = gc.nft.num_of_states(); + const size_t num_transitions = gc.nft.delta.num_of_transitions(); + + for (const Query& q : queries) { + for (bool match_prefix : { false, true }) { + // Called with 2 args (no explicit jump_mode) so this compiles unchanged against master's + // older signature too; nft_post defaults the 3rd param to JumpMode::RepeatSymbol anyway, + // which is what is_in_lang_by_levels_repeat_symbol below is restricted to. + TimingResult post_result = time_call([&] { + return gc.nft.is_in_lang_by_levels(q.level_words, match_prefix); + }); +#ifdef MATA_BENCH_HAS_REPEAT_SYMBOL + TimingResult repeat_result = time_call([&] { + return mata::nft::is_in_lang_by_levels_repeat_symbol(gc.nft, q.level_words, match_prefix); + }); + std::cout << p.name << ',' << p.num_layers << ',' << p.branching << ',' << p.eps_chain_len << ',' + << p.num_levels << ',' << p.alphabet_size << ',' << num_states << ',' << num_transitions + << ',' << q.type << ',' << (match_prefix ? 1 : 0) << ',' + << (post_result.result ? 1 : 0) << ',' << post_result.repeats << ',' << std::fixed + << std::setprecision(2) << post_result.avg_ns << ',' + << (repeat_result.result ? 1 : 0) << ',' << repeat_result.repeats << ',' + << std::fixed << std::setprecision(2) << repeat_result.avg_ns << '\n'; +#else + std::cout << p.name << ',' << p.num_layers << ',' << p.branching << ',' << p.eps_chain_len << ',' + << p.num_levels << ',' << p.alphabet_size << ',' << num_states << ',' << num_transitions + << ',' << q.type << ',' << (match_prefix ? 1 : 0) << ',' << (post_result.result ? 1 : 0) + << ',' << post_result.repeats << ',' << std::fixed << std::setprecision(2) + << post_result.avg_ns << '\n'; +#endif + } + } + } + + return 0; +} diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 3e6c14f3c..02fc7efca 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -901,9 +901,9 @@ public: * That is, the function checks whether a tuple @p level_words (word1, word2, word3, ..., wordn) is in the regular * relation accepted by the transducer with 'n' levels (tracks). * - * For @c JumpMode::RepeatSymbol (the default), a dedicated worklist algorithm is used which is considerably - * faster than the general algorithm. For @c JumpMode::AppendDontCares, the check is delegated to the general - * @c post()-based implementation, which is the only one able to correctly interpret @c DONT_CARE-padded jumps. + * @c JumpMode::RepeatSymbol is handled by the dedicated hand-rolled worklist + * @c is_in_lang_by_levels_repeat_symbol() (a constant factor faster on that mode); the other jump modes go + * through the general @c post()-based algorithm, which short-circuits on the first accepting configuration. * * @param level_words The words to check. * @param match_prefix Whether to also match the prefix of the word. @@ -1448,6 +1448,23 @@ Nft invert_levels(const Nft& aut, JumpMode jump_mode = JumpMode::RepeatSymbol); */ Nft remove_epsilon(const Nft& aut, Symbol epsilon = EPSILON); +/** + * @brief Dedicated worklist check equivalent to Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol. + * + * This is the hand-rolled algorithm that predates the general post()-based membership check, and remains the + * production path for JumpMode::RepeatSymbol: Nft::is_in_lang_by_levels() delegates here for that jump mode (it is a + * constant factor faster there) and uses the post()-based algorithm for the other jump modes. + * + * @warning Correct only under JumpMode::RepeatSymbol. Unlike the post()-based check it keeps no visited set, so it + * must not be called on automata containing epsilon cycles (it may not terminate). + * + * @param aut The transducer whose relation is queried. @p level_words.size() must equal @c aut.levels.num_of_levels. + * @param level_words The tuple of per-level words to check. + * @param match_prefix Whether to also accept a prefix of @p level_words. + * @return @c true iff @p level_words (or a prefix of it, if @p match_prefix) is in the relation of @p aut. + */ +bool is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, bool match_prefix = false); + /** * @brief Projects out specified levels @p levels_to_project in the given transducer @p nft. * @@ -1556,16 +1573,6 @@ bool symbols_match(Symbol a, Symbol b); namespace std { std::ostream& operator<<(std::ostream& os, const mata::nft::Nft& nft); -template<> -struct hash, mata::nfa::State>> { - size_t operator()(const std::pair, mata::nfa::State>& p) const { - size_t h = std::hash{}(p.second); - for (auto v : p.first) { - h ^= std::hash{}(v) + 0x9e3779b9 + (h << 6) + (h >> 2); - } - return h; - } -}; } // namespace std. #endif /* MATA_NFT_HH_ */ diff --git a/src/nft/nft.cc b/src/nft/nft.cc index e883f0cff..dff67acd1 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -4,10 +4,14 @@ #include #include +#include #include +#include #include #include #include +#include +#include #include #include "mata/nfa/builder.hh" @@ -660,19 +664,74 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols } StateSet result{}; - // A search node is a full configuration: the reading-head position on each of the n input words (n = number - // of levels) plus the current state. `visited` deduplicates configurations so the search terminates even on - // cyclic inputs. Because unordered_set is node-based, pointers to its elements stay valid across further - // insertions, so the worklist carries plain pointers into `visited` instead of a second copy of each config. - using Config = std::pair, State>; - std::unordered_set visited; - std::stack stack; - - // End positions of reading heads after processing all symbols on each word. - std::vector end_positions(tape_symbols.size(), 0); - for (size_t i = 0; i < tape_symbols.size(); ++i) { - end_positions[i] = tape_symbols[i].size(); - } + + // End positions of the reading heads after all symbols on each word have been read. + std::vector end_positions(tape_symbols.size()); + for (size_t i = 0; i < tape_symbols.size(); ++i) { end_positions[i] = tape_symbols[i].size(); } + + // A search node is a full configuration: the reading-head position on each of the n input words (n = number of + // levels) plus the current state. The position part is a heavy vector that is heavily shared -- every + // state along an epsilon chain carries the identical positions (epsilon reads nothing), and a branching step + // hands the same positions to every target -- so each distinct positions vector is interned to a small uint32 + // id once. The search then works entirely on cheap (positions_id, state) pairs: the visited set keys on a + // single packed integer instead of re-hashing a vector on every step, and a non-consuming epsilon step reuses + // the source id with no vector work at all. Interned vectors live in position_ids; unordered_map nodes are + // stable across insertion, so id_to_positions can hold plain pointers to them. + std::unordered_map, uint32_t> position_ids; + std::vector*> id_to_positions; + auto intern = [&](const std::vector& positions) -> uint32_t { + const auto [it, inserted]{ position_ids.try_emplace(positions, static_cast(id_to_positions.size())) }; + if (inserted) { id_to_positions.push_back(&it->first); } + return it->second; + }; + const std::vector start_positions(tape_symbols.size(), 0); + const uint32_t start_id{ intern(start_positions) }; + const uint32_t end_id{ intern(end_positions) }; + + // `visited` deduplicates configurations (so the search terminates even on cyclic inputs), keyed on the packed + // (positions_id, state) pair. States comfortably fit in 32 bits (asserted), so the pair packs losslessly into + // one uint64 and membership is a scalar hash/compare -- no per-config vector work. + assert(num_of_states() <= std::numeric_limits::max()); + const auto pack = [](const uint32_t positions_id, const State state) -> uint64_t { + return (static_cast(positions_id) << 32) | static_cast(state); + }; + std::unordered_set visited; + + // Worklist. Its ordering only matters when short-circuiting (should_stop set). Then the search runs best-first, + // always expanding the configuration that has consumed the most input so far: an accepting exact match must + // consume every symbol, so "most consumed" is the greedy estimate of "closest to accepting". This beelines down + // the real input-consuming path (like a depth-first dive on the easy cases) yet defers epsilon transitions, which + // consume nothing -- so it neither plunges blindly down long epsilon chains the way a plain stack (DFS) does, nor + // sweeps the whole breadth the way a queue (BFS) does; both of those lose badly on opposite corners of the input + // space. Without a stop condition the entire reachable space is explored regardless of order, so the plain + // reachability sweep keeps a cheap LIFO stack. + const bool best_first{ static_cast(should_stop) }; + struct QueueItem { + size_t consumed; // total input symbols read so far; higher = closer to a full (accepting) match + uint32_t positions_id; + State state; + bool operator<(const QueueItem& other) const { return consumed < other.consumed; } // max-heap on consumed + }; + std::priority_queue best_first_queue; // used when best_first + std::vector> stack; // used otherwise + auto total_consumed = [](const std::vector& positions) { + size_t sum{ 0 }; + for (const size_t position : positions) { sum += position; } + return sum; + }; + + bool stopped{ false }; + // Registers a freshly reached configuration: deduplicates it, fires the optional stop hook (which may halt the + // whole search, matching a final state as soon as it is generated rather than when it is later expanded), and + // otherwise queues it for expansion. + auto discover = [&](const uint32_t positions_id, const State target, const std::vector& target_positions) { + if (stopped || !visited.insert(pack(positions_id, target)).second) { return; } + if (should_stop && should_stop(target, target_positions)) { stopped = true; return; } + if (best_first) { best_first_queue.push({ total_consumed(target_positions), positions_id, target }); } + else { stack.emplace_back(positions_id, target); } + }; + + for (const State state : states) { discover(start_id, state, start_positions); } // Two symbols match iff they are equal, or one is DONT_CARE and neither is EPSILON. // EPSILON matches only EPSILON. (The same relation as nft::symbols_match.) @@ -680,64 +739,56 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols return (a == EPSILON || b == EPSILON) ? (a == EPSILON && b == EPSILON) : (a == b || a == DONT_CARE || b == DONT_CARE); }; - // Enqueue a configuration (reading-head positions + state) unless already visited. The positions are moved - // straight into `visited` with a single hash lookup (emplace), and the worklist gets a pointer to the stored - // element, so the position vector is neither hashed twice nor copied into a separate worklist entry. - auto enqueue = [&](std::vector next_positions, const State target) { - const auto [it, inserted] = visited.emplace(std::move(next_positions), target); - if (inserted) { stack.push(&*it); } - }; - - for (const State state : states) { enqueue(std::vector(tape_symbols.size(), 0), state); } - - // The main loop. post() is a pure reachability primitive with no notion of final states, so it cannot - // short-circuit on acceptance: it always explores the entire reachable configuration space and returns the - // full reached set, leaving any accept/prefix decision to the caller. This inability to stop early is the - // main reason the post()-based Nft::is_in_lang_by_levels is slower than is_in_lang_by_levels_repeat_symbol(). - while (!stack.empty()) { - const Config& current = *stack.top(); - stack.pop(); - const std::vector& current_positions = current.first; - const State current_state = current.second; - const Level current_level = levels[current_state]; - // Optional early-exit hook: a caller-supplied stop condition, evaluated for every reached configuration - // (state + reading-head positions) before it is expanded. Returning true halts the search and returns the - // states reached so far; the caller captures whatever it needs. A plain post (empty hook) skips this. - if (should_stop && should_stop(current_state, current_positions)) { return result; } + while (!stopped && (best_first ? !best_first_queue.empty() : !stack.empty())) { + // Best-first (most input consumed) when short-circuiting, depth-first otherwise (see the worklist comment). + uint32_t current_positions_id; + State current_state; + if (best_first) { + const QueueItem top{ best_first_queue.top() }; + best_first_queue.pop(); + current_positions_id = top.positions_id; + current_state = top.state; + } else { + const std::pair top{ stack.back() }; + stack.pop_back(); + current_positions_id = top.first; + current_state = top.second; + } + const std::vector& current_positions{ *id_to_positions[current_positions_id] }; + const Level current_level{ levels[current_state] }; if (current_level == 0) { if (visited_zero_level_states != nullptr) { - // Keep track of visited zero level states. - // This is usefull for is_prefix_in_lang function. + // Keep track of visited zero level states. This is useful for the is_prefix_in_lang function. visited_zero_level_states->insert(current_state); } - if(current_positions == end_positions) { - // We reached a zero level state with all tape symbols processed. + if (current_positions_id == end_id) { + // A zero-level state reached with all tape symbols consumed. result.insert(current_state); if (!epsilon_closure_after) { - continue; // No need to explore further if we are not looking for epsilon closure. + continue; // No need to explore further unless we are computing the epsilon closure. } } } - for (const SymbolPost &symbol_post: delta[current_state]) { - const Symbol transition_symbol = symbol_post.symbol; - for (const State target: symbol_post.targets) { - const Level target_level = levels[target]; - // The (possibly jumping) transition reads one symbol on each level it spans: - // [current_level, stop_level_idx). On a jump the symbol is repeated, or replaced by - // DONT_CARE for the trailing levels in JumpMode::AppendDontCares. - const size_t stop_level_idx = target_level == 0 ? levels.num_of_levels : target_level; - - // Consuming step: check that one input symbol can be read on each used level of the span. - // A level with no input left cannot be read, so the step fails. Because exhaustion is - // detected by the reading-head position (not by an EPSILON sentinel), a literal EPSILON - // symbol in an input word is matched and consumed here by an EPSILON transition. The - // position vector is copied only once the whole span is known to be readable, so a - // mismatching transition (the common case when scanning a state's outgoing symbols) costs - // no allocation. - bool consumed = true; + // Expand one outgoing transition (possibly a jump) of the current state. + const StatePost& state_post{ delta[current_state] }; + auto expand = [&](const SymbolPost& symbol_post) { + const Symbol transition_symbol{ symbol_post.symbol }; + for (const State target : symbol_post.targets) { + const Level target_level{ levels[target] }; + // The (possibly jumping) transition reads one symbol on each level it spans: [current_level, + // stop_level_idx). On a jump the symbol is repeated, or replaced by DONT_CARE for the trailing + // levels in JumpMode::AppendDontCares. + const size_t stop_level_idx{ target_level == 0 ? levels.num_of_levels : target_level }; + + // Consuming step: check that one input symbol can be read on each used level of the span. A level + // with no input left cannot be read, so the step fails. Because exhaustion is detected by the + // reading-head position (not an EPSILON sentinel), a literal EPSILON symbol in an input word is + // matched and consumed here by an EPSILON transition. The position vector is built only once the + // whole span is known to be readable, so a mismatching transition costs no allocation. + bool consumed{ true }; for (size_t level = current_level; level < stop_level_idx; ++level) { if (!use_tape[level]) { continue; } // Projected-out level: take the transition, read nothing. const Symbol expected = (level == current_level || jump_mode != JumpMode::AppendDontCares) @@ -749,18 +800,47 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols } } if (consumed) { - // Advance one reading head on each used level of the span. std::vector next_positions{ current_positions }; for (size_t level = current_level; level < stop_level_idx; ++level) { if (use_tape[level]) { ++next_positions[level]; } } - enqueue(std::move(next_positions), target); + discover(intern(next_positions), target, next_positions); + if (stopped) { return; } } - // Non-consuming step: an EPSILON transition may change state without reading any input. - // This is what lets it be taken when a tape is exhausted; kept separate from the consuming - // step above so that a literal EPSILON in an input word can still be read there. - if (transition_symbol == EPSILON) { enqueue(current_positions, target); } + // Non-consuming step: an EPSILON transition may change state without reading any input. This is what + // lets it be taken when a tape is exhausted; kept separate from the consuming step above so that a + // literal EPSILON in an input word can still be read there. Positions are unchanged, so the source + // id is reused directly -- no vector work. + if (transition_symbol == EPSILON) { + discover(current_positions_id, target, current_positions); + if (stopped) { return; } + } + } + }; + + // Pick only the outgoing transitions that can possibly fire, instead of scanning them all. A non-consuming + // EPSILON move is always available; a consuming move must match the current level's input symbol, so only + // that exact symbol and DONT_CARE can fire -- both found by direct lookup (StatePost is symbol-sorted). The + // exceptions, where any symbol might match and so all must be scanned, are a projected-out current level or a + // literal DONT_CARE in the input word. + const bool current_used{ use_tape[current_level] != 0 }; + const bool current_has_symbol{ + current_used && current_positions[current_level] < end_positions[current_level] }; + const Symbol current_symbol{ + current_has_symbol ? tape_symbols[current_level][current_positions[current_level]] : EPSILON }; + if (!current_used || current_symbol == DONT_CARE) { + for (const SymbolPost& symbol_post : state_post) { + expand(symbol_post); + if (stopped) { break; } + } + } else { + if (const auto it = state_post.find(EPSILON); it != state_post.end()) { expand(*it); } + if (!stopped && current_has_symbol && current_symbol != EPSILON) { + if (const auto it = state_post.find(current_symbol); it != state_post.end()) { expand(*it); } + if (!stopped) { + if (const auto it = state_post.find(DONT_CARE); it != state_post.end()) { expand(*it); } + } } } } diff --git a/src/nft/operations.cc b/src/nft/operations.cc index ea3dd760e..cd4e0ce70 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -119,12 +119,14 @@ Nft reduce_size_by_simulation(const Nft& aut, StateRenaming& state_renaming) { return result; } - -/// Dedicated worklist algorithm for Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol (a jump transition -/// reads the same symbol on every level it spans). Kept as a separate, hand-rolled implementation because it is -/// considerably faster in this common case than the general post()-based algorithm, which additionally has to -/// support JumpMode::AppendDontCares. -bool is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, const bool match_prefix) { +} // Anonymous namespace. + +/// Dedicated worklist algorithm equivalent to Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol (a jump +/// transition reads the same symbol on every level it spans). This is the production path for that jump mode: +/// Nft::is_in_lang_by_levels() delegates here for JumpMode::RepeatSymbol and uses the general post()-based algorithm +/// for the other jump modes. See the header for the caveats (RepeatSymbol only; keeps no visited set, so it must not +/// run on automata with epsilon cycles). +bool mata::nft::is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, const bool match_prefix) { std::vector track_words_begins(aut.levels.num_of_levels); for (size_t track{ 0 }; track < aut.levels.num_of_levels; ++track) { track_words_begins[track] = level_words[track].begin(); @@ -239,7 +241,6 @@ bool is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& } return false; } -} Nft mata::nft::remove_epsilon(const Nft& aut, Symbol epsilon) { const size_t num_of_states{ aut.num_of_states() }; @@ -958,22 +959,24 @@ bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool throw std::invalid_argument("Invalid number of tracks. Expected " + std::to_string(levels.num_of_levels) + "."); } - if (jump_mode != JumpMode::AppendDontCares) { - // Dedicated worklist algorithm, considerably faster than the general post()-based algorithm below. + // JumpMode::RepeatSymbol (the common mode) is handled by the dedicated hand-rolled worklist: it is a constant + // factor faster than the general post()-based path on this mode. See is_in_lang_by_levels_repeat_symbol() for its + // one caveat (it keeps no visited set, so it must not run on automata with epsilon cycles). + if (jump_mode == JumpMode::RepeatSymbol) { return is_in_lang_by_levels_repeat_symbol(*this, level_words, match_prefix); } - // General post()-based algorithm: the only one able to correctly interpret DONT_CARE-padded jumps - // (JumpMode::AppendDontCares). Membership is a thin consumer of the reachability primitive post(): the level - // words are in the language iff a final state is reachable after consuming all of them; for a prefix query it - // suffices to reach a final zero-level state after consuming any prefix. + // Every other jump mode goes through the general post()-based algorithm (post() interprets jump_mode itself, + // including the DONT_CARE-padded jumps of JumpMode::AppendDontCares). Membership is a thin consumer of the + // reachability primitive post(): the level words are in the language iff a final state is reachable after + // consuming all of them; for a prefix query it suffices to reach a final zero-level state after consuming any + // prefix. // // post() has no notion of final states, so on its own it would explore the whole reachable configuration space. // We give it a stop condition that fires the moment a final zero-level state is reached (with all input // consumed, unless this is a prefix query) and records the hit in `accepted`; post() then stops at the first - // accepting configuration, just like is_in_lang_by_levels_repeat_symbol() above. A non-accepting query still has - // to exhaust the space (and dedup full (head-positions, state) configurations to stay terminating on cycles), - // which is the residual reason this path is slower than the dedicated one. + // accepting configuration. A non-accepting query still has to exhaust the space (and dedup full + // (head-positions, state) configurations to stay terminating on cycles). std::vector end_positions(level_words.size()); for (size_t i{ 0 }; i < level_words.size(); ++i) { end_positions[i] = level_words[i].size(); } bool accepted{ false }; diff --git a/tests/nft/nft-post.cc b/tests/nft/nft-post.cc index d5903a4e7..baa80ee34 100644 --- a/tests/nft/nft-post.cc +++ b/tests/nft/nft-post.cc @@ -393,3 +393,43 @@ TEST_CASE("mata::nft::Nft::is_in_lang_by_levels — post-based JumpMode::AppendD CHECK(n.is_in_lang_prefix_by_levels(a_b, JumpMode::AppendDontCares)); } } + +// The dedicated RepeatSymbol worklist (mata::nft::is_in_lang_by_levels_repeat_symbol) is no longer on the +// production path, so nothing else exercises it. This checks its results directly and cross-checks them against the +// post()-based Nft::is_in_lang_by_levels it is retained to be benchmarked against. +TEST_CASE("mata::nft::is_in_lang_by_levels_repeat_symbol — agrees with the post()-based membership check") { + // Cross-check full and prefix membership of a tuple against the production (post()-based) path. + auto agree = [](const Nft& n, const std::vector& words) { + for (const bool prefix : { false, true }) { + if (is_in_lang_by_levels_repeat_symbol(n, words, prefix) + != n.is_in_lang_by_levels(words, prefix, JumpMode::RepeatSymbol)) { + return false; + } + } + return true; + }; + + SECTION("level-by-level transitions") { + const Nft n{ make_ab_c() }; // Relation { ("ab", "c") }. + CHECK(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a, b }, Word{ c } })); + CHECK_FALSE(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a, b }, Word{ d } })); + CHECK(agree(n, std::vector{ Word{ a, b }, Word{ c } })); + CHECK(agree(n, std::vector{ Word{ a, b }, Word{ d } })); + CHECK(agree(n, std::vector{ Word{ a }, Word{ c } })); // Reaches a non-final zero-level state. + CHECK(agree(n, std::vector{ Word{}, Word{} })); + } + + SECTION("a jump transition, where RepeatSymbol reads the same symbol on every spanned level") { + Nft n{ Nft::with_levels(2) }; + const State q0{ n.add_state_with_level(0) }; + const State qf{ n.add_state_with_level(0) }; + n.initial.insert(q0); + n.final.insert(qf); + n.delta.add(q0, a, qf); // Jump q0 --a--> qf spanning both levels: both must read 'a'. + + CHECK(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a }, Word{ a } })); + CHECK_FALSE(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a }, Word{ b } })); + CHECK(agree(n, std::vector{ Word{ a }, Word{ a } })); + CHECK(agree(n, std::vector{ Word{ a }, Word{ b } })); + } +} From b13e0e7487bc43e04a073dc69e2007d3b7a378b0 Mon Sep 17 00:00:00 2001 From: koniksedy Date: Fri, 7 Aug 2026 14:49:33 +0200 Subject: [PATCH 06/10] is_in_lang_by_levels dispatcher --- examples/CMakeLists.txt | 8 +++--- examples/bench_is_in_lang_by_levels.cc | 5 ++++ include/mata/nft/nft.hh | 23 +++-------------- src/nft/operations.cc | 18 ++++++++------ tests/nft/nft-post.cc | 34 +++++++------------------- 5 files changed, 33 insertions(+), 55 deletions(-) diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 2cb28b5e7..5479d8cf8 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -3,9 +3,11 @@ foreach(MATA_EXAMPLE ${MATA_EXAMPLES}) file(RELATIVE_PATH MATA_EXAMPLE_REL "${CMAKE_CURRENT_SOURCE_DIR}" "${MATA_EXAMPLE}") string(REPLACE "/" "-" MATA_EXAMPLE_NAME "${MATA_EXAMPLE_REL}") string(REPLACE ".cc" "" MATA_EXAMPLE_NAME "${MATA_EXAMPLE_NAME}") - add_executable(${MATA_EXAMPLE_NAME} ${MATA_EXAMPLE}) - target_link_libraries(${MATA_EXAMPLE_NAME} PRIVATE libmata) + # Not built: is_in_lang_by_levels_repeat_symbol(), which it timed directly against MATA_BENCH_HAS_REPEAT_SYMBOL, + # is no longer a public symbol. Left on disk for its scenario/query generation code, not currently buildable. if (${MATA_EXAMPLE_NAME} STREQUAL "bench_is_in_lang_by_levels") - target_compile_definitions(${MATA_EXAMPLE_NAME} PRIVATE MATA_BENCH_HAS_REPEAT_SYMBOL) + continue() endif () + add_executable(${MATA_EXAMPLE_NAME} ${MATA_EXAMPLE}) + target_link_libraries(${MATA_EXAMPLE_NAME} PRIVATE libmata) endforeach() diff --git a/examples/bench_is_in_lang_by_levels.cc b/examples/bench_is_in_lang_by_levels.cc index 1ac3ad38e..b8f862b27 100644 --- a/examples/bench_is_in_lang_by_levels.cc +++ b/examples/bench_is_in_lang_by_levels.cc @@ -14,6 +14,11 @@ // old hand-rolled worklist around as the free function mata::nft::is_in_lang_by_levels_repeat_symbol // specifically for this kind of benchmarking), each query is additionally timed against that // implementation in the same process, so the two can be compared without cross-run noise. +// +// STALE: is_in_lang_by_levels_repeat_symbol() is no longer a public symbol (it moved into the anonymous +// namespace in operations.cc, reachable only via the dispatcher), so the MATA_BENCH_HAS_REPEAT_SYMBOL path +// below no longer compiles. Disconnected from examples/CMakeLists.txt rather than fixed up, since this +// benchmark is headed for deletion; kept on disk so the scenario/query generation doesn't need reinventing. #include "mata/nft/nft.hh" diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 02fc7efca..4cbf0896e 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -901,9 +901,9 @@ public: * That is, the function checks whether a tuple @p level_words (word1, word2, word3, ..., wordn) is in the regular * relation accepted by the transducer with 'n' levels (tracks). * - * @c JumpMode::RepeatSymbol is handled by the dedicated hand-rolled worklist - * @c is_in_lang_by_levels_repeat_symbol() (a constant factor faster on that mode); the other jump modes go - * through the general @c post()-based algorithm, which short-circuits on the first accepting configuration. + * @c JumpMode::RepeatSymbol is handled by an internal dedicated hand-rolled worklist (a constant factor faster on + * that mode); the other jump modes go through the general @c post()-based algorithm, which short-circuits on the + * first accepting configuration. * * @param level_words The words to check. * @param match_prefix Whether to also match the prefix of the word. @@ -1448,23 +1448,6 @@ Nft invert_levels(const Nft& aut, JumpMode jump_mode = JumpMode::RepeatSymbol); */ Nft remove_epsilon(const Nft& aut, Symbol epsilon = EPSILON); -/** - * @brief Dedicated worklist check equivalent to Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol. - * - * This is the hand-rolled algorithm that predates the general post()-based membership check, and remains the - * production path for JumpMode::RepeatSymbol: Nft::is_in_lang_by_levels() delegates here for that jump mode (it is a - * constant factor faster there) and uses the post()-based algorithm for the other jump modes. - * - * @warning Correct only under JumpMode::RepeatSymbol. Unlike the post()-based check it keeps no visited set, so it - * must not be called on automata containing epsilon cycles (it may not terminate). - * - * @param aut The transducer whose relation is queried. @p level_words.size() must equal @c aut.levels.num_of_levels. - * @param level_words The tuple of per-level words to check. - * @param match_prefix Whether to also accept a prefix of @p level_words. - * @return @c true iff @p level_words (or a prefix of it, if @p match_prefix) is in the relation of @p aut. - */ -bool is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, bool match_prefix = false); - /** * @brief Projects out specified levels @p levels_to_project in the given transducer @p nft. * diff --git a/src/nft/operations.cc b/src/nft/operations.cc index cd4e0ce70..d6f28dd3b 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -119,14 +119,17 @@ Nft reduce_size_by_simulation(const Nft& aut, StateRenaming& state_renaming) { return result; } -} // Anonymous namespace. /// Dedicated worklist algorithm equivalent to Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol (a jump /// transition reads the same symbol on every level it spans). This is the production path for that jump mode: /// Nft::is_in_lang_by_levels() delegates here for JumpMode::RepeatSymbol and uses the general post()-based algorithm -/// for the other jump modes. See the header for the caveats (RepeatSymbol only; keeps no visited set, so it must not -/// run on automata with epsilon cycles). -bool mata::nft::is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, const bool match_prefix) { +/// for the other jump modes. It has no reason to be called any other way, so it lives here as an internal helper +/// rather than a public API function: the dispatcher (Nft::is_in_lang_by_levels()) is what validates level_words +/// against aut.levels.num_of_levels, and the general post()-based path's edge-case handling (e.g. an empty delta) +/// likewise lives at that shared level rather than being duplicated here. +/// @warning Correct only under JumpMode::RepeatSymbol or JumpMode::NoJump. Unlike the post()-based check it keeps no visited set, so it +/// must not run on automata with epsilon cycles (it may not terminate). +bool is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, const bool match_prefix) { std::vector track_words_begins(aut.levels.num_of_levels); for (size_t track{ 0 }; track < aut.levels.num_of_levels; ++track) { track_words_begins[track] = level_words[track].begin(); @@ -241,6 +244,7 @@ bool mata::nft::is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::ve } return false; } +} // Anonymous namespace. Nft mata::nft::remove_epsilon(const Nft& aut, Symbol epsilon) { const size_t num_of_states{ aut.num_of_states() }; @@ -960,9 +964,9 @@ bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool } // JumpMode::RepeatSymbol (the common mode) is handled by the dedicated hand-rolled worklist: it is a constant - // factor faster than the general post()-based path on this mode. See is_in_lang_by_levels_repeat_symbol() for its - // one caveat (it keeps no visited set, so it must not run on automata with epsilon cycles). - if (jump_mode == JumpMode::RepeatSymbol) { + // factor faster than the general post()-based path on this mode. + // It has one problem, it keeps no visited set, so it must not run on automata with epsilon cycles. + if (jump_mode == JumpMode::RepeatSymbol || jump_mode == JumpMode::NoJump) { return is_in_lang_by_levels_repeat_symbol(*this, level_words, match_prefix); } diff --git a/tests/nft/nft-post.cc b/tests/nft/nft-post.cc index baa80ee34..e5880b100 100644 --- a/tests/nft/nft-post.cc +++ b/tests/nft/nft-post.cc @@ -394,29 +394,15 @@ TEST_CASE("mata::nft::Nft::is_in_lang_by_levels — post-based JumpMode::AppendD } } -// The dedicated RepeatSymbol worklist (mata::nft::is_in_lang_by_levels_repeat_symbol) is no longer on the -// production path, so nothing else exercises it. This checks its results directly and cross-checks them against the -// post()-based Nft::is_in_lang_by_levels it is retained to be benchmarked against. -TEST_CASE("mata::nft::is_in_lang_by_levels_repeat_symbol — agrees with the post()-based membership check") { - // Cross-check full and prefix membership of a tuple against the production (post()-based) path. - auto agree = [](const Nft& n, const std::vector& words) { - for (const bool prefix : { false, true }) { - if (is_in_lang_by_levels_repeat_symbol(n, words, prefix) - != n.is_in_lang_by_levels(words, prefix, JumpMode::RepeatSymbol)) { - return false; - } - } - return true; - }; - +// The dedicated RepeatSymbol worklist is an internal helper (anonymous namespace in operations.cc), reachable only +// through Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol (its default), which is exercised here directly. +TEST_CASE("mata::nft::Nft::is_in_lang_by_levels — JumpMode::RepeatSymbol dedicated worklist") { SECTION("level-by-level transitions") { const Nft n{ make_ab_c() }; // Relation { ("ab", "c") }. - CHECK(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a, b }, Word{ c } })); - CHECK_FALSE(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a, b }, Word{ d } })); - CHECK(agree(n, std::vector{ Word{ a, b }, Word{ c } })); - CHECK(agree(n, std::vector{ Word{ a, b }, Word{ d } })); - CHECK(agree(n, std::vector{ Word{ a }, Word{ c } })); // Reaches a non-final zero-level state. - CHECK(agree(n, std::vector{ Word{}, Word{} })); + CHECK(n.is_in_lang_by_levels(std::vector{ Word{ a, b }, Word{ c } })); + CHECK_FALSE(n.is_in_lang_by_levels(std::vector{ Word{ a, b }, Word{ d } })); + CHECK_FALSE(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ c } })); // Reaches a non-final zero-level state. + CHECK_FALSE(n.is_in_lang_by_levels(std::vector{ Word{}, Word{} })); } SECTION("a jump transition, where RepeatSymbol reads the same symbol on every spanned level") { @@ -427,9 +413,7 @@ TEST_CASE("mata::nft::is_in_lang_by_levels_repeat_symbol — agrees with the pos n.final.insert(qf); n.delta.add(q0, a, qf); // Jump q0 --a--> qf spanning both levels: both must read 'a'. - CHECK(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a }, Word{ a } })); - CHECK_FALSE(is_in_lang_by_levels_repeat_symbol(n, std::vector{ Word{ a }, Word{ b } })); - CHECK(agree(n, std::vector{ Word{ a }, Word{ a } })); - CHECK(agree(n, std::vector{ Word{ a }, Word{ b } })); + CHECK(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ a } })); + CHECK_FALSE(n.is_in_lang_by_levels(std::vector{ Word{ a }, Word{ b } })); } } From 4e58f23996e0a8213c23e2853287522a6206136c Mon Sep 17 00:00:00 2001 From: koniksedy Date: Fri, 7 Aug 2026 17:09:55 +0200 Subject: [PATCH 07/10] fix comments --- include/mata/nft/nft.hh | 110 ++++++++++++++++++++++++++++------------ src/nft/operations.cc | 82 +++++++++++++++++++++++++++--- tests/nft/nft.cc | 62 ++++++++++++++++++++++ 3 files changed, 214 insertions(+), 40 deletions(-) diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 4cbf0896e..715e789e8 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -681,7 +681,7 @@ public: /** * @brief Get the set of zero-level states reachable from the given set of zero-level @p states, * over the @p symbol on a given @p symbol_level. It does not care about symbols on other levels. - * + * * This is an optimized version of post methods for words. * * @param states Set of zero-level states to compute the post set from. @@ -715,13 +715,13 @@ public: } /** - * @brief Get the set of states reachable from the given set of @p states over the given vector of @p words + * @brief Get the set of states reachable from the given set of @p states over the given vector of @p words * (index corresponds to the level). Levels with the corresponding @p use_level set to false will be ignored. - * + * * This post uses a bitmask @p use_level to determine which levels to use. * Node: Use of @p use_level si similar to applying a projection of levels whose entries are set to true. * It is a general post method that is used by all of its overloads. - * + * * @param states Set of states to compute the post set from. * @param words Vector of words (w_1, w_2, ..., w_num_of_levels) to compute the post set for. * The index of the word in the vector corresponds to the level (tape) on which the word is used. @@ -739,14 +739,16 @@ public: * for a full post. * @return Set of states reachable from the given set of states over the given words. */ - StateSet post(const StateSet& states, const std::vector& words, const BoolVector& use_level, StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol, const std::function&)>& should_stop = {}) const; + StateSet post(const StateSet& states, const std::vector& words, const BoolVector& use_level, + StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, + JumpMode jump_mode = JumpMode::RepeatSymbol, const std::function&)>& should_stop = {}) const; /** * @brief Get the set of zero-level states reachable from the given set of zero-level @p states over the given * vector of @p words (index corresponds to the level). All words on all levels are used and have to be specified. - * + * * This post uses all words on all levels. - * + * * @param states Set of zero-level states to compute the post set from. * @param words Vector of words (w_1, w_2, ..., w_num_of_levels) to compute the post set for. * The index of the word in the vector corresponds to the level (tape) on which the word is used. @@ -758,16 +760,19 @@ public: * 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 Set of states reachable from the given set of states over the given words. */ - StateSet post(const StateSet& states, const std::vector& words, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol, const std::function&)>& should_stop = {}) const { + StateSet post(const StateSet& states, const std::vector& words, StateSet* visited_zero_level_states = nullptr, + const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol, + const std::function&)>& should_stop = {}) const + { return post(states, words, BoolVector(words.size(), true), visited_zero_level_states, epsilon_closure_after, jump_mode, should_stop); } /** * @brief Get the set of zero-level states reachable from the given zero-level @p state over the given * vector of @p words (index corresponds to the level). All words on all levels are used and have to be specified. - * + * * This post uses all words on all levels. - * + * * @param state Zero-level state to compute the post set from. * @param words Vector of words (w_1, w_2, ..., w_num_of_levels) to compute the post set for. * The index of the word in the vector corresponds to the level (tape) on which the word is used. @@ -779,19 +784,21 @@ public: * 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 Set of states reachable from the given set of states over the given words. */ - StateSet post(const State state, const std::vector& words, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol) const { + StateSet post(const State state, const std::vector& words, StateSet* visited_zero_level_states = nullptr, + const bool epsilon_closure_after = true, const JumpMode jump_mode = JumpMode::RepeatSymbol) const + { return post(StateSet{ state }, words, BoolVector(words.size(), true), visited_zero_level_states, epsilon_closure_after, jump_mode); } /** * @brief Get the set of zero-level states reachable from the given set of @p states over the given - * vector of @p words. The levels of the words are specified in @p word_levels vector. The post is computed only - * for the words that have a level corresponding to the level of the state. Levels not specified in @p word_levels + * vector of @p words. The levels of the words are specified in @p word_levels vector. The post is computed only + * for the words that have a level corresponding to the level of the state. Levels not specified in @p word_levels * are ignored (projected-out) - * + * * This post uses a vector @p word_levels to specify levels of used words. * Note: Use of @p word_levels is similar to applying a projection of levels from the vector @p word_levels. - * + * * @param states Set of zero-level states to compute the post set from. * @param words Vector of words to compute the post set for. * @param word_levels Vector of levels corresponding to the words in @p words (has to be the same size as @p words). @@ -804,17 +811,18 @@ public: * of @c DONT_CARE symbols. * @return Set of states reachable from the given set of states over the given words. */ - StateSet post(const StateSet& states, const std::vector& words, const std::vector& word_levels, StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const; + StateSet post(const StateSet& states, const std::vector& words, const std::vector& word_levels, + StateSet* visited_zero_level_states = nullptr, bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const; /** * @brief Get the set of zero-level states reachable from the given zero-level @p state over the given - * vector of @p words. The levels of the words are specified in @p word_levels vector. The post is computed only - * for the words that have a level corresponding to the level of the state. Levels not specified in @p word_levels + * vector of @p words. The levels of the words are specified in @p word_levels vector. The post is computed only + * for the words that have a level corresponding to the level of the state. Levels not specified in @p word_levels * are ignored (projected-out). - * + * * This post uses a vector @p word_levels to specify levels of used words. * Note: Use of @p word_levels is similar to applying a projection of levels from the vector @p word_levels. - * + * * @param state Zero-level state to compute the post set from. * @param words Vector of words to compute the post set for. * @param word_levels Vector of levels corresponding to the words in @p words (has to be the same size as @p words). @@ -827,7 +835,9 @@ public: * of @c DONT_CARE symbols. * @return Set of states reachable from the given set of states over the given words. */ - StateSet post(const State state, const std::vector& words, const std::vector& word_levels, StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const { + StateSet post(const State state, const std::vector& words, const std::vector& word_levels, + StateSet* visited_zero_level_states = nullptr, const bool epsilon_closure_after = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const + { return post(StateSet{ state }, words, word_levels, visited_zero_level_states, epsilon_closure_after, jump_mode); } @@ -846,9 +856,14 @@ public: * 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. Dispatches to the dedicated fast algorithm for @c JumpMode::RepeatSymbol and * to the general @c post()-based algorithm otherwise. + * @param has_epsilon_cycles Whether the automaton has a cycle of epsilon transitions. + * + * @warning If @p has_epsilon_cycles is unknown, it is recommended to set it to @c true. + * if it is set to @c false and the automaton does have an epsilon cycle, the query will loop forever. + * * @return @c true if @p run is in the language of the automaton, @c false otherwise. */ - bool is_in_lang(const Run& run, bool match_prefix = false, JumpMode jump_mode = JumpMode::RepeatSymbol) const; + bool is_in_lang(const Run& run, bool match_prefix = false, JumpMode jump_mode = JumpMode::RepeatSymbol, bool has_epsilon_cycles = false) const; bool is_in_lang(const Run&, bool, bool) const = delete; /** @@ -859,10 +874,16 @@ public: * @param jump_mode 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. + * @param has_epsilon_cycles Whether the automaton has a cycle of epsilon transitions. + * + * @warning If @p has_epsilon_cycles is unknown, it is recommended to set it to @c true. + * if it is set to @c false and the automaton does have an epsilon cycle, the query will loop forever. + * * @return @c true if @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang(const Word& word, const bool match_prefix = false, const JumpMode jump_mode = JumpMode::RepeatSymbol) const { - return is_in_lang(Run{ word, {} }, match_prefix, jump_mode); + bool is_in_lang(const Word& word, const bool match_prefix = false, + const JumpMode jump_mode = JumpMode::RepeatSymbol, const bool has_epsilon_cycles = false) const { + return is_in_lang(Run{ word, {} }, match_prefix, jump_mode, has_epsilon_cycles); } bool is_in_lang(const Word& word, bool, bool) const = delete; @@ -873,10 +894,16 @@ public: * @param jump_mode 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. + * @param has_epsilon_cycles Whether the automaton has a cycle of epsilon transitions. + * + * @warning If @p has_epsilon_cycles is unknown, it is recommended to set it to @c true. + * if it is set to @c false and the automaton does have an epsilon cycle, the query will loop forever. + * * @return @c true if the prefix of @p run is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_prefix(const Run& run, JumpMode jump_mode = JumpMode::RepeatSymbol) const { - return is_in_lang(run, true, jump_mode); + bool is_in_lang_prefix(const Run& run, JumpMode jump_mode = JumpMode::RepeatSymbol, + const bool has_epsilon_cycles = false) const { + return is_in_lang(run, true, jump_mode, has_epsilon_cycles); } bool is_in_lang_prefix(const Run&, bool) const = delete; @@ -888,10 +915,16 @@ public: * @param jump_mode 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. + * @param has_epsilon_cycles Whether the automaton has a cycle of epsilon transitions. + * + * @warning If @p has_epsilon_cycles is unknown, it is recommended to set it to @c true. + * if it is set to @c false and the automaton does have an epsilon cycle, the query will loop forever. + * * @return @c true if the prefix of @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_prefix(const Word& word, JumpMode jump_mode = JumpMode::RepeatSymbol) const { - return is_in_lang_prefix(Run{ word, {} }, jump_mode); + bool is_in_lang_prefix(const Word& word, JumpMode jump_mode = JumpMode::RepeatSymbol, + const bool has_epsilon_cycles = false) const { + return is_in_lang_prefix(Run{ word, {} }, jump_mode, has_epsilon_cycles); } bool is_in_lang_prefix(const Word&, bool) const = delete; @@ -910,9 +943,15 @@ public: * @param jump_mode 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. + * @param has_epsilon_cycles Whether the automaton has a cycle of epsilon transitions + * + * @warning If @p has_epsilon_cycles is unknown, it is recommended to set it to @c true. + * if it is set to @c false and the automaton does have an epsilon cycle, the query will loop forever. + * * @return @c true if @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_by_levels(const std::vector& level_words, bool match_prefix = false, JumpMode jump_mode = JumpMode::RepeatSymbol) const; + bool is_in_lang_by_levels(const std::vector& level_words, bool match_prefix = false, + JumpMode jump_mode = JumpMode::RepeatSymbol, bool has_epsilon_cycles = false) const; /** * @brief Checks whether the prefix of @p level_words is in the language of the transducer. @@ -924,10 +963,17 @@ public: * @param jump_mode 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. + * @param has_epsilon_cycles Whether the automaton has a cycle of epsilon transitions. + * + * @warning If @p has_epsilon_cycles is unknown, it is recommended to set it to @c true. + * if it is set to @c false and the automaton does have an epsilon cycle, the query will loop forever. + * * @return @c true if the prefix of @p word is in the language of the automaton, @c false otherwise. */ - bool is_in_lang_prefix_by_levels(const std::vector& level_words, JumpMode jump_mode = JumpMode::RepeatSymbol) const { - return is_in_lang_by_levels(level_words, true, jump_mode); + bool is_in_lang_prefix_by_levels(const std::vector& level_words, + JumpMode jump_mode = JumpMode::RepeatSymbol, + const bool has_epsilon_cycles = false) const { + return is_in_lang_by_levels(level_words, true, jump_mode, has_epsilon_cycles); } /** @@ -1190,7 +1236,7 @@ Nft compose(const Nft& lhs, const Nft& rhs, * - the synchronizing level (possibly missing if project_out_sync_levels is true) * - levels of `lhs` after its synvhronization level * - levels of `rhs` after its synvhronization level - * + * * @param[in] lhs First transducer to compose. * @param[in] rhs Second transducer to compose. * @param[in] lhs_sync_level The synchronization level of the @p lhs. diff --git a/src/nft/operations.cc b/src/nft/operations.cc index d6f28dd3b..5f16d8fc3 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -120,6 +120,71 @@ Nft reduce_size_by_simulation(const Nft& aut, StateRenaming& state_renaming) { return result; } +/// Get targets of the epsilon transitions of @p state. +[[maybe_unused]] const StateSet* epsilon_targets(const Nft& aut, const State state) { + static_assert(nft::EPSILON == Limits::max_symbol, "epsilon is expected to sort last in a state post"); + const StatePost& state_post{ aut.delta[state] }; + if (state_post.empty() || state_post.back().symbol != nft::EPSILON) { + return nullptr; + } + return &state_post.back().targets; +} + +/// True whether the automaton has a cycle of epsilon transitions, false otherwise. +[[maybe_unused]] bool has_epsilon_cycle(const Nft& aut) { + const size_t num_of_states{ aut.num_of_states() }; + std::vector epsilon_sources{}; + std::vector num_of_epsilon_predecessors{}; + for (State source{ 0 }; source < num_of_states; ++source) { + const StateSet* const targets{ epsilon_targets(aut, source) }; + if (targets == nullptr) { + continue; + } + if (num_of_epsilon_predecessors.empty()) { + num_of_epsilon_predecessors.assign(num_of_states, 0); + } + epsilon_sources.push_back(source); + for (const State target : *targets) { + ++num_of_epsilon_predecessors[target]; + } + } + if (epsilon_sources.empty()) { + // No epsilon transitions, hence no epsilon cycle. + return false; + } + + // A cycle lies entirely within the states an epsilon transition starts from or leads to. + // Peeling starts from those of them that have nothing to peel away first. + size_t num_of_states_on_epsilon_transitions{ 0 }; + for (State state{ 0 }; state < num_of_states; ++state) { + if (num_of_epsilon_predecessors[state] != 0) { + ++num_of_states_on_epsilon_transitions; + } + } + std::vector peelable{}; + for (const State source : epsilon_sources) { + if (num_of_epsilon_predecessors[source] == 0) { + ++num_of_states_on_epsilon_transitions; + peelable.push_back(source); + } + } + + size_t num_of_peeled_states{ 0 }; + while (!peelable.empty()) { + const State state{ peelable.back() }; + peelable.pop_back(); + ++num_of_peeled_states; + if (const StateSet* const targets{ epsilon_targets(aut, state) }; targets != nullptr) { + for (const State target : *targets) { + if (--num_of_epsilon_predecessors[target] == 0) { + peelable.push_back(target); + } + } + } + } + return num_of_peeled_states != num_of_states_on_epsilon_transitions; +} + /// Dedicated worklist algorithm equivalent to Nft::is_in_lang_by_levels() under JumpMode::RepeatSymbol (a jump /// transition reads the same symbol on every level it spans). This is the production path for that jump mode: /// Nft::is_in_lang_by_levels() delegates here for JumpMode::RepeatSymbol and uses the general post()-based algorithm @@ -127,8 +192,8 @@ Nft reduce_size_by_simulation(const Nft& aut, StateRenaming& state_renaming) { /// rather than a public API function: the dispatcher (Nft::is_in_lang_by_levels()) is what validates level_words /// against aut.levels.num_of_levels, and the general post()-based path's edge-case handling (e.g. an empty delta) /// likewise lives at that shared level rather than being duplicated here. -/// @warning Correct only under JumpMode::RepeatSymbol or JumpMode::NoJump. Unlike the post()-based check it keeps no visited set, so it -/// must not run on automata with epsilon cycles (it may not terminate). +/// @warning Correct only under JumpMode::RepeatSymbol or JumpMode::NoJump, and only on an automaton without epsilon +/// cycles. This search keeps no visited set. That is what makes it fast. bool is_in_lang_by_levels_repeat_symbol(const Nft& aut, const std::vector& level_words, const bool match_prefix) { std::vector track_words_begins(aut.levels.num_of_levels); for (size_t track{ 0 }; track < aut.levels.num_of_levels; ++track) { @@ -954,19 +1019,20 @@ Nft nft::invert_levels(const Nft& aut, const JumpMode jump_mode) { return aut_inv; } -bool Nft::is_in_lang(const Run& run, const bool match_prefix, const JumpMode jump_mode) const { - return is_in_lang_by_levels(mk_level_word_from_word(run.word), match_prefix, jump_mode); +bool Nft::is_in_lang(const Run& run, const bool match_prefix, const JumpMode jump_mode, const bool has_epsilon_cycles) const { + return is_in_lang_by_levels(mk_level_word_from_word(run.word), match_prefix, jump_mode, has_epsilon_cycles); } -bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool match_prefix, const JumpMode jump_mode) const { +bool Nft::is_in_lang_by_levels(const std::vector& level_words, const bool match_prefix, const JumpMode jump_mode, const bool has_epsilon_cycles) const { if (level_words.size() != levels.num_of_levels) { throw std::invalid_argument("Invalid number of tracks. Expected " + std::to_string(levels.num_of_levels) + "."); } // JumpMode::RepeatSymbol (the common mode) is handled by the dedicated hand-rolled worklist: it is a constant - // factor faster than the general post()-based path on this mode. - // It has one problem, it keeps no visited set, so it must not run on automata with epsilon cycles. - if (jump_mode == JumpMode::RepeatSymbol || jump_mode == JumpMode::NoJump) { + // factor faster than the general post()-based path on this mode. What buys that speed is keeping no visited set. + // The caller is trusted on the absence of epsilon cycles, it would be too expensive to check for them every time. + if ((jump_mode == JumpMode::RepeatSymbol || jump_mode == JumpMode::NoJump) && !has_epsilon_cycles) { + assert(!has_epsilon_cycle(*this)); return is_in_lang_by_levels_repeat_symbol(*this, level_words, match_prefix); } diff --git a/tests/nft/nft.cc b/tests/nft/nft.cc index 4737ffd4b..807f5c0a2 100644 --- a/tests/nft/nft.cc +++ b/tests/nft/nft.cc @@ -2475,6 +2475,68 @@ TEST_CASE("mata::nft::Nft::is_in_lang[_prefix][_by_levels]()") { CHECK_THROWS_AS(nft.is_in_lang_prefix(Word{ 'a', 'b' }), std::invalid_argument); } + + SECTION("epsilon cycle") { + // The epsilon cycle 0 -> 1 -> 2 -> 0 reads nothing, so the dedicated JumpMode::RepeatSymbol worklist, which + // makes progress only by reading, cannot terminate on this automaton: every query has to declare the cycle + // (the last argument) to be answered by the general post()-based algorithm instead. + constexpr bool HAS_EPSILON_CYCLES{ true }; + nft.add_state_with_level(0, 0); + nft.add_state_with_level(1, 1); + nft.add_state_with_level(2, 2); + nft.add_state_with_level(3, 0); + nft.initial.insert(0); + nft.final.insert(3); + nft.delta.add(0, EPSILON, 1); + nft.delta.add(1, EPSILON, 2); + nft.delta.add(2, EPSILON, 0); + nft.delta.add(0, 'a', 1); + nft.delta.add(1, 'b', 2); + nft.delta.add(2, 'c', 3); + + CHECK(nft.is_in_lang_by_levels({ { 'a' }, { 'b' }, { 'c' } }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(nft.is_in_lang(Word{ 'a', 'b', 'c' }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(nft.is_in_lang_prefix_by_levels({ { 'a' }, { 'b' }, { 'c' } }, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + // The rejecting answers are the ones that have to exhaust the whole search space with the cycle in it. + CHECK(not nft.is_in_lang_by_levels({ { 'a' }, { 'b' }, { 'd' } }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(not nft.is_in_lang_by_levels({ { 'a' }, { 'b' }, {} }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(not nft.is_in_lang_by_levels({ {}, {}, {} }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(not nft.is_in_lang_prefix_by_levels({ { 'a' }, { 'b' }, { 'd' } }, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + // Going around the cycle up to state 2 reads nothing, so 'c' alone is read on the last level. + CHECK(nft.is_in_lang_prefix_by_levels({ { 'a' }, { 'd' }, { 'c' } }, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + + // The automaton has no jump transitions, so every jump mode must give the same answers. + for (const std::vector& level_words : + std::vector>{ { { 'a' }, { 'b' }, { 'c' } }, { { 'a' }, { 'b' }, { 'd' } }, + { { 'a' }, { 'd' }, { 'c' } }, { { 'a' }, { 'b' }, {} }, + { {}, {}, {} } }) { + for (const bool match_prefix : { false, true }) { + CHECK( + nft.is_in_lang_by_levels(level_words, match_prefix, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES) == + nft.is_in_lang_by_levels(level_words, match_prefix, JumpMode::AppendDontCares, HAS_EPSILON_CYCLES) + ); + } + } + } + + SECTION("epsilon self-loop") { + constexpr bool HAS_EPSILON_CYCLES{ true }; + nft.add_state_with_level(0, 0); + nft.add_state_with_level(1, 1); + nft.add_state_with_level(2, 2); + nft.add_state_with_level(3, 0); + nft.initial.insert(0); + nft.final.insert(3); + nft.delta.add(0, EPSILON, 0); // The shortest cycle there is, and it reads nothing. + nft.delta.add(0, 'a', 1); + nft.delta.add(1, 'b', 2); + nft.delta.add(2, 'c', 3); + + CHECK(nft.is_in_lang_by_levels({ { 'a' }, { 'b' }, { 'c' } }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(not nft.is_in_lang_by_levels({ { 'a' }, { 'b' }, { 'd' } }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(not nft.is_in_lang_by_levels({ {}, {}, {} }, false, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + CHECK(not nft.is_in_lang_prefix_by_levels({ { 'd' }, { 'b' }, { 'c' } }, JumpMode::RepeatSymbol, HAS_EPSILON_CYCLES)); + } } TEST_CASE("mata::nft::fw-direct-simulation()") { // {{{ From dede2b777bbd4cf5a9f02f26193d3806f94c3544 Mon Sep 17 00:00:00 2001 From: koniksedy Date: Fri, 7 Aug 2026 17:21:57 +0200 Subject: [PATCH 08/10] rebase --- src/nft/nft.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/src/nft/nft.cc b/src/nft/nft.cc index dff67acd1..fbbec62b6 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -5,6 +5,7 @@ #include #include #include +#include #include #include #include From 9a283b5639e2fac8f266bcaa43b956ebc17a9b99 Mon Sep 17 00:00:00 2001 From: koniksedy Date: Fri, 7 Aug 2026 17:24:04 +0200 Subject: [PATCH 09/10] remove benchmarking --- examples/CMakeLists.txt | 5 - examples/bench_is_in_lang_by_levels.cc | 303 ------------------------- 2 files changed, 308 deletions(-) delete mode 100644 examples/bench_is_in_lang_by_levels.cc diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 5479d8cf8..e0d790343 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -3,11 +3,6 @@ foreach(MATA_EXAMPLE ${MATA_EXAMPLES}) file(RELATIVE_PATH MATA_EXAMPLE_REL "${CMAKE_CURRENT_SOURCE_DIR}" "${MATA_EXAMPLE}") string(REPLACE "/" "-" MATA_EXAMPLE_NAME "${MATA_EXAMPLE_REL}") string(REPLACE ".cc" "" MATA_EXAMPLE_NAME "${MATA_EXAMPLE_NAME}") - # Not built: is_in_lang_by_levels_repeat_symbol(), which it timed directly against MATA_BENCH_HAS_REPEAT_SYMBOL, - # is no longer a public symbol. Left on disk for its scenario/query generation code, not currently buildable. - if (${MATA_EXAMPLE_NAME} STREQUAL "bench_is_in_lang_by_levels") - continue() - endif () add_executable(${MATA_EXAMPLE_NAME} ${MATA_EXAMPLE}) target_link_libraries(${MATA_EXAMPLE_NAME} PRIVATE libmata) endforeach() diff --git a/examples/bench_is_in_lang_by_levels.cc b/examples/bench_is_in_lang_by_levels.cc deleted file mode 100644 index b8f862b27..000000000 --- a/examples/bench_is_in_lang_by_levels.cc +++ /dev/null @@ -1,303 +0,0 @@ -// Benchmark harness for mata::nft::Nft::is_in_lang_by_levels(). -// -// Generates synthetic layered transducers with controllable word length (number of layers), -// branching factor (fan-out per layer), epsilon-closure chain depth (length of an epsilon-only -// detour inserted at each layer boundary), number of levels (tapes), and alphabet size. -// Then times is_in_lang_by_levels() on a handful of representative queries per scenario and -// prints one CSV row per (scenario, query, match_prefix) combination to stdout. -// -// This file is identical across the branches being compared (built independently against each -// branch's library) so the exact same automata and queries (same PRNG, same seed) are used on -// both sides, making the CSV outputs directly diffable. -// -// If MATA_BENCH_HAS_REPEAT_SYMBOL is defined (only true on the nft_post branch, which keeps the -// old hand-rolled worklist around as the free function mata::nft::is_in_lang_by_levels_repeat_symbol -// specifically for this kind of benchmarking), each query is additionally timed against that -// implementation in the same process, so the two can be compared without cross-run noise. -// -// STALE: is_in_lang_by_levels_repeat_symbol() is no longer a public symbol (it moved into the anonymous -// namespace in operations.cc, reachable only via the dispatcher), so the MATA_BENCH_HAS_REPEAT_SYMBOL path -// below no longer compiles. Disconnected from examples/CMakeLists.txt rather than fixed up, since this -// benchmark is headed for deletion; kept on disk so the scenario/query generation doesn't need reinventing. - -#include "mata/nft/nft.hh" - -#include -#include -#include -#include -#include -#include -#include - -using namespace mata; -using namespace mata::nft; - -namespace { - -struct ScenarioParams { - std::string name; - size_t num_layers; - size_t branching; - size_t eps_chain_len; - size_t num_levels; - size_t alphabet_size; - unsigned seed; -}; - -struct GeneratedCase { - Nft nft; - std::vector accept_words; // accept_words[level] = symbols along the designated accepting path -}; - -GeneratedCase generate(const ScenarioParams& p) { - std::mt19937 rng(p.seed); - std::uniform_int_distribution sym_dist(0, static_cast(p.alphabet_size - 1)); - - Nft nft{ Nft::with_levels(p.num_levels) }; - const State start = nft.add_state(); - nft.initial.insert(start); - - std::vector accept_words(p.num_levels); - - std::vector frontier{ start }; - size_t designated_idx = 0; - - for (size_t layer = 0; layer < p.num_layers; ++layer) { - std::vector next_frontier; - next_frontier.reserve(p.branching); - for (size_t i = 0; i < p.branching; ++i) { next_frontier.push_back(nft.add_state()); } - - std::vector correct_symbols(p.num_levels); - for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { correct_symbols[lvl] = sym_dist(rng); } - const size_t next_designated_idx = std::uniform_int_distribution(0, next_frontier.size() - 1)(rng); - - for (size_t fi = 0; fi < frontier.size(); ++fi) { - for (size_t ti = 0; ti < next_frontier.size(); ++ti) { - std::vector word_parts(p.num_levels); - if (fi == designated_idx && ti == next_designated_idx) { - for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { word_parts[lvl] = { correct_symbols[lvl] }; } - } else { - for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { word_parts[lvl] = { sym_dist(rng) }; } - } - nft.insert_word_by_levels(frontier[fi], word_parts, next_frontier[ti]); - } - } - - if (p.eps_chain_len > 0) { - State prev = frontier[designated_idx]; - for (size_t k = 0; k < p.eps_chain_len; ++k) { - const State mid = nft.add_state(); - nft.delta.add(prev, EPSILON, mid); - prev = mid; - } - nft.delta.add(prev, EPSILON, next_frontier[next_designated_idx]); - } - - for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { accept_words[lvl].push_back(correct_symbols[lvl]); } - - frontier = std::move(next_frontier); - designated_idx = next_designated_idx; - } - - nft.final.insert(frontier[designated_idx]); - - return { std::move(nft), std::move(accept_words) }; -} - -struct Query { - std::string type; - std::vector level_words; -}; - -std::vector make_queries(const ScenarioParams& p, const std::vector& accept_words, std::mt19937& rng) { - std::vector queries; - std::uniform_int_distribution sym_dist(0, static_cast(p.alphabet_size - 1)); - - queries.push_back({ "exact", accept_words }); - - { - std::vector prefix(p.num_levels); - const size_t half = p.num_layers / 2; - for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { - prefix[lvl] = Word(accept_words[lvl].begin(), accept_words[lvl].begin() + half); - } - queries.push_back({ "prefix_half", prefix }); - } - - if (p.num_layers > 0) { - std::vector mutated = accept_words; - const size_t pos = p.num_layers / 2; - const size_t lvl = 0; - Symbol orig = mutated[lvl][pos]; - Symbol replacement; - do { replacement = sym_dist(rng); } while (replacement == orig); - mutated[lvl][pos] = replacement; - queries.push_back({ "mutate_middle", mutated }); - } - - { - std::vector empty(p.num_levels); - queries.push_back({ "empty", empty }); - } - - { - std::vector too_long = accept_words; - for (size_t lvl = 0; lvl < p.num_levels; ++lvl) { too_long[lvl].push_back(sym_dist(rng)); } - queries.push_back({ "too_long", too_long }); - } - - return queries; -} - -std::vector make_scenarios() { - std::vector scenarios; - unsigned seed_counter = 1000; - - const ScenarioParams base{ "base", 30, 4, 0, 2, 64, 0 }; - auto add = [&](ScenarioParams s) { - s.seed = seed_counter++; - scenarios.push_back(std::move(s)); - }; - - add(base); - - for (size_t v : { (size_t)5, (size_t)30, (size_t)150, (size_t)600 }) { - ScenarioParams s = base; - s.num_layers = v; - s.name = "word_len_" + std::to_string(v); - add(s); - } - - for (size_t v : { (size_t)1, (size_t)2, (size_t)4, (size_t)8, (size_t)16 }) { - ScenarioParams s = base; - s.branching = v; - s.alphabet_size = std::max(64, v * 4); - s.name = "branching_" + std::to_string(v); - add(s); - } - - for (size_t v : { (size_t)0, (size_t)1, (size_t)5, (size_t)20, (size_t)100 }) { - ScenarioParams s = base; - s.eps_chain_len = v; - s.name = "eps_len_" + std::to_string(v); - add(s); - } - - for (size_t v : { (size_t)1, (size_t)2, (size_t)3, (size_t)5 }) { - ScenarioParams s = base; - s.num_levels = v; - s.name = "num_levels_" + std::to_string(v); - add(s); - } - - for (size_t v : { (size_t)4, (size_t)16, (size_t)64, (size_t)256 }) { - ScenarioParams s = base; - s.alphabet_size = v; - s.name = "alphabet_" + std::to_string(v); - add(s); - } - - { - ScenarioParams s{ "combined_large", 100, 8, 10, 2, 128, 0 }; - add(s); - } - { - ScenarioParams s{ "combined_heavy_branch_eps", 50, 20, 50, 3, 256, 0 }; - add(s); - } - { - ScenarioParams s{ "combined_long_thin", 800, 2, 3, 2, 32, 0 }; - add(s); - } - - return scenarios; -} - -// Adaptively picks a repeat count so the timed loop takes roughly target_ns. -struct TimingResult { - double avg_ns; - uint64_t repeats; - bool result; -}; - -template -TimingResult time_call(Fn&& fn) { - using clock = std::chrono::steady_clock; - constexpr double target_ns = 100'000'000.0; // ~100ms per measurement - constexpr uint64_t max_repeats = 2'000'000; - - const bool result = fn(); - - uint64_t repeats = 1; - double elapsed_ns = 0.0; - while (true) { - const auto t0 = clock::now(); - for (uint64_t i = 0; i < repeats; ++i) { - volatile bool r = fn(); - (void)r; - } - const auto t1 = clock::now(); - elapsed_ns = std::chrono::duration(t1 - t0).count(); - if (elapsed_ns >= target_ns || repeats >= max_repeats) { break; } - const double scale = target_ns / std::max(elapsed_ns, 1.0); - uint64_t next_repeats = static_cast(static_cast(repeats) * std::min(scale, 64.0)); - if (next_repeats <= repeats) { next_repeats = repeats * 2; } - repeats = std::min(next_repeats, max_repeats); - } - - return { elapsed_ns / static_cast(repeats), repeats, result }; -} - -} // namespace - -int main() { -#ifdef MATA_BENCH_HAS_REPEAT_SYMBOL - std::cout << "scenario,num_layers,branching,eps_chain_len,num_levels,alphabet_size," - "num_states,num_transitions,query_type,match_prefix," - "result_post,repeats_post,avg_ns_post," - "result_repeat,repeats_repeat,avg_ns_repeat\n"; -#else - std::cout << "scenario,num_layers,branching,eps_chain_len,num_levels,alphabet_size," - "num_states,num_transitions,query_type,match_prefix,result,repeats,avg_ns\n"; -#endif - - for (const ScenarioParams& p : make_scenarios()) { - GeneratedCase gc = generate(p); - std::mt19937 query_rng(p.seed * 7919u + 17); - std::vector queries = make_queries(p, gc.accept_words, query_rng); - const size_t num_states = gc.nft.num_of_states(); - const size_t num_transitions = gc.nft.delta.num_of_transitions(); - - for (const Query& q : queries) { - for (bool match_prefix : { false, true }) { - // Called with 2 args (no explicit jump_mode) so this compiles unchanged against master's - // older signature too; nft_post defaults the 3rd param to JumpMode::RepeatSymbol anyway, - // which is what is_in_lang_by_levels_repeat_symbol below is restricted to. - TimingResult post_result = time_call([&] { - return gc.nft.is_in_lang_by_levels(q.level_words, match_prefix); - }); -#ifdef MATA_BENCH_HAS_REPEAT_SYMBOL - TimingResult repeat_result = time_call([&] { - return mata::nft::is_in_lang_by_levels_repeat_symbol(gc.nft, q.level_words, match_prefix); - }); - std::cout << p.name << ',' << p.num_layers << ',' << p.branching << ',' << p.eps_chain_len << ',' - << p.num_levels << ',' << p.alphabet_size << ',' << num_states << ',' << num_transitions - << ',' << q.type << ',' << (match_prefix ? 1 : 0) << ',' - << (post_result.result ? 1 : 0) << ',' << post_result.repeats << ',' << std::fixed - << std::setprecision(2) << post_result.avg_ns << ',' - << (repeat_result.result ? 1 : 0) << ',' << repeat_result.repeats << ',' - << std::fixed << std::setprecision(2) << repeat_result.avg_ns << '\n'; -#else - std::cout << p.name << ',' << p.num_layers << ',' << p.branching << ',' << p.eps_chain_len << ',' - << p.num_levels << ',' << p.alphabet_size << ',' << num_states << ',' << num_transitions - << ',' << q.type << ',' << (match_prefix ? 1 : 0) << ',' << (post_result.result ? 1 : 0) - << ',' << post_result.repeats << ',' << std::fixed << std::setprecision(2) - << post_result.avg_ns << '\n'; -#endif - } - } - } - - return 0; -} From bec90bc133b5cc33cd0a463fdaf20cf93474912d Mon Sep 17 00:00:00 2001 From: koniksedy Date: Fri, 7 Aug 2026 17:49:40 +0200 Subject: [PATCH 10/10] cmnt --- src/nft/nft.cc | 22 +--------------------- 1 file changed, 1 insertion(+), 21 deletions(-) diff --git a/src/nft/nft.cc b/src/nft/nft.cc index fbbec62b6..e9bc64023 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -670,14 +670,6 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols std::vector end_positions(tape_symbols.size()); for (size_t i = 0; i < tape_symbols.size(); ++i) { end_positions[i] = tape_symbols[i].size(); } - // A search node is a full configuration: the reading-head position on each of the n input words (n = number of - // levels) plus the current state. The position part is a heavy vector that is heavily shared -- every - // state along an epsilon chain carries the identical positions (epsilon reads nothing), and a branching step - // hands the same positions to every target -- so each distinct positions vector is interned to a small uint32 - // id once. The search then works entirely on cheap (positions_id, state) pairs: the visited set keys on a - // single packed integer instead of re-hashing a vector on every step, and a non-consuming epsilon step reuses - // the source id with no vector work at all. Interned vectors live in position_ids; unordered_map nodes are - // stable across insertion, so id_to_positions can hold plain pointers to them. std::unordered_map, uint32_t> position_ids; std::vector*> id_to_positions; auto intern = [&](const std::vector& positions) -> uint32_t { @@ -698,14 +690,6 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols }; std::unordered_set visited; - // Worklist. Its ordering only matters when short-circuiting (should_stop set). Then the search runs best-first, - // always expanding the configuration that has consumed the most input so far: an accepting exact match must - // consume every symbol, so "most consumed" is the greedy estimate of "closest to accepting". This beelines down - // the real input-consuming path (like a depth-first dive on the easy cases) yet defers epsilon transitions, which - // consume nothing -- so it neither plunges blindly down long epsilon chains the way a plain stack (DFS) does, nor - // sweeps the whole breadth the way a queue (BFS) does; both of those lose badly on opposite corners of the input - // space. Without a stop condition the entire reachable space is explored regardless of order, so the plain - // reachability sweep keeps a cheap LIFO stack. const bool best_first{ static_cast(should_stop) }; struct QueueItem { size_t consumed; // total input symbols read so far; higher = closer to a full (accepting) match @@ -820,11 +804,7 @@ StateSet Nft::post(const StateSet& states, const std::vector& tape_symbols } }; - // Pick only the outgoing transitions that can possibly fire, instead of scanning them all. A non-consuming - // EPSILON move is always available; a consuming move must match the current level's input symbol, so only - // that exact symbol and DONT_CARE can fire -- both found by direct lookup (StatePost is symbol-sorted). The - // exceptions, where any symbol might match and so all must be scanned, are a projected-out current level or a - // literal DONT_CARE in the input word. + // Pick only the outgoing transitions that can possibly fire, instead of scanning them all. const bool current_used{ use_tape[current_level] != 0 }; const bool current_has_symbol{ current_used && current_positions[current_level] < end_positions[current_level] };