diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 4061324d5..0391f144d 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -669,8 +669,15 @@ public: */ std::optional get_word(std::optional first_epsilon = EPSILON) const; - /// Returns any accepted shortest word in the language of the automaton - std::optional get_shortest_word(); + /** + * @brief Get any accepted shortest word in the language of the automaton. + * + * The automaton is searched using BFS, returning a word for the first reached final state. + * + * @param first_epsilon If defined, all symbols >=first_epsilon are assumed to be epsilon and therefore are not in the returned word. + * @return std::optional Some shortest word from the language. If the language is empty, returns std::nullopt. + */ + std::optional get_shortest_word(const std::optional first_epsilon = EPSILON) const; /** * @brief Get any arbitrary accepted word in the language of the complement of the automaton. diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index ea9dd1485..66ad83fa8 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -1368,73 +1368,76 @@ std::optional Nfa::get_word(const std::optional first_epsilo return word; } -std::optional Nfa::get_shortest_word(){ - - //Predecessor state and the symbol used to reach the current state. - struct Predecessor { - mata::nfa::State prev; - mata::Symbol sym; - }; - - //Resulting word - mata::Word res; - const size_t num_of_states = this->num_of_states(); - - std::queue worklist; - std::vector dist(num_of_states, -1); - std::vector pred(num_of_states); - - // Initialize BFS from all initial states - for (mata::nfa::State init_state : this->initial) { - dist[init_state] = 0; - worklist.push(init_state); - - if (this->final.contains(init_state)) { - return res; // empty word accepted - } - } - - // Standard BFS loop - while (!worklist.empty()) { - // Get the next state in the queue and remove it - mata::nfa::State curr_state = worklist.front(); - worklist.pop(); +std::optional Nfa::get_shortest_word(const std::optional first_epsilon) const { + if (initial.empty() || final.empty()) { return std::nullopt; } - // Calculate the distance for any newly discovered states from this node - int next_dist = dist[curr_state] + 1; + //Predecessor state and the symbol used to reach the current state. + struct Predecessor { + mata::nfa::State prev; + mata::Symbol sym; + }; - // Iterate outgoing transitions - for (const auto& sym_post : this->delta[curr_state]) { - mata::Symbol transition_sym = sym_post.symbol; + //Resulting word + const size_t num_of_states = this->num_of_states(); - // Iterate over all destination states for this specific symbol - for (mata::nfa::State target_state : sym_post.targets) { - //Skip if the state has already been visited - if (dist[target_state] != -1) continue; + std::queue worklist; + std::vector dist(num_of_states, -1); + std::vector pred(num_of_states); - dist[target_state] = next_dist; //Mark state as visited - pred[target_state] = { curr_state, transition_sym }; // Store made transition + // Initialize BFS from all initial states + for (mata::nfa::State init_state : this->initial) { + dist[init_state] = 0; + worklist.push(init_state); - // Check if the newly reached state is an accepting state - if (this->final.contains(target_state)) { + if (this->final.contains(init_state)) { + return std::nullopt; // empty word accepted + } + } - // reconstruct shortest word - for (mata::nfa::State backtrack_state = target_state; dist[backtrack_state] > 0; - backtrack_state = pred[backtrack_state].prev) { - res.push_back(pred[backtrack_state].sym); + // Standard BFS loop + while (!worklist.empty()) { + // Get the next state in the queue and remove it + mata::nfa::State curr_state = worklist.front(); + worklist.pop(); + + // Calculate the distance for any newly discovered states from this node + int next_dist = dist[curr_state] + 1; + + // Iterate outgoing transitions + for (const auto& sym_post : this->delta[curr_state]) { + mata::Symbol transition_sym = sym_post.symbol; + + // Iterate over all destination states for this specific symbol + for (mata::nfa::State target_state : sym_post.targets) { + //Skip if the state has already been visited + if (dist[target_state] != -1) continue; + + dist[target_state] = next_dist; //Mark state as visited + pred[target_state] = { curr_state, transition_sym }; // Store made transition + + // Check if the newly reached state is an accepting state + if (this->final.contains(target_state)) { + mata::Word res; + // reconstruct shortest word + for (mata::nfa::State backtrack_state = target_state; dist[backtrack_state] > 0; + backtrack_state = pred[backtrack_state].prev) { + Symbol next_symbol = pred[backtrack_state].sym; + if (!first_epsilon.has_value() || next_symbol < first_epsilon) { + res.push_back(next_symbol); } - //Reverse the backtracked word - std::reverse(res.begin(), res.end()); - return res; } - - // If 'target_state' is not a final state, push it to the queue to explore its transitions later - worklist.push(target_state); + //Reverse the backtracked word + std::reverse(res.begin(), res.end()); + return res; } + + // If 'target_state' is not a final state, push it to the queue to explore its transitions later + worklist.push(target_state); } } + } - return res; // language empty + return std::nullopt; // language empty } std::optional Nfa::get_word_from_complement(const Alphabet* alphabet) const {