add failling test for inclusion cex

VeriFIT · Oct 17, 2024 · e6ee3df · e6ee3df
1 parent 17ffaf6
commit e6ee3df
Show file tree

Hide file tree

Showing 2 changed files with 101 additions and 3 deletions.
diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc
@@ -167,10 +167,10 @@ bool mata::nfa::algorithms::is_included_antichains(
                         cex->word.clear();
                         cex->word.push_back(smaller_symbol);
                         ProdStateType trav = prod_state;
-                        while (paths[trav].first != trav)
+                        while (paths.at(trav).first != trav)
                         { // go back until initial state
-                            cex->word.push_back(paths[trav].second);
-                            trav = paths[trav].first;
+                            cex->word.push_back(paths.at(trav).second);
+                            trav = paths.at(trav).first;
                         }
 
                         std::reverse(cex->word.begin(), cex->word.end());

diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc
@@ -2065,6 +2065,104 @@ TEST_CASE("mata::nfa::is_included()")
         }
     }
 
+    SECTION("large example")
+    {
+        plumbing::construct(&smaller, mata::IntermediateAut::parse_from_mf(parse_mf(
+R"(@NFA-explicit
+%Alphabet-auto
+%Initial q0
+%Final q10
+q0 65 q1
+q0 66 q1
+q0 67 q1
+q0 196608 q1
+q1 65 q2
+q1 66 q2
+q1 67 q2
+q1 196608 q2
+q2 65 q2
+q2 65 q3
+q2 66 q2
+q2 66 q4
+q2 67 q2
+q2 196608 q2
+q4 66 q5
+q5 66 q6
+q6 65 q6
+q6 65 q7
+q6 66 q6
+q6 67 q6
+q6 196608 q6
+q7 67 q8
+q8 67 q9
+q9 67 q10
+q10 65 q10
+q10 66 q10
+q10 67 q10
+q10 196608 q10
+q3 67 q11
+q11 67 q12
+q12 67 q13
+q13 65 q13
+q13 66 q13
+q13 66 q14
+q13 67 q13
+q13 196608 q13
+q14 66 q15
+q15 66 q16
+q16 65 q10
+q16 66 q10
+q16 67 q10
+q16 196608 q10
+)"
+            ))[0]);
+        plumbing::construct(&bigger, mata::IntermediateAut::parse_from_mf(parse_mf(
+R"(@NFA-explicit
+%Alphabet-auto
+%Initial q0 q7
+%Final q6
+q0 65 q1
+q0 66 q1
+q0 67 q1
+q0 196608 q1
+q1 65 q2
+q1 66 q2
+q1 67 q2
+q1 196608 q2
+q2 65 q2
+q2 66 q2
+q2 66 q3
+q2 67 q2
+q2 196608 q2
+q3 66 q4
+q4 66 q5
+q5 66 q6
+q6 65 q6
+q6 66 q6
+q6 67 q6
+q6 196608 q6
+q7 65 q8
+q7 66 q8
+q7 67 q8
+q7 196608 q8
+q8 65 q8
+q8 66 q9
+q8 67 q8
+q8 196608 q8
+q9 65 q9
+q9 65 q10
+q9 66 q9
+q9 67 q9
+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));
+    }
+
     SECTION("wrong parameters 1")
     {
         OnTheFlyAlphabet alph{};