boundedness check is broken
Bug #1939878 reported by
Jiri Srba
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Committed
|
Undecided
|
Unassigned | ||
Bug Description
Open the attached net, it should need 1 extra token to prove boundedness, but the boundedness check in query dialog sets it to 0 and claims that this is enough (which is wrong).
Related branches
lp:~tapaal-contributor/tapaal/boundedness-check
- Jiri Srba: Needs Fixing
-
Diff: 311 lines (+118/-33)5 files modifiedsrc/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java (+2/-1)
src/pipe/gui/KBoundAnalyzer.java (+66/-15)
src/pipe/gui/RunKBoundAnalysis.java (+29/-6)
src/pipe/gui/RunVerification.java (+3/-2)
src/pipe/gui/RunVerificationBase.java (+18/-9)
Revision history for this message
| Jiri Srba (srba) wrote | #1 |
| Changed in tapaal: | |
| status: | New → Fix Committed |
To post a comment you must log in.
