From e6ee3df975fafcbd696c4d54388d9eeea00e27d0 Mon Sep 17 00:00:00 2001
From: jurajsic <juraj.sic@outlook.com>
Date: Thu, 17 Oct 2024 13:41:27 +0200
Subject: [PATCH] add failling test for inclusion cex

---
 src/nfa/inclusion.cc |  6 +--
 tests/nfa/nfa.cc     | 98 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 101 insertions(+), 3 deletions(-)

diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc
index 0358e0c41..8f67b56e0 100644
--- 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
index e45771e13..4e7dc87df 100644
--- 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{};