Wrong trace delay - fix 2035819

[mtygesen]

Fix for:
https://bugs.launchpad.net/tapaal/+bug/2035819

[srba]

One could have set the max constant to 0 already at line 122 with the same effect (at least from a quick look). I am though afraid that this could kill some of the optimizations as if the constant is -1 the engine regards it essentially as untimed place. I think that maybe one could set it to 0 at line 122 only if we ask for the fastest trace, otherwise we could leave it at -1. What do you think @petergjoel ?

[petergjoel]

Unfortunately I think this fix is coincidental (or at least not the right fix). AFAIK, the fastest trace is preserved even by the local pruning, so changing the max-constant should not impact the existence of the fastest trace.

The adverse effect of this fix is an exponential blowup in the statespace when we have untimed places (they can now have the value 0 and 1 as delay), so it is not a light cost, even if the fix is correct.

But it indicates that something fishy is going on during the extrapolation/pruning operation.
I still have a hunch that it is down to the next-state computation order somehow messing up the search order OR the stored trace.

Some things to check:

1. on termination, is the search stack still neatly ordered?
2. do we add a "predecessor" in the trace too early due to ordering? (check https://github.com/TAPAAL/verifydtapn/blob/main/src/DiscreteVerification/DataStructures/PWList.cpp line PWListHybrid::add Specifically, should we sometimes store another predecessor as the parent, not just the first?