Tarjan reporting false loops - fix 2080845#212
Conversation
srba
left a comment
srba
left a comment
There was a problem hiding this comment.
The fix is wrong, if you open the net from this bug report
https://bugs.launchpad.net/tapaal/+bug/2127171
and ask the LTL query
E (G ((F TAPN1.P6 = 1) and (F TAPN1.P5 = 1)))
using Tarjen, it gives a finite trace which is wrong - compare with the trace returned without Tarjan that is correct.
srba
left a comment
srba
left a comment
There was a problem hiding this comment.
The attached query on the model returns a trace that is not executable in the net.
srba
left a comment
srba
left a comment
There was a problem hiding this comment.
Fixes all the issues but there is a new bug introduce - see the attached net and run the second query - this gives a trace that is not executable. This works correctly in the current main, so it was introduced in this PR.
test2.tapn.zip
srba
left a comment
srba
left a comment
There was a problem hiding this comment.
The trace changes in the PR also cause wrong verifications answers for LTL with Tarjan, see this bug report
https://bugs.launchpad.net/tapaal/+bug/2131082
2 participants
Fixes:
https://bugs.launchpad.net/tapaal/+bug/2080845