Impossible trace is returned

Bug #1300632 reported by Jiri Srba on 2014-04-01
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
VerifyDTAPN
Critical
Peter Gjøl Jensen

Bug Description

Open the attached net and verify couple of times (there is random search strategy used). After about 5 tries or so,
you should get a trace that ends with "delay for ever" but it is impossible to execute this trace in the simulator
due to invariants and hence it gives NPE.

Related branches

Revision history for this message
Jiri Srba (srba) wrote :
Revision history for this message
Mathias Grund Sørensen (mathias.grund) wrote :

This is a problem in the engine; the following trace is returned:

Marking: (P0,0) (P0,0) (P1,0) (P1,0) (P6,0)
 Delay: 7
 Marking: (P0,7) (P0,7) (P1,0) (P1,0) (P6,7)
 Transistion: T0
 Marking: (P0,0) (P0,7) (P1,0) (P2,0) (P6,7)
 Delay: 3
 Marking: (P0,3) (P0,10) (P1,0) (P2,3) (P6,10)
 Transistion: T0
 Marking: (P0,0) (P0,3) (P2,0) (P2,3) (P6,10)
 Delay: 6
 Marking: (P0,6) (P0,9) (P2,6) (P2,9) (P6,10)
 Transistion: T1
 Marking: (P0,6) (P0,9) (P2,6) (P3,9) (P6,10)
 Transistion: T3
 Marking: (P0,6) (P0,9) (P2,6) (P4,0) (P5,9) (P6,10)
 Transistion: T4
 Marking: (P0,6) (P0,9) (P2,6) (P4,0) (P6,0)
 Delay: 3
 Marking: (P0,9) (P0,12) (P2,9) (P4,3) (P6,3)
 Transistion: T1
 Marking: (P0,9) (P0,12) (P3,9) (P4,3) (P6,3)
 Transistion: T3
 Marking: (P0,9) (P0,12) (P4,0) (P4,3) (P5,9) (P6,3)
 Delay: 6
 Marking: (P0,15) (P0,18) (P4,6) (P4,9) (P5,15) (P6,9)
 Transistion: T4
 Marking: (P0,15) (P0,18) (P4,6) (P4,9) (P6,0)
 Delay: 1
 Marking: (P0,16) (P0,19) (P4,7) (P4,10) (P6,1)
 Transistion: T2
 Marking: (P0,16) (P0,19) (P1,0) (P4,7) (P6,1)
 Transistion: T0
 Marking: (P0,0) (P0,16) (P2,0) (P4,7) (P6,1)
 Delay: 1
 Marking: (P0,1) (P0,17) (P2,1) (P4,8) (P6,2)
 Transistion: T2
 Marking: (P0,1) (P0,17) (P1,0) (P2,1) (P6,2)
 Delay: 2
 Marking: (P0,3) (P0,19) (P1,0) (P2,3) (P6,4)
 Transistion: T0
 Marking: (P0,0) (P0,3) (P2,0) (P2,3) (P6,4)
 Delay: Forever

Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

The error is in the engine where a loop is detected as delay forever. See attached trace where last marking
P0(0, 4), P2(0, 4) is also in the trace after second fireing of "ComposedModel.T0".

It looks like this problem has something to do with the recreation of the trace from the PTrie - hence an engine bug.

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

Yes, I just checked and without PTrie there is no problem. This is possible only if PTrie is enabled.

Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

Attached net forces the bug to appear; it occurs when a delay gives a loop. This is an issue regardless of PTries.

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

I cannot reproduce it without PTries, only with PTries.

Also, only Darts give a trace that is also wrong (not maximal).

Changed in tapaal:
status: New → In Progress
assignee: nobody → Peter Gjøl Jensen (peter-gjoel)
Revision history for this message
Jiri Srba (srba) wrote :

The last fix in verifydtapn destroys a lot of other stuff. See the attached net and verify.
It does not report "delay for ever" any more and after delaying twice 1 time unit it
announces a deadlock (that is not there).

Jiri Srba (srba) on 2014-04-04
affects: tapaal → verifydtapn
Jiri Srba (srba) on 2014-06-22
Changed in verifydtapn:
status: In Progress → Fix Released
To post a comment you must log in.
This report contains Public information  Edit
Everyone can see this information.

Other bug subscribers