TAPAAL

Very slow verification when trace is on "some"

Bug #868151 reported by Jiri Srba
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
TAPAAL
Fix Released
Critical
Morten Jacobsen
2.0
Fix Released
High
Morten Jacobsen
TAPAAL 2.0.2
VerifyTAPN
Status tracked in Trunk
Trunk
Fix Released
Critical
Morten Jacobsen
VerifyTAPN 1.0.2

Bug Description

Open the attached net and verify the query. It takes no time. Now open the query dialog and change "no trace" to "some trace". The verification now takes more than 30 seconds!

Revision history for this message
Jiri Srba (srba) wrote :
Changed in verifytapn:
importance: Undecided → Critical
assignee: nobody → Morten Jacobsen (mortenja)
milestone: none → 1.0.2
Revision history for this message
Jiri Srba (srba) wrote :

Now I know where is the problem. I forgot a transition T2 in the model that has no input and no output places. This causes
the problem with trace generation. Otherwise the model works fine. Can this be somehow fixed?

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

The UPPAAL optimized translation completely fails on this model too!

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

In fact both the optimized translations (also broadcast fail on exporting this model). I will make a separate bug report for this.

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

The problem was solved by removing orphan transitions before the verification. Verifytapn will print a line to the output should any orphan transitions (no input arcs, no output arcs) be removed.

Changed in tapaal:
status: New → Fix Released
Changed in verifytapn:
status: New → Fix Committed
Kenneth Yrke Jørgensen (yrke)
Changed in tapaal:
milestone: 2.1 → none
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.