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
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.4
Hardware: PC Linux
: P2 major
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2007-02-04 12:17 CET by Gerd Behrmann
Modified: 2007-05-13 18:11 CEST (History)
1 user (show)

See Also:
Architecture:

Attachments
Test case (14.89 KB, application/octet-stream)
2007-02-04 12:18 CET, Gerd Behrmann 		Details
Query file for test case (84 bytes, application/octet-stream)
2007-02-04 12:18 CET, Gerd Behrmann 		Details
Add an attachment (proposed patch, testcase, etc.)

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.