Boundedness for timed CPN issues
Bug #2024923 reported by
Jiri Srba
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Committed
|
Undecided
|
Lena Ernstsen | ||
Bug Description
Open the first net tacpn-005.tapn and open the query and run boundedness check and minimize. It keeps there one extra token but the correct answer should be 0. The boundedness check is moreover done using verifypn engine but in the lens it is a timed net so verifytapn should be run here.
The net tacpn-006.tapn is a small variant where there is an useless invariant added. The boundedness check now correctly runs verifytapn and minimizes the number of extra tokens to 0. If then however run the verification of the query, the engine complains that it got fewer tokens (-k 9) than the number of tokens in the initial marking (there are 10 tokens). To the GUI passes wrong number to the engine.
Revision history for this message
| Jiri Srba (srba) wrote | #1 |
Revision history for this message
| Jiri Srba (srba) wrote | #2 |
Revision history for this message
| Jiri Srba (srba) wrote | #3 |
| Changed in tapaal: | |
| milestone: | none → cpn |
| Changed in tapaal: | |
| status: | New → In Progress |
| Changed in tapaal: | |
| status: | In Progress → Fix Committed |
To post a comment you must log in.
After the fix, please, double check if the other boundedness related bugs are still okay.