fix cex path for naive alg

VeriFIT · Oct 18, 2024 · 9074a98 · 9074a98
1 parent b52bdde
commit 9074a98
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 11 deletions.
diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc
@@ -21,9 +21,21 @@ bool mata::nfa::algorithms::is_included_naive(
     } else {
         bigger_cmpl = complement(bigger, *alphabet);
     }
-    Nfa nfa_isect = intersection(smaller, bigger_cmpl);
 
-    return nfa_isect.is_lang_empty(cex);
+    std::unordered_map<std::pair<State,State>,State> prod_map;
+    Nfa nfa_isect = intersection(smaller, bigger_cmpl, Limits::max_symbol, &prod_map);
+
+    bool result = nfa_isect.is_lang_empty(cex);
+    if (cex != nullptr && !result) {
+        std::unordered_map<State,State> nfa_isect_state_to_smaller_state;
+        for (const auto& prod_map_item : prod_map) {
+            nfa_isect_state_to_smaller_state[prod_map_item.second] = prod_map_item.first.first;
+        }
+        for (State& path_state : cex->path) {
+            path_state = nfa_isect_state_to_smaller_state[path_state];
+        }
+    }
+    return result;
 } // is_included_naive }}}
 
 

diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc
@@ -2184,15 +2184,22 @@ q9 196608 q9
 q10 67 q5
 )"
             ))[0]);
-        bool is_incl = mata::nfa::algorithms::is_included_antichains(smaller, bigger, nullptr, &cex);
-        REQUIRE(!is_incl);
-        REQUIRE(smaller.is_in_lang(cex.word));
-        REQUIRE(!bigger.is_in_lang(cex.word));
-        REQUIRE(cex.path.size() == cex.word.size() + 1);
-        for (size_t i = 0; i < cex.word.size(); ++i) {
-            const auto& s = smaller.delta[cex.path[i]].find(cex.word[i]);
-            REQUIRE(s != smaller.delta[cex.path[i]].end());
-            REQUIRE(s->targets.contains(cex.path[i+1]));
+
+        for (const auto& algo : ALGORITHMS) {
+            SECTION(algo)
+            {
+                params["algorithm"] = algo;
+                bool is_incl = is_included(smaller, bigger, &cex, nullptr, params);
+                REQUIRE(!is_incl);
+                REQUIRE(smaller.is_in_lang(cex.word));
+                REQUIRE(!bigger.is_in_lang(cex.word));
+                REQUIRE(cex.path.size() == cex.word.size() + 1);
+                for (size_t i = 0; i < cex.word.size(); ++i) {
+                    const auto& s = smaller.delta[cex.path[i]].find(cex.word[i]);
+                    REQUIRE(s != smaller.delta[cex.path[i]].end());
+                    CHECK(s->targets.contains(cex.path[i+1]));
+                }
+            }
         }
     }