|Summary:||Crash during concrete trace generation|
|Product:||UPPAAL||Reporter:||Gerd Behrmann <behrmann>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
Query file for test case
Description Gerd Behrmann 2007-02-04 12:17:50 CET
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.
Comment 2 Gerd Behrmann 2007-02-04 12:18:39 CET
Created attachment 142 [details] Query file for test case
Comment 3 Gerd Behrmann 2007-02-04 12:24:20 CET
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.
Comment 4 Gerd Behrmann 2007-02-04 17:58:12 CET
Turns out to be a problem in the delay computation in the presence of open bounds in the DBM.
Comment 5 Gerd Behrmann 2007-02-04 18:01:18 CET
Correction to comment #3: I meant to say that symbolic trace generation is _not_ affected.
Comment 6 Gerd Behrmann 2007-02-04 22:49:42 CET
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.
Comment 7 Gerd Behrmann 2007-02-06 22:16:31 CET
Fixed on the 4.0 branch from rev. 2945. Still open for the trunk.