doxygen comments + operator=

include/mata/nfa/algorithms.hh

@@ -36,7 +36,7 @@ Nfa minimize_brzozowski(const Nfa& aut);
  * Hopcroft minimization of automata. Based on the algorithm from the paper:
  *  "Efficient Minimization of DFAs With Partial Transition Functions" by Antti Valmari and Petri Lehtinen.
  *  The algorithm works in O(a*n*log(n)) time and O(m+n+a) space, where: n is the number of states, a is the size
- *  of the alphabet, and m is the number of transitions.
+ *  of the alphabet, and m is the number of transitions. [https://dl.acm.org/doi/10.1016/j.ipl.2011.12.004]
  * @param[in] dfa_trimmed Deterministic automaton without useless states. Perform trimming before calling this function.
  * @return Minimized deterministic automaton.
  */

src/nfa/operations.cc

@@ -963,15 +963,15 @@ class RefinablePartition {
     static_assert(std::is_unsigned<T>::value, "T must be an unsigned type.");
     static const T NO_MORE_ELEMENTS = std::numeric_limits<T>::max();
     static const size_t NO_SPLIT = std::numeric_limits<size_t>::max();
-    size_t num_of_sets;            // The number of sets in the partition.
-    std::vector<size_t> set_idx;   // For each element, tells the index of the set it belongs to.
+    size_t num_of_sets;            ///< The number of sets in the partition.
+    std::vector<size_t> set_idx;   ///< For each element, tells the index of the set it belongs to.
 
 private:
-    std::vector<T> elems;       // Contains all elements in an order such that the elements of the same set are contiguous.
-    std::vector<T> location;    // Contains the location of each element in the elements vector.
-    std::vector<size_t> first;  // Contains the index of the first element of each set in the elements vector.
-    std::vector<size_t> end;    // Contains the index after the last element of each set in the elements vector.
-    std::vector<size_t> mid;    // Contains the index after the last element of the first half of the set in the elements vector.
+    std::vector<T> elems;       ///< Contains all elements in an order such that the elements of the same set are contiguous.
+    std::vector<T> location;    ///< Contains the location of each element in the elements vector.
+    std::vector<size_t> first;  ///< Contains the index of the first element of each set in the elements vector.
+    std::vector<size_t> end;    ///< Contains the index after the last element of each set in the elements vector.
+    std::vector<size_t> mid;    ///< Contains the index after the last element of the first half of the set in the elements vector.
 
 public:
     /**
@@ -1058,6 +1058,31 @@ class RefinablePartition {
         : elems(std::move(other.elems)), set_idx(std::move(other.set_idx)), location(std::move(other.location)),
           first(std::move(other.first)), end(std::move(other.end)), mid(std::move(other.mid)), num_of_sets(other.num_of_sets) {}
 
+    RefinablePartition& operator=(const RefinablePartition &other) {
+        if (this != &other) {
+            elems = other.elems;
+            set_idx = other.set_idx;
+            location = other.location;
+            first = other.first;
+            end = other.end;
+            mid = other.mid;
+            num_of_sets = other.num_of_sets;
+        }
+        return *this;
+    }
+
+    RefinablePartition& operator=(RefinablePartition &&other) noexcept {
+        if (this != &other) {
+            elems = std::move(other.elems);
+            set_idx = std::move(other.set_idx);
+            location = std::move(other.location);
+            first = std::move(other.first);
+            end = std::move(other.end);
+            mid = std::move(other.mid);
+            num_of_sets = other.num_of_sets;
+        }
+        return *this;
+    }
 
     /**
      * @brief Get the number of elements across all sets.
@@ -1159,17 +1184,17 @@ Nfa mata::nfa::algorithms::minimize_hopcroft(const Nfa& dfa_trimmed) {
     assert(dfa_trimmed.get_useful_states().size() == dfa_trimmed.num_of_states());
 
     // Initialize equivalence classes. The initial partition is {Q}.
-    RefinablePartition<State> BRP(dfa_trimmed.num_of_states());
+    RefinablePartition<State> brp(dfa_trimmed.num_of_states());
     // Initialize splitters. A splitter is a set of transitions
     // over a common symbol incoming to an equivalence class. Initially,
     // the partition has m splitters, where m is the alphabet size.
-    RefinablePartition<size_t> TRP(dfa_trimmed.delta);
+    RefinablePartition<size_t> trp(dfa_trimmed.delta);
 
     // Initialize vector of incoming transitions for each state. Transitions
     // are represented only by their indices in the (flattened) delta.
     // Initialize mapping from transition index to its source state.
-    std::vector<State> trans_source_map(TRP.size());
-    std::vector<std::vector<size_t>> incomming_trans_idxs(BRP.size(), std::vector<size_t>());
+    std::vector<State> trans_source_map(trp.size());
+    std::vector<std::vector<size_t>> incomming_trans_idxs(brp.size(), std::vector<size_t>());
     size_t trans_idx = 0;
     for (const auto &trans : dfa_trimmed.delta.transitions()) {
         trans_source_map[trans_idx] = trans.source;
@@ -1190,32 +1215,32 @@ Nfa mata::nfa::algorithms::minimize_hopcroft(const Nfa& dfa_trimmed) {
     auto split_block = [&](size_t b) {
         // touched_spls has been moved to a higher scope to avoid multiple constructions/destructions.
         assert(touched_spls.empty());
-        size_t b_prime = BRP.split(b);  // One block will keep the old name 'b'.
+        size_t b_prime = brp.split(b);  // One block will keep the old name 'b'.
         if (b_prime == RefinablePartition<size_t>::NO_SPLIT) {
             // All or no states in the block were marked (touched) during the backpropagation.
             return;
         }
         // According to the Hopcroft's algorithm, it is sufficient to work only with the smaller block.
-        if (BRP.size_of_set(b) < BRP.size_of_set(b_prime)) {
+        if (brp.size_of_set(b) < brp.size_of_set(b_prime)) {
             b_prime = b;
         }
         // Split the transitions of the splitters according to the new partitioning.
         // Transitions in one splitter must have the same symbol and go to the same block.
-        for (State q = BRP.get_first(b_prime); q != RefinablePartition<State>::NO_MORE_ELEMENTS; q = BRP.get_next(q)) {
+        for (State q = brp.get_first(b_prime); q != RefinablePartition<State>::NO_MORE_ELEMENTS; q = brp.get_next(q)) {
             for (const size_t trans_idx : incomming_trans_idxs[q]) {
-                const size_t splitter_idx = TRP.set_idx[trans_idx];
-                if (TRP.no_marks(splitter_idx)) {
+                const size_t splitter_idx = trp.set_idx[trans_idx];
+                if (trp.no_marks(splitter_idx)) {
                     touched_spls.push(splitter_idx);
                 }
                 // Mark the transition in the splitter and move it to the first half of the set.
-                TRP.mark(trans_idx);
+                trp.mark(trans_idx);
             }
         }
         // Refine all splitters where some transitions were marked.
         while (!touched_spls.empty()) {
             const size_t splitter_idx = touched_spls.top();
             touched_spls.pop();
-            const size_t splitter_pime = TRP.split(splitter_idx);
+            const size_t splitter_pime = trp.split(splitter_idx);
             if (splitter_pime != RefinablePartition<size_t>::NO_SPLIT) {
                 // Use the new splitter for further refinement of the equivalence classes.
                 unready_spls.push(splitter_pime);
@@ -1224,13 +1249,13 @@ Nfa mata::nfa::algorithms::minimize_hopcroft(const Nfa& dfa_trimmed) {
     };
 
     // Use all splitters for the initial refinement.
-    for (size_t splitter_idx = 0; splitter_idx < TRP.num_of_sets; ++splitter_idx) {
+    for (size_t splitter_idx = 0; splitter_idx < trp.num_of_sets; ++splitter_idx) {
         unready_spls.push(splitter_idx);
     }
 
     // In the first refinement, we split the equivalence classes according to the final states.
     for (const State q : dfa_trimmed.final) {
-        BRP.mark(q);
+        brp.mark(q);
     }
     split_block(0);
 
@@ -1241,13 +1266,13 @@ Nfa mata::nfa::algorithms::minimize_hopcroft(const Nfa& dfa_trimmed) {
         // Backpropagation.
         // Fire back all transitions of the splitter. (Transitions over the same
         // symbol that go to the same block.) Mark the source states of these transitions.
-        for (size_t trans_idx = TRP.get_first(splitter_idx); trans_idx != RefinablePartition<size_t>::NO_MORE_ELEMENTS; trans_idx = TRP.get_next(trans_idx)) {
+        for (size_t trans_idx = trp.get_first(splitter_idx); trans_idx != RefinablePartition<size_t>::NO_MORE_ELEMENTS; trans_idx = trp.get_next(trans_idx)) {
             const State q = trans_source_map[trans_idx];
-            const size_t b_prime = BRP.set_idx[q];
-            if (BRP.no_marks(b_prime)) {
+            const size_t b_prime = brp.set_idx[q];
+            if (brp.no_marks(b_prime)) {
                 touched_blocks.push(b_prime);
             }
-            BRP.mark(q);
+            brp.mark(q);
         }
         // Try to split the blocks touched during the backpropagation.
         // The block will be split only if some states (not all) were touched (marked).
@@ -1260,16 +1285,16 @@ Nfa mata::nfa::algorithms::minimize_hopcroft(const Nfa& dfa_trimmed) {
 
     // Construct the minimized automaton using equivalence classes (BRP).
     assert(dfa_trimmed.initial.size() == 1);
-    Nfa result(BRP.num_of_sets, StateSet{ BRP.set_idx[*dfa_trimmed.initial.begin()] }, StateSet{});
-    for (size_t block_idx = 0; block_idx < BRP.num_of_sets; ++block_idx) {
-        const State q = BRP.get_first(block_idx);
+    Nfa result(brp.num_of_sets, StateSet{ brp.set_idx[*dfa_trimmed.initial.begin()] }, StateSet{});
+    for (size_t block_idx = 0; block_idx < brp.num_of_sets; ++block_idx) {
+        const State q = brp.get_first(block_idx);
         if (dfa_trimmed.final.contains(q)) {
             result.final.insert(block_idx);
         }
         StatePost &mut_state_post = result.delta.mutable_state_post(block_idx);
         for (const SymbolPost &symbol_post : dfa_trimmed.delta[q]) {
             assert(symbol_post.targets.size() == 1);
-            const State target = BRP.set_idx[*symbol_post.targets.begin()];
+            const State target = brp.set_idx[*symbol_post.targets.begin()];
             mut_state_post.push_back(SymbolPost{ symbol_post.symbol, StateSet{ target } });
         }
     }