From Henning Dierks: Yesterday I downloaded the latest version of Uppaal and today I observed that the trace generator (which I really need...) does not do its job all times. I added the model and the query.
Created attachment 141 [details] Test case
Created attachment 142 [details] Query file for test case
Symbolic trace generation does seem to be affected. I get the following assertion failure on the 4.0 branch with concrete trace generation: verifyta: /home/behrmann/uppaal-4.0/server/modules/verifier/Path.cpp:266: void computeConcretePath(Path*, dbm::DoubleValuation&): Assertion `zone->contains(valuation)' failed. The problem also exists on the trunk.
Turns out to be a problem in the delay computation in the presence of open bounds in the DBM.
Correction to comment #3: I meant to say that symbolic trace generation is _not_ affected.
A fix has been developed, however the algorithm seems to suffer from problems with precision of the fixed precision floating point representation used. Further investigation is needed.
Fixed on the 4.0 branch from rev. 2945. Still open for the trunk.