This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 389 - Crash during concrete trace generation
Summary: Crash during concrete trace generation
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.4
Hardware: PC Linux
: P2 major
Assignee: Gerd Behrmann
Depends on:
Reported: 2007-02-04 12:17 CET by Gerd Behrmann
Modified: 2007-05-13 18:11 CEST (History)
1 user (show)

See Also:

Test case (14.89 KB, application/octet-stream)
2007-02-04 12:18 CET, Gerd Behrmann
Query file for test case (84 bytes, application/octet-stream)
2007-02-04 12:18 CET, Gerd Behrmann

Note You need to log in before you can comment on or make changes to this bug.
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 1 Gerd Behrmann 2007-02-04 12:18:17 CET
Created attachment 141 [details]
Test case
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.