works on empty automata

VeriFIT · Oct 30, 2024 · d2cec6b · d2cec6b
1 parent 31413b1
commit d2cec6b
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 0 deletions.
diff --git a/src/inter-aut.cc b/src/inter-aut.cc
@@ -292,6 +292,11 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) {
             }
         }
 
+        // In case of no transition
+        if (opstack.size() != 1) {
+            return {};
+        }
+
         assert(opstack.size() == 1);
         return std::move(*opstack.begin());
 }

diff --git a/tests/nfa/builder.cc b/tests/nfa/builder.cc
@@ -18,6 +18,44 @@ using Word = std::vector<Symbol>;
 TEST_CASE("parse_from_mata()") {
     Delta delta;
 
+    SECTION("Empty automaton - No initial and final") {
+        Nfa nfa{ delta, {}, {} };
+        SECTION("from String") {
+            std::string empty_nfa_str = "@NFA-explicit\n%Alphabet-auto\n";
+            Nfa empty_nfa{ mata::nfa::builder::parse_from_mata(empty_nfa_str) };
+            CHECK(are_equivalent(empty_nfa, nfa));
+        }
+
+        SECTION("from file") {
+            std::filesystem::path nfa_file{ "./temp-test-parse_from_mata-empty_nfa.mata" };
+            std::fstream file{ nfa_file, std::fstream::in | std::fstream::out | std::fstream::trunc };
+            file << "@NFA-explicit\n%Alphabet-auto\n";
+            file.close();
+            Nfa parsed{ mata::nfa::builder::parse_from_mata(nfa_file) };
+            std::filesystem::remove(nfa_file);
+            CHECK(are_equivalent(parsed, nfa));
+        }
+
+    }
+
+    SECTION("Empty automaton with empty final and initial") {
+        Nfa nfa{ delta, {}, {} };
+        SECTION("from String") {
+            std::string empty_nfa_str = "@NFA-explicit\n%Alphabet-auto\n%Initial\n%Final\n";
+            Nfa empty_nfa{ mata::nfa::builder::parse_from_mata(empty_nfa_str) };
+            CHECK(are_equivalent(empty_nfa, nfa));
+        }
+        SECTION("from file") {
+            std::filesystem::path nfa_file{ "./temp-test-parse_from_mata-empty_nfa-empty_initial_final.mata" };
+            std::fstream file{ nfa_file, std::fstream::in | std::fstream::out | std::fstream::trunc };
+            file << "@NFA-explicit\n%Alphabet-auto\n%Initial\n%Final\n";
+            file.close();
+            Nfa parsed{ mata::nfa::builder::parse_from_mata(nfa_file) };
+            std::filesystem::remove(nfa_file);
+            CHECK(are_equivalent(parsed, nfa));
+        }
+    }
+
     SECTION("Simple automaton") {
         delta.add(0, 0, 0);
         delta.add(0, 1, 1);