Also optimized language emptiness check a bit (get_useful_states term…

…inates after finding first final state).

src/nfa/delta.cc

@@ -375,14 +375,14 @@ bool Delta::operator==(const Delta& other) const {
     return other_transitions_it == other_transitions_end;
 }
 
-//Returns an iterator to the smallest epsilon, or end() if there is no epsilon
-//Searches from the end of the vector of SymbolPosts, since epsilons are at the end and they are typically few, mostly 1.
+///Returns an iterator to the smallest epsilon, or end() if there is no epsilon
+///Searches from the end of the vector of SymbolPosts, since epsilons are at the end and they are typically few, mostly 1.
 StatePost::const_iterator StatePost::first_epsilon_it(Symbol first_epsilon) const {
     auto it = end();
     while (it != begin()) {
         --it;
         if (it->symbol < first_epsilon) { //is it a normal symbol already?
-            return it + 1; // Return one step back: the smallest epsilon or end().
+            return it + 1; // Return the previous position, the smallest epsilon or end().
         }
     }
 

src/nfa/nfa.cc

@@ -243,8 +243,11 @@ namespace {
  *    in @p tarjan_stack as it contains states that can reach this closed SCC.
  *
  * @return BoolVector
+ *
+ * If stop_at_first_useful_state is true, then the algo stops at the first found useful state.
+ * This is used at emptiness test.
  */
-BoolVector Nfa::get_useful_states() const {
+BoolVector Nfa::get_useful_states(bool stop_at_first_useful_state) const {
     BoolVector useful(this->num_of_states(),false);
     std::vector<TarjanNodeData> node_info(this->num_of_states());
     std::deque<State> program_stack;
@@ -273,6 +276,8 @@ BoolVector Nfa::get_useful_states() const {
             tarjan_stack.push_back(act_state);
             if(this->final.contains(act_state)) {
                 useful[act_state] = true;
+                if (stop_at_first_useful_state)
+                    return useful;
             }
         } else { // return from the recursive call
             State act_succ = act_state_data.get_curr_succ();

src/nfa/operations.cc

@@ -519,7 +519,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();
+        BoolVector useful_states = get_useful_states(true);
         for (State is_state_useful: useful_states)
             if (is_state_useful)
                 return false;

tests-integration/src/bench-bool-comb-cox-inter.cc

@@ -29,23 +29,31 @@ int main(int argc, char *argv[]) {
     Nfa lhs = automata[0];
     Nfa rhs = automata[1];
 
-    // Setting precision of the times to fixed points and 4 decimal places
 
+    // Setting precision of the times to fixed points and 4 decimal places
 
     TIME_BEGIN(intersection);
-    Nfa intersect_aut = intersection(lhs, rhs);
+    Nfa intersect_aut = intersection(rhs, rhs);
     TIME_END(intersection);
-    std::cout<<"states: "<<intersect_aut.num_of_states()<<std::endl;
-    TIME_BEGIN(is_lang_empty);
-    intersect_aut.is_lang_empty();
-    TIME_END(is_lang_empty);
+    TIME_BEGIN(uni);
+    Nfa uni_aut = uni(intersect_aut,intersect_aut);
+    TIME_BEGIN(is_lang_empty1);
+    uni_aut.is_lang_empty();
+    TIME_END(is_lang_empty1);
+    TIME_BEGIN(is_lang_empty2);
+    uni_aut.is_lang_empty();
+    TIME_END(is_lang_empty2);
+    TIME_BEGIN(get_useful_states1);
+    uni_aut.get_useful_states();
+    TIME_END(get_useful_states1);
+    TIME_BEGIN(get_useful_states2);
+    uni_aut.get_useful_states();
+    TIME_END(get_useful_states2);
     //intersect_aut.final.clear();
     TIME_BEGIN(trim);
-    intersect_aut.trim();
+    uni_aut.trim();
     TIME_END(trim);
-    std::cout<<"lhs states: "<<lhs.num_of_states()<<std::endl;
-    std::cout<<"lhs states: "<<rhs.num_of_states()<<std::endl;
-    std::cout<<"prod states: "<<intersect_aut.num_of_states()<<std::endl;
+    std::cout<<"trimmed states: "<<intersect_aut.num_of_states()<<std::endl;
 
     return EXIT_SUCCESS;
 }