tests

VeriFIT · Nov 30, 2024 · 094ad6a · 094ad6a
1 parent a7d7b60
commit 094ad6a
Show file tree

Hide file tree

Showing 2 changed files with 95 additions and 4 deletions.
diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc
@@ -980,7 +980,7 @@ class RefinablePartition {
      * @param n The number of states.
      */
     RefinablePartition(const size_t num_of_states)
-        : num_of_sets(1), elems(num_of_states), location(num_of_states), set_idx(num_of_states),
+        : num_of_sets(1), set_idx(num_of_states), elems(num_of_states), location(num_of_states),
           first(num_of_states), end(num_of_states), mid(num_of_states) {
         // Initially, all states are in the same equivalence class.
         first[0] = mid[0] = 0;
@@ -998,7 +998,7 @@ class RefinablePartition {
      * @param delta The transition function.
      */
     RefinablePartition(const Delta &delta)
-        : num_of_sets(0), elems(), location(), set_idx(), first(), end(), mid() {
+        : num_of_sets(0), set_idx(), elems(), location(), first(), end(), mid() {
         size_t num_of_transitions = 0;
         std::vector<size_t> counts;
         std::unordered_map<Symbol, size_t> symbol_map;
@@ -1051,11 +1051,11 @@ class RefinablePartition {
     }
 
     RefinablePartition(const RefinablePartition &other)
-        : elems(other.elems), location(other.location), set_idx(other.set_idx),
+        : 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) {}
 
     RefinablePartition(RefinablePartition &&other) noexcept
-        : elems(std::move(other.elems)), location(std::move(other.location)), set_idx(std::move(other.set_idx)),
+        : 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) {}
 
 

diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc
@@ -2858,6 +2858,97 @@ TEST_CASE("mata::nfa::reduce_size_by_simulation()")
     }
 }
 
+TEST_CASE("mata::nfa::algorithms::minimize_hopcroft()") {
+    SECTION("empty automaton") {
+        Nfa aut;
+        Nfa result = minimize_hopcroft(aut);
+        CHECK(result.is_lang_empty());
+    }
+
+    SECTION("one state") {
+        Nfa aut(1);
+        aut.initial.insert(0);
+        aut.final.insert(0);
+        Nfa result = minimize_hopcroft(aut);
+        CHECK(result.delta.num_of_transitions() == 0);
+        CHECK(result.num_of_states() == 1);
+        CHECK(result.initial.size() == 1);
+        CHECK(result.final.size() == 1);
+        CHECK(result.initial == result.final);
+    }
+
+    SECTION("one trans") {
+        Nfa aut(2);
+        aut.initial.insert(0);
+        aut.final.insert(1);
+        aut.delta.add(0, 'a', 1);
+        Nfa result = minimize_hopcroft(aut);
+        CHECK(result.delta.num_of_transitions() == 1);
+        CHECK(result.num_of_states() == 2);
+        CHECK(result.initial.size() == 1);
+        CHECK(result.final.size() == 1);
+        CHECK(result.initial != result.final);
+        CHECK(are_equivalent(aut, result));
+    }
+
+    SECTION("line") {
+        Nfa aut(3);
+        aut.initial.insert(0);
+        aut.final.insert(2);
+        aut.delta.add(0, 'a', 1);
+        aut.delta.add(1, 'a', 2);
+        aut.delta.add(2, 'a', 3);
+        Nfa result = minimize_hopcroft(aut);
+        CHECK(result.delta.num_of_transitions() == 3);
+        CHECK(result.num_of_states() == 4);
+        CHECK(result.initial.size() == 1);
+        CHECK(result.final.size() == 1);
+        CHECK(result.initial != result.final);
+        CHECK(are_equivalent(aut, result));
+    }
+
+    SECTION("loop") {
+        Nfa aut;
+        aut.initial.insert(0);
+        aut.final.insert(1);
+        aut.delta.add(0, 1, 2);
+        aut.delta.add(1, 0, 1);
+        aut.delta.add(1, 1, 1);
+        aut.delta.add(2, 1, 1);
+
+        Nfa aut_brz = minimize_brzozowski(aut);
+        Nfa aut_hop = minimize_hopcroft(aut);
+        CHECK(are_equivalent(aut_brz, aut_hop));
+        CHECK(aut_brz.num_of_states() == aut_hop.num_of_states());
+        CHECK(aut_brz.delta.num_of_transitions() == aut_hop.delta.num_of_transitions());
+        CHECK(aut_brz.initial.size() == aut_hop.initial.size());
+        CHECK(aut_brz.final.size() == aut_hop.final.size());
+    }
+
+    SECTION("difficult") {
+        Nfa aut;
+        aut.initial.insert(0);
+        aut.final.insert(1);
+        aut.final.insert(6);
+        aut.delta.add(0, 0, 1);
+        aut.delta.add(1, 0, 2);
+        aut.delta.add(2, 0, 4);
+        aut.delta.add(4, 1, 5);
+        aut.delta.add(4, 0, 3);
+        aut.delta.add(5, 0, 6);
+        aut.delta.add(3, 0, 1);
+
+        Nfa aut_brz = minimize_brzozowski(aut);
+        Nfa aut_hop = minimize_hopcroft(aut);
+        CHECK(are_equivalent(aut_brz, aut_hop));
+        CHECK(aut_brz.num_of_states() == aut_hop.num_of_states());
+        CHECK(aut_brz.delta.num_of_transitions() == aut_hop.delta.num_of_transitions());
+        CHECK(aut_brz.initial.size() == aut_hop.initial.size());
+        CHECK(aut_brz.final.size() == aut_hop.final.size());
+    }
+
+}
+
 TEST_CASE("mata::nfa::reduce_size_by_residual()") {
     Nfa aut;
     StateRenaming state_renaming;