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)
Changed in tapaal: | |
status: | New → Fix Committed |
To post a comment you must log in.