From 7ed500302f54a58c2c7929f6c1f59f5de2f2a417 Mon Sep 17 00:00:00 2001
From: Mikkel Tygesen <mikkel.tygesen@gmail.com>
Date: Wed, 29 Oct 2025 16:40:12 +0100
Subject: [PATCH 1/3] fixed some traces reporting as finite even though they
 contain a loop

---
 src/LTL/Algorithm/NestedDepthFirstSearch.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/LTL/Algorithm/NestedDepthFirstSearch.cpp b/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
index 41e6c151b..b43a34efe 100644
--- a/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
+++ b/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
@@ -229,7 +229,7 @@ namespace LTL {
         if(!nested_todo.empty()) {
             // here the last state is significant
             // of the successor is the check that demonstrates the violation.
-            loop_id = nested_todo.back()._id;
+            loop_id = nested_todo.front()._id;
             nested_todo.pop_back();
         }
 

From 4c878f62673b756a8fc0f5169cc501fe19179f5d Mon Sep 17 00:00:00 2001
From: Mikkel Tygesen <mikkel.tygesen@gmail.com>
Date: Wed, 12 Nov 2025 17:58:13 +0100
Subject: [PATCH 2/3] fix popping before processing

---
 src/LTL/Algorithm/NestedDepthFirstSearch.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/LTL/Algorithm/NestedDepthFirstSearch.cpp b/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
index b43a34efe..20ee371c4 100644
--- a/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
+++ b/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
@@ -227,10 +227,9 @@ namespace LTL {
         if(!todo.empty())
             todo.pop_back();
         if(!nested_todo.empty()) {
-            // here the last state is significant
+            // here the first state is significant
             // of the successor is the check that demonstrates the violation.
             loop_id = nested_todo.front()._id;
-            nested_todo.pop_back();
         }
 
         for(auto* stck : {&todo, &nested_todo})

From 51b9032a28693727f0239d2fc7cc95719f782837 Mon Sep 17 00:00:00 2001
From: Mikkel Tygesen <mikkel.tygesen@gmail.com>
Date: Wed, 12 Nov 2025 19:25:14 +0100
Subject: [PATCH 3/3] fix test failing

---
 src/LTL/Algorithm/NestedDepthFirstSearch.cpp | 57 +++++++++-----------
 1 file changed, 25 insertions(+), 32 deletions(-)

diff --git a/src/LTL/Algorithm/NestedDepthFirstSearch.cpp b/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
index 20ee371c4..da93d00d4 100644
--- a/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
+++ b/src/LTL/Algorithm/NestedDepthFirstSearch.cpp
@@ -218,42 +218,35 @@ namespace LTL {
 
 
     template<typename T>
-    void NestedDepthFirstSearch::build_trace(light_deque<stack_entry_t<T>>& todo, light_deque<stack_entry_t<T>>& nested_todo)
-    {
-        size_t loop_id = std::numeric_limits<size_t>::max();
-        // last element of todo-stack always has a "garbage" transition, it is the
-        // current working element OR first element of nested.
+    void NestedDepthFirstSearch::build_trace(light_deque<stack_entry_t<T>>& todo, light_deque<stack_entry_t<T>>& nested_todo) {
+        if (!todo.empty()) todo.pop_back();
+        while (!todo.empty()) {
+            const auto& top = todo.front();
+            const auto res = top._sucinfo.transition();
+            if constexpr (std::is_same<std::decay_t<decltype(res)>, std::vector<uint32_t>>::value) {
+                _trace.emplace_back(res);
+            } else {
+                _trace.push_back({res});
+                assert(res < _net.numberOfTransitions());
+            }
 
-        if(!todo.empty())
-            todo.pop_back();
-        if(!nested_todo.empty()) {
-            // here the first state is significant
-            // of the successor is the check that demonstrates the violation.
-            loop_id = nested_todo.front()._id;
+            todo.pop_front();
         }
 
-        for(auto* stck : {&todo, &nested_todo})
-        {
-            while(!(*stck).empty())
-            {
-                auto& top = (*stck).front();
-                if(top._id == loop_id)
-                {
-                    _loop = _trace.size();
-                    loop_id = std::numeric_limits<size_t>::max();
-                }
-                auto res = top._sucinfo.transition();
-                if constexpr (std::is_same<decltype(res),std::vector<uint32_t>>::value)
-                {
-                    _trace.emplace_back(top._sucinfo.transition());
-                }
-                else
-                {
-                    _trace.push_back({top._sucinfo.transition()});
-                    assert(top._sucinfo.transition() < _net.numberOfTransitions());
-                }
-                (*stck).pop_front();
+        _loop = _trace.size();
+        if (nested_todo.empty()) return;
+        while (!nested_todo.empty()) {
+            const auto& top = nested_todo.front();
+            const auto res = top._sucinfo.transition();
+            if constexpr (std::is_same<std::decay_t<decltype(res)>, std::vector<uint32_t>>::value) {
+                _trace.emplace_back(res);
+            } else if (res < _net.numberOfTransitions()) {
+                _trace.push_back({res});
+            } else {
+                break;
             }
+
+            nested_todo.pop_front();
         }
     }
 }