From 1352ae928485d17dc0bb8cdf275c0495ff2154fb Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Wed, 8 Oct 2025 20:12:27 +0200 Subject: [PATCH 1/9] fixed tarjan reporting false loops --- src/LTL/Algorithm/TarjanModelChecker.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index dd0b1b5d3..69ffcb27e 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -294,8 +294,6 @@ namespace LTL { void TarjanModelChecker::build_trace(S& seen, light_deque &&dstack, light_deque& cstack) { assert(_violation); - if (cstack[dstack.back()._pos]._stateid == _loop_state) - _loop = _trace.size(); dstack.pop_back(); size_t p = 0; bool had_deadlock = _loop_trans == std::numeric_limits::max() - 1; @@ -311,8 +309,6 @@ namespace LTL { had_deadlock = true; break; } - if(cstack[p]._stateid == _loop_state) - _loop = _trace.size(); cstack[p]._lowlink = std::numeric_limits::max(); } // follow previously found back edges via lowsource until back in dstack. @@ -334,9 +330,10 @@ namespace LTL { p = cstack[p]._lowsource; } } - if(!had_deadlock && _loop_trans < _net.numberOfTransitions()) - { + + if (!had_deadlock && !_invariant_loop && _loop_trans < _net.numberOfTransitions()) { assert(_loop_trans < _net.numberOfTransitions()); + _loop = _trace.size(); _trace.push_back({_loop_trans}); } } From a5a183987fd5229ed08cbb75a306b5f1eea0f84f Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Thu, 9 Oct 2025 18:06:34 +0200 Subject: [PATCH 2/9] only set loop state if violation --- src/LTL/Algorithm/TarjanModelChecker.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index 69ffcb27e..c1279ee3e 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -270,9 +270,11 @@ namespace LTL { // either way update the component ID of the state we came from. cstack[from]._lowlink = cstack[to]._lowlink; if constexpr (T::save_trace()) { - _loop_state = cstack[to]._stateid; - _loop_trans = successorGenerator.fired(); - cstack[to]._lowsource = from; + if (_violation) { + _loop_state = cstack[to]._stateid; + _loop_trans = successorGenerator.fired(); + cstack[to]._lowsource = from; + } } } } @@ -294,6 +296,8 @@ namespace LTL { void TarjanModelChecker::build_trace(S& seen, light_deque &&dstack, light_deque& cstack) { assert(_violation); + if (cstack[dstack.back()._pos]._stateid == _loop_state) + _loop = _trace.size(); dstack.pop_back(); size_t p = 0; bool had_deadlock = _loop_trans == std::numeric_limits::max() - 1; @@ -309,6 +313,8 @@ namespace LTL { had_deadlock = true; break; } + if(cstack[p]._stateid == _loop_state) + _loop = _trace.size(); cstack[p]._lowlink = std::numeric_limits::max(); } // follow previously found back edges via lowsource until back in dstack. @@ -331,7 +337,7 @@ namespace LTL { } } - if (!had_deadlock && !_invariant_loop && _loop_trans < _net.numberOfTransitions()) { + if(!had_deadlock && _loop_trans < _net.numberOfTransitions()) { assert(_loop_trans < _net.numberOfTransitions()); _loop = _trace.size(); _trace.push_back({_loop_trans}); From cc36b14762e619b81eedeb78549de86f61d57e9c Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Wed, 15 Oct 2025 00:43:07 +0200 Subject: [PATCH 3/9] fixed loop position --- src/LTL/Algorithm/TarjanModelChecker.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index c1279ee3e..32400da5e 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -339,7 +339,6 @@ namespace LTL { if(!had_deadlock && _loop_trans < _net.numberOfTransitions()) { assert(_loop_trans < _net.numberOfTransitions()); - _loop = _trace.size(); _trace.push_back({_loop_trans}); } } From 106b5f8ede4a342a17806255d326d5164365791c Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Mon, 20 Oct 2025 20:09:57 +0200 Subject: [PATCH 4/9] fixed buffer example --- src/LTL/Algorithm/TarjanModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index 32400da5e..854aa99ce 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -151,7 +151,7 @@ namespace LTL { if constexpr (SaveTrace) { if (isnew) { - seen.set_history(stateid, successorGenerator.fired()); + seen.set_history(stateid, dtop._sucinfo.transition()); } } From 105d3a63a36fe119224540b4f4a8abee59bdff38 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Wed, 22 Oct 2025 16:52:44 +0200 Subject: [PATCH 5/9] fixed parent referencing --- include/LTL/Structures/BitProductStateSet.h | 8 ++------ include/LTL/Structures/CompoundStateSet.h | 8 ++------ src/LTL/Algorithm/TarjanModelChecker.cpp | 7 ++++--- 3 files changed, 8 insertions(+), 15 deletions(-) diff --git a/include/LTL/Structures/BitProductStateSet.h b/include/LTL/Structures/BitProductStateSet.h index 40f6e0c6d..68e2ae536 100644 --- a/include/LTL/Structures/BitProductStateSet.h +++ b/include/LTL/Structures/BitProductStateSet.h @@ -132,14 +132,13 @@ namespace LTL { namespace Structures { void decode(ProductState &state, stateid_t id) override { - _parent = id; BitProductStateSet>,nbits>::decode(state, id); } - void set_history(stateid_t id, size_t transition) + void set_history(stateid_t id, stateid_t parent, size_t transition) { assert(this->_states.exists(id).first); - this->_states[id] = {_parent, transition}; + this->_states[id] = {parent, transition}; } std::pair get_history(stateid_t stateid) @@ -147,9 +146,6 @@ namespace LTL { namespace Structures { assert(this->_states.exists(stateid).first); return this->_states[stateid]; } - - private: - stateid_t _parent = 0; }; } } diff --git a/include/LTL/Structures/CompoundStateSet.h b/include/LTL/Structures/CompoundStateSet.h index 81da2659e..8f2cd8b97 100644 --- a/include/LTL/Structures/CompoundStateSet.h +++ b/include/LTL/Structures/CompoundStateSet.h @@ -131,14 +131,13 @@ namespace LTL { namespace Structures { void decode(ProductState &state, stateid_t id) override { - _parent = id; BitProductStateSet>,nbits>::decode(state, id); } - void set_history(stateid_t id, size_t transition) + void set_history(stateid_t id, stateid_t parent, size_t transition) { assert(this->_states.exists(id).first); - this->_states[id] = {_parent, transition}; + this->_states[id] = {parent, transition}; } std::pair get_history(stateid_t stateid) @@ -146,9 +145,6 @@ namespace LTL { namespace Structures { assert(this->_states.exists(stateid).first); return this->_states[stateid]; } - - private: - stateid_t _parent = 0; }; } } #endif /* COMPOUNDSTATESET_H */ diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index 854aa99ce..d7ced560b 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -148,14 +148,15 @@ namespace LTL { if (stateid == std::numeric_limits::max()) { continue; } - + if constexpr (SaveTrace) { if (isnew) { - seen.set_history(stateid, dtop._sucinfo.transition()); + auto parent_stateid = cstack[dtop._pos]._stateid; + seen.set_history(stateid, parent_stateid, successorGenerator.fired()); } } - dtop._sucinfo._last_state = stateid; + // lookup successor in 'hash' table auto marking = StateSet::get_marking_id(stateid); From 11aa56218664839acfa2d3fe8f715913ab429cdf Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Wed, 12 Nov 2025 17:15:25 +0100 Subject: [PATCH 6/9] fixed last state not being updated --- src/LTL/Algorithm/TarjanModelChecker.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index d7ced560b..89ac6bfe4 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -156,7 +156,7 @@ namespace LTL { } } - + dtop._sucinfo._last_state = stateid; // lookup successor in 'hash' table auto marking = StateSet::get_marking_id(stateid); @@ -337,7 +337,7 @@ namespace LTL { p = cstack[p]._lowsource; } } - + if(!had_deadlock && _loop_trans < _net.numberOfTransitions()) { assert(_loop_trans < _net.numberOfTransitions()); _trace.push_back({_loop_trans}); From b225d00dcefe14fbba2469bdb961f047e05a90d7 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Wed, 12 Nov 2025 17:23:53 +0100 Subject: [PATCH 7/9] fix indent --- src/LTL/Algorithm/TarjanModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index 89ac6bfe4..144c4a7a8 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -156,7 +156,7 @@ namespace LTL { } } - dtop._sucinfo._last_state = stateid; + dtop._sucinfo._last_state = stateid; // lookup successor in 'hash' table auto marking = StateSet::get_marking_id(stateid); From f4a7de5f7c74956a37bb5bf119e3f49b9cd89648 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Tue, 9 Dec 2025 15:37:42 +0100 Subject: [PATCH 8/9] revert last change --- include/LTL/Structures/BitProductStateSet.h | 7 +++++-- include/LTL/Structures/CompoundStateSet.h | 7 +++++-- src/LTL/Algorithm/TarjanModelChecker.cpp | 3 +-- 3 files changed, 11 insertions(+), 6 deletions(-) diff --git a/include/LTL/Structures/BitProductStateSet.h b/include/LTL/Structures/BitProductStateSet.h index 68e2ae536..8f51a1d4d 100644 --- a/include/LTL/Structures/BitProductStateSet.h +++ b/include/LTL/Structures/BitProductStateSet.h @@ -135,10 +135,10 @@ namespace LTL { namespace Structures { BitProductStateSet>,nbits>::decode(state, id); } - void set_history(stateid_t id, stateid_t parent, size_t transition) + void set_history(stateid_t id, size_t transition) { assert(this->_states.exists(id).first); - this->_states[id] = {parent, transition}; + this->_states[id] = {_parent, transition}; } std::pair get_history(stateid_t stateid) @@ -146,6 +146,9 @@ namespace LTL { namespace Structures { assert(this->_states.exists(stateid).first); return this->_states[stateid]; } + + private: + stateid_t _parent = 0; }; } } diff --git a/include/LTL/Structures/CompoundStateSet.h b/include/LTL/Structures/CompoundStateSet.h index 8f2cd8b97..f5689fa04 100644 --- a/include/LTL/Structures/CompoundStateSet.h +++ b/include/LTL/Structures/CompoundStateSet.h @@ -134,10 +134,10 @@ namespace LTL { namespace Structures { BitProductStateSet>,nbits>::decode(state, id); } - void set_history(stateid_t id, stateid_t parent, size_t transition) + void set_history(stateid_t id, size_t transition) { assert(this->_states.exists(id).first); - this->_states[id] = {parent, transition}; + this->_states[id] = {_parent, transition}; } std::pair get_history(stateid_t stateid) @@ -145,6 +145,9 @@ namespace LTL { namespace Structures { assert(this->_states.exists(stateid).first); return this->_states[stateid]; } + + private: + stateid_t _parent = 0; }; } } #endif /* COMPOUNDSTATESET_H */ diff --git a/src/LTL/Algorithm/TarjanModelChecker.cpp b/src/LTL/Algorithm/TarjanModelChecker.cpp index 144c4a7a8..6110d8dbf 100644 --- a/src/LTL/Algorithm/TarjanModelChecker.cpp +++ b/src/LTL/Algorithm/TarjanModelChecker.cpp @@ -151,8 +151,7 @@ namespace LTL { if constexpr (SaveTrace) { if (isnew) { - auto parent_stateid = cstack[dtop._pos]._stateid; - seen.set_history(stateid, parent_stateid, successorGenerator.fired()); + seen.set_history(stateid, successorGenerator.fired()); } } From 113f88ea0b740342bff7be5adaeab675f28943ce Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Wed, 10 Dec 2025 14:06:43 +0100 Subject: [PATCH 9/9] revert stateset change --- include/LTL/Structures/BitProductStateSet.h | 1 + include/LTL/Structures/CompoundStateSet.h | 1 + 2 files changed, 2 insertions(+) diff --git a/include/LTL/Structures/BitProductStateSet.h b/include/LTL/Structures/BitProductStateSet.h index 8f51a1d4d..40f6e0c6d 100644 --- a/include/LTL/Structures/BitProductStateSet.h +++ b/include/LTL/Structures/BitProductStateSet.h @@ -132,6 +132,7 @@ namespace LTL { namespace Structures { void decode(ProductState &state, stateid_t id) override { + _parent = id; BitProductStateSet>,nbits>::decode(state, id); } diff --git a/include/LTL/Structures/CompoundStateSet.h b/include/LTL/Structures/CompoundStateSet.h index f5689fa04..843f04e18 100644 --- a/include/LTL/Structures/CompoundStateSet.h +++ b/include/LTL/Structures/CompoundStateSet.h @@ -131,6 +131,7 @@ namespace LTL { namespace Structures { void decode(ProductState &state, stateid_t id) override { + _parent = id; BitProductStateSet>,nbits>::decode(state, id); }