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

Bug 389

Summary: Crash during concrete trace generation
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: ASSIGNED ---    
Severity: major CC: dierks
Priority: P2    
Version: 4.0.4   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: Test case
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 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.