Merge pull request #374 from VeriFIT/scc-refactor

Refactoring of SCC-based Algorithms

include/mata/nfa/nfa.hh

@@ -161,12 +161,31 @@ public:
      * @brief Get the useful states using a modified Tarjan's algorithm. A state
      * is useful if it is reachable from an initial state and can reach a final state.
      *
-     * @param state_at_first_useful_state Whether only the first found useful state is set to true. Useful when
-     *  checking whether the set of useful states is empty.
-     *
      * @return BoolVector Bool vector whose ith value is true iff the state i is useful.
      */
-    BoolVector get_useful_states(const bool stop_at_first_useful_state = false) const;
+    BoolVector get_useful_states() const;
+
+    /**
+     * @brief Structure for storing callback functions (event handlers) utilizing 
+     * Tarjan's SCC discover algorithm.
+     */
+    struct TarjanDiscoverCallback {
+        // event handler for the first-time state discovery
+        std::function<bool(State)> state_discover;
+        // event handler for SCC discovery (together with the whole Tarjan stack)
+        std::function<bool(const std::vector<State>&, const std::vector<State>&)> scc_discover;
+        // event handler for state in SCC discovery
+        std::function<void(State)> scc_state_discover;
+        // event handler for visiting of the state successors
+        std::function<void(State,State)> succ_state_discover;
+    };
+
+    /**
+     * @brief Tarjan's SCC discover algorihm.
+     * 
+     * @param callback Callbacks class to instantiate callbacks for the Tarjan's algorithm.
+     */
+    void tarjan_scc_discover(const TarjanDiscoverCallback& callback) const;
 
     /**
      * @brief Remove inaccessible (unreachable) and not co-accessible (non-terminating) states in-place.
@@ -256,12 +275,20 @@ public:
     StateSet post(const StateSet& states, const Symbol& symbol) const;
 
     /**
-     * Check whether the language of NFA is empty.
+     * Check whether the language of NFA is empty. 
+     * Currently calls is_lang_empty_scc if cex is null 
      * @param[out] cex Counter-example path for a case the language is not empty.
      * @return True if the language is empty, false otherwise.
      */
     bool is_lang_empty(Run* cex = nullptr) const;
 
+    /**
+     * @brief Check if the language is empty using Tarjan's SCC discover algorithm.
+     * 
+     * @return Language empty <-> True
+     */
+    bool is_lang_empty_scc() const;
+
     /**
      * @brief Test whether an automaton is deterministic.
      *
@@ -278,6 +305,13 @@ public:
      */
     bool is_complete(Alphabet const* alphabet = nullptr) const;
 
+    /**
+     * @brief Is the automaton graph acyclic? Used for checking language finiteness.
+     * 
+     * @return true <-> Automaton graph is acyclic.
+     */
+    bool is_acyclic() const;
+
     /**
      * Fill @p alphabet with symbols from @p nfa.
      * @param[in] nfa NFA with symbols to fill @p alphabet with.

src/nfa/nfa.cc

@@ -217,13 +217,8 @@ namespace {
  *    SCC if useful, we declare all nodes in the SCC useful and moreover we propagate usefulness also the states
  *    in @p tarjan_stack as it contains states that can reach this closed SCC.
  *
- * @return BoolVector
- *
- * If @p stop_at_first_useful_state is true, then the algo stops at the first found useful state. This is used in an
- *  emptiness test.
  */
-BoolVector Nfa::get_useful_states(const bool stop_at_first_useful_state) const {
-    BoolVector useful(this->num_of_states(),false);
+void Nfa::tarjan_scc_discover(const TarjanDiscoverCallback& callback) const {
     std::vector<TarjanNodeData> node_info(this->num_of_states());
     std::vector<State> program_stack;
     std::vector<State> tarjan_stack;
@@ -249,9 +244,9 @@ BoolVector Nfa::get_useful_states(const bool stop_at_first_useful_state) const {
             // initialize node
             act_state_data = TarjanNodeData(act_state, this->delta, index_cnt++);
             tarjan_stack.push_back(act_state);
-            if(this->final.contains(act_state)) {
-                useful[act_state] = true;
-                if (stop_at_first_useful_state) { return useful; }
+
+            if(callback.state_discover && callback.state_discover(act_state)) {
+                return;
             }
         } else { // return from the recursive call
             State act_succ = act_state_data.current_move->target;
@@ -267,9 +262,8 @@ BoolVector Nfa::get_useful_states(const bool stop_at_first_useful_state) const {
         bool rec_call = false;
         for(; act_state_data.current_move != act_state_data.end_move; ++act_state_data.current_move) {
             next_state = act_state_data.current_move->target;
-            // if successor is useful, act_state is useful as well
-            if(useful[next_state]) {
-                useful[act_state] = true;
+            if(callback.succ_state_discover) {
+                callback.succ_state_discover(act_state, next_state);
             }
             if(!node_info[next_state].initilized) { // recursive call
                 program_stack.push_back(next_state);
@@ -284,37 +278,107 @@ BoolVector Nfa::get_useful_states(const bool stop_at_first_useful_state) const {
         // check if we have the root of a SCC
         if(act_state_data.lowlink == act_state_data.index) {
             State st;
-            // contains the closed SCC a final state
-            bool final_scc = false;
             std::vector<State> scc;
             do {
                 st = tarjan_stack.back();
                 tarjan_stack.pop_back();
                 node_info[st].on_stack = false;
 
-                // SCC contains a final state
-                if(useful[st]) {
-                    final_scc = true;
+                if(callback.scc_state_discover) {
+                    callback.scc_state_discover(st);
                 }
                 scc.push_back(st);
             } while(st != act_state);
-            if(final_scc) {
-                // Propagate usefulness to the closed SCC.
-                for(const State& st: scc) { useful[st] = true; }
-                // Propagate usefulness to predecessors in @p tarjan_stack.
-                for (auto state_it{ tarjan_stack.rbegin() }, state_it_end{ tarjan_stack.rend() };
-                     state_it != state_it_end; ++state_it) {
-                    if (useful[*state_it]) { break; }
-                    useful[*state_it] = true;
-                }
+            if(callback.scc_discover && callback.scc_discover(scc, tarjan_stack)) {
+                return;
             }
         }
         // all successors have been processed, we can remove act_state from the program stack
         program_stack.pop_back();
     }
+}
+
+BoolVector Nfa::get_useful_states() const {
+    BoolVector useful(this->num_of_states(), false);
+    bool final_scc = false;
+
+    TarjanDiscoverCallback callback {};
+    callback.state_discover = [&](State state) -> bool {
+        if(this->final.contains(state)) {
+            useful[state] = true;
+        }
+        return false;
+    };
+    callback.scc_discover = [&](const std::vector<State>& scc, const std::vector<State>& tarjan_stack) -> bool {
+        if(final_scc) {
+            // Propagate usefulness to the closed SCC.
+            for(const State& st: scc) { useful[st] = true; }
+            // Propagate usefulness to predecessors in @p tarjan_stack.
+            for (auto state_it{ tarjan_stack.rbegin() }, state_it_end{ tarjan_stack.rend() };
+                    state_it != state_it_end; ++state_it) {
+                if (useful[*state_it]) { break; }
+                useful[*state_it] = true;
+            }
+        }
+        final_scc = false;
+        return false;
+    };
+    callback.scc_state_discover = [&](State state) {
+        if(useful[state]) {
+            final_scc = true;
+        }
+    };
+    callback.succ_state_discover = [&](State act_state, State next_state) {
+        if(useful[next_state]) {
+            useful[act_state] = true;
+        }
+    };
+
+    tarjan_scc_discover(callback);
     return useful;
 }
 
+bool Nfa::is_lang_empty_scc() const {
+    bool accepting_state = false;
+
+    TarjanDiscoverCallback callback {};
+    callback.state_discover = [&](State state) -> bool {
+        if(this->final.contains(state)) {
+            accepting_state = true;
+            return true;
+        }
+        return false;
+    };
+
+    tarjan_scc_discover(callback);
+    return !accepting_state;
+}
+
+bool Nfa::is_acyclic() const {
+    bool acyclic = true;
+
+    TarjanDiscoverCallback callback {};
+    callback.scc_discover = [&](const std::vector<State>& scc, const std::vector<State>& tarjan_stack) -> bool {
+        (void)tarjan_stack;
+        if(scc.size() > 1) {
+            acyclic = false;
+                return true;
+            } else { // check for self-loops
+                State st = scc[0];
+                for(const auto& sp : this->delta[st]) {
+                    if(sp.targets.find(st) != sp.targets.end()) {
+                        acyclic = false;
+                        return true;
+                    }
+                }
+            }
+            return false;
+    };
+
+    tarjan_scc_discover(callback);
+    return acyclic;
+}
+
 std::string Nfa::print_to_DOT() const {
     std::stringstream output;
     print_to_DOT(output);

src/nfa/operations.cc

@@ -505,11 +505,7 @@ bool mata::nfa::Nfa::is_lang_empty(Run* cex) const {
     //TOOD: hot fix for performance reasons for TACAS.
     // Perhaps make the get_useful_states return a witness on demand somehow.
     if (!cex) {
-        BoolVector useful_states = get_useful_states(true);
-        for (State is_state_useful: useful_states)
-            if (is_state_useful)
-                return false;
-        return true;
+        return is_lang_empty_scc();
     }
 
     std::list<State> worklist(initial.begin(), initial.end());

tests/nfa/nfa.cc

@@ -263,6 +263,64 @@ TEST_CASE("mata::nfa::is_lang_empty()")
     }
 } // }}}
 
+TEST_CASE("mata::nfa::is_acyclic")
+{ // {{{
+    Nfa aut(14);
+
+    SECTION("An empty automaton is acyclic")
+    {
+        REQUIRE(aut.is_acyclic());
+    }
+
+    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_acyclic());
+    }
+
+    SECTION("More complicated automaton")
+    {
+        aut.initial = {1, 2};
+        aut.delta.add(1, 'a', 2);
+        aut.delta.add(1, 'a', 3);
+        aut.delta.add(1, 'b', 4);
+        aut.delta.add(2, 'a', 3);
+        aut.delta.add(2, 'b', 4);
+        aut.delta.add(3, 'b', 4);
+        aut.delta.add(3, 'c', 7);
+        aut.delta.add(7, 'a', 8);
+
+        SECTION("without final states")
+        {
+            REQUIRE(aut.is_lang_empty());
+        }
+    }
+
+    SECTION("Cyclic automaton")
+    {
+        aut.initial = {1, 2};
+        aut.final = {8, 9};
+        aut.delta.add(1, 'c', 2);
+        aut.delta.add(2, 'a', 4);
+        aut.delta.add(2, 'c', 1);
+        aut.delta.add(2, 'c', 3);
+        aut.delta.add(3, 'e', 5);
+        aut.delta.add(4, 'c', 8);
+        REQUIRE(!aut.is_acyclic());
+    }
+
+    SECTION("Automaton with self-loops")
+    {
+        Nfa aut(2);
+        aut.initial = {0};
+        aut.final = {1};
+        aut.delta.add(0, 'c', 1);
+        aut.delta.add(1, 'a', 1);
+        REQUIRE(!aut.is_acyclic());
+    }
+} // }}}
+
 TEST_CASE("mata::nfa::get_word_for_path()")
 { // {{{
     Nfa aut(5);