TAPAAL

CPN verification fails for int ranges not starting with 1

Bug #1964790 reported by Jiri Srba
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
TAPAAL
Fix Committed
Undecided
Unassigned
TAPAAL cpn "cpn"

Bug Description

I made a model with two integer ranges and some reachability query but the verification fails
with the engine returning: "CANNOT_COMPUTE".

Revision history for this message
Jiri Srba (srba) wrote :
Revision history for this message
Jiri Srba (srba) wrote :

Unfolding of the net also fails.

Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

I asked peter to look at this, it seem like it does not like intranges not starting at 1

summary: - CPN verification fails
+ CPN verification fails for int ranges not starting with 1
Revision history for this message
Jiri Srba (srba) wrote :

The problem is now fixed for the verifypn. If you make the same net timed in the GUI and run verifydtapn, the problem is still there.

Revision history for this message
Jiri Srba (srba) wrote :

The problem is now fixed in the engines both for verifypn, verifydtapn as well as verifytapn.

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.
Subscribing...

Other bug subscribers

Remote bug watches

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