Impossible trace is returned

[Jiri Srba]

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.

[Mathias Grund Sørensen (mathias.grund)]

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

[Peter Gjøl Jensen (peter-gjoel)]

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.

[Jiri Srba (srba)]

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

[Peter Gjøl Jensen (peter-gjoel)]

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

[Jiri Srba (srba)]

I cannot reproduce it without PTries, only with PTries.

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

[Jiri Srba (srba)]

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