Skip to content

Tarjan reporting false loops - fix 2080845 #212

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mtygesen wants to merge 10 commits into
base: main
Choose a base branch
from
Open

Tarjan reporting false loops - fix 2080845 #212

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
1352ae9
fixed tarjan reporting false loops
mtygesen Oct 8, 2025
a5a1839
only set loop state if violation
mtygesen Oct 9, 2025
cc36b14
fixed loop position
mtygesen Oct 14, 2025
106b5f8
fixed buffer example
mtygesen Oct 20, 2025
105d3a6
fixed parent referencing
mtygesen Oct 22, 2025
11aa562
fixed last state not being updated
mtygesen Nov 12, 2025
b225d00
fix indent
mtygesen Nov 12, 2025
f4a7de5
revert last change
mtygesen Dec 9, 2025
113f88e
revert stateset change
mtygesen Dec 10, 2025
e3372d7
Merge branch 'TAPAAL:main' into tarjan-false-loop-2080845
mtygesen Jan 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion include/LTL/Structures/CompoundStateSet.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ namespace LTL { namespace Structures {
assert(this->_states.exists(stateid).first);
return this->_states[stateid];
}

private:
stateid_t _parent = 0;
};
Expand Down
14 changes: 8 additions & 6 deletions src/LTL/Algorithm/TarjanModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ namespace LTL {
if (stateid == std::numeric_limits<idx_t>::max()) {
continue;
}

if constexpr (SaveTrace) {
if (isnew) {
seen.set_history(stateid, successorGenerator.fired());
Expand Down Expand Up @@ -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;
}
}
}
}
Expand Down Expand Up @@ -334,8 +336,8 @@ namespace LTL {
p = cstack[p]._lowsource;
}
}
if(!had_deadlock && _loop_trans < _net.numberOfTransitions())
{

if(!had_deadlock && _loop_trans < _net.numberOfTransitions()) {
assert(_loop_trans < _net.numberOfTransitions());
_trace.push_back({_loop_trans});
}
Expand Down
Loading