Flatness checking

include/mata/nfa/nfa.hh

@@ -320,6 +320,16 @@ 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.

include/mata/utils/ord-vector.hh

@@ -267,7 +267,7 @@ public:
     /**
      * Check whether @p key exists in the ordered vector.
      */
-    bool contains(const Key& key) { return find(key) != end(); }
+    bool contains(const Key& key) const { return find(key) != end(); }
 
     /**
      * @brief Remove @p k from sorted vector.

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.contains(tgt)) {
+                        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);

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);