Add epsilon for get_shortest_word

include/mata/nfa/nfa.hh

@@ -669,8 +669,15 @@ public:
      */
     std::optional<Word> get_word(std::optional<Symbol> first_epsilon = EPSILON) const;
 
-    /// Returns any accepted shortest word in the language of the automaton
-    std::optional<mata::Word> 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<Word> Some shortest word from the language. If the language is empty, returns std::nullopt.
+     */
+    std::optional<mata::Word> get_shortest_word(const std::optional<Symbol> first_epsilon = EPSILON) const;
 
     /**
      * @brief Get any arbitrary accepted word in the language of the complement of the automaton.

src/nfa/operations.cc

@@ -1368,73 +1368,76 @@ std::optional<mata::Word> Nfa::get_word(const std::optional<Symbol> first_epsilo
     return word;
 }
 
-std::optional<mata::Word> 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<mata::nfa::State> worklist;
-        std::vector<int> dist(num_of_states, -1);
-        std::vector<Predecessor> 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<mata::Word> Nfa::get_shortest_word(const std::optional<Symbol> 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<mata::nfa::State> worklist;
+    std::vector<int> dist(num_of_states, -1);
+    std::vector<Predecessor> 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<mata::Word> Nfa::get_word_from_complement(const Alphabet* alphabet) const {