wrong k-bound

Bug #2004468 reported by Lena Ernstsen
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
TAPAAL
Fix Committed
Undecided
Lena Ernstsen

Bug Description

K-bound is incorrectly calculated when verifying nets.

How to reproduce:
    1) Open token-ring net.
    2) Convert to timed net.
    3) Verify the query.
    !) Verification error occurs: Zero color constituents

The GUI is passing the wrong number of tokens to the engine. Should be fixed for both verifypn and verifydtapn.

Also, double check the boundedness check.

Jiri Srba (srba)
Changed in tapaal:
milestone: none → cpn
Lena Ernstsen (lsaid)
Changed in tapaal:
assignee: nobody → Lena Ernstsen (lsaid)
Jiri Srba (srba)
Changed in tapaal:
status: New → Fix Committed
To post a comment you must log in.
This report contains Public information  
Everyone can see this information.

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.