Wrong EG trace (delay for ever)
Bug #1339221 reported by
Jiri Srba
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Released
|
Critical
|
Peter Gjøl Jensen | ||
Bug Description
Open the attached net and verify. It will return a trace that is not executable in the net
(delay for ever while there is an invariant).
This is not an issue introduced in the latest branches, it is already in the released 3.1 version
and both with and without darts!
A new branch for this one, please.
Related branches
lp:~verifydtapn-contributers/verifydtapn/DeadlockInvariantPropagation
- Jiri Srba: Approve
-
Diff: 13 lines (+2/-1)1 file modifiedsrc/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp (+2/-1)
Revision history for this message
| Jiri Srba (srba) wrote | #1 |
Revision history for this message
| Peter Gjøl Jensen (peter-gjoel) wrote | #2 |
| Changed in tapaal: | |
| status: | New → In Progress |
| Changed in tapaal: | |
| status: | In Progress → Fix Committed |
| Changed in tapaal: | |
| status: | Fix Committed → Fix Released |
To post a comment you must log in.
Fixed,
In short, the bug occurred because the deadlock-check code did not check the invariant of P2 and therefor saw the transition T0 as enabled (even though it was not). The deadlock check was used for the trace-generation.