is_flat: flatness checking

VeriFIT · Jul 12, 2024 · 08d5ffb · 08d5ffb
1 parent 0a54bb0
commit 08d5ffb
Show file tree

Hide file tree

Showing 3 changed files with 85 additions and 0 deletions.
diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh
@@ -320,6 +320,15 @@ public:
      */
     bool is_acyclic() const;
 
+    /**
+     * @brief Is the automaton flat?
+     * Flat automaton is an NFA whose every SCC is a simple loop. Basically each state in an 
+     * SCC has at most one successor within this SCC.
+     * 
+     * @return true <-> Automaton graph is flat.
+     */
+    bool is_flat() const;
+
     /**
      * Fill @p alphabet_to_fill with symbols from @p nfa.
      * @param[in] nfa NFA with symbols to fill @p alphabet_to_fill with.

diff --git a/src/nfa/nfa.cc b/src/nfa/nfa.cc
@@ -379,6 +379,34 @@ bool Nfa::is_acyclic() const {
     return acyclic;
 }
 
+bool Nfa::is_flat() const {
+    bool flat = true;
+
+    mata::nfa::Nfa::TarjanDiscoverCallback callback {};
+    callback.scc_discover = [&](const std::vector<mata::nfa::State>& scc, const std::vector<mata::nfa::State>& tarjan_stack) -> bool {
+        (void)tarjan_stack;
+
+        for(const mata::nfa::State& st : scc) {
+            bool one_input_visited = false;
+            for (const mata::nfa::SymbolPost& sp : this->delta[st]) {
+                for (const mata::nfa::State& tgt : scc) {
+                    if(sp.targets.find(tgt) != sp.targets.end()) {
+                        if(one_input_visited) {
+                            flat = false;
+                            return true;
+                        }
+                        one_input_visited = true;
+                    }
+                }
+            }
+        }
+        return false;
+    };
+
+    tarjan_scc_discover(callback);
+    return flat;
+}
+
 std::string Nfa::print_to_dot() const {
     std::stringstream output;
     print_to_dot(output);

diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc
@@ -328,6 +328,54 @@ TEST_CASE("mata::nfa::is_acyclic")
     }
 } // }}}
 
+TEST_CASE("mata::nfa::is_flat")
+{ // {{{
+    Nfa aut(14);
+
+    SECTION("An empty automaton is flat")
+    {
+        REQUIRE(aut.is_flat());
+    }
+
+    SECTION("An automaton with a state that is both initial and final is acyclic")
+    {
+        aut.initial = {1, 2};
+        aut.final = {2, 3};
+        REQUIRE(aut.is_flat());
+    }
+
+    SECTION("More complicated automaton")
+    {
+        aut.initial = {0};
+        aut.final = {4};
+        aut.delta.add(0, 'a', 1);
+        aut.delta.add(1, 'a', 3);
+        aut.delta.add(3, 'b', 2);
+        aut.delta.add(2, 'a', 1);
+        aut.delta.add(1, 'b', 4);
+        aut.delta.add(4, 'b', 6);
+        aut.delta.add(6, 'c', 5);
+        aut.delta.add(5, 'a', 4);
+        REQUIRE(aut.is_flat());
+    }
+
+    SECTION("Nonflat automaton")
+    {
+        aut.initial = {0};
+        aut.final = {4};
+        aut.delta.add(0, 'a', 1);
+        aut.delta.add(1, 'a', 3);
+        aut.delta.add(3, 'b', 2);
+        aut.delta.add(2, 'a', 1);
+        aut.delta.add(1, 'b', 4);
+        aut.delta.add(4, 'b', 6);
+        aut.delta.add(6, 'c', 5);
+        aut.delta.add(5, 'a', 4);
+        aut.delta.add(1, 'c', 2);
+        REQUIRE(!aut.is_flat());
+    }
+} // }}}
+
 TEST_CASE("mata::nfa::get_word_for_path()")
 { // {{{
     Nfa aut(5);