Bug 376 - Bug in stepBack
Summary: Bug in stepBack
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.3
Hardware: All All
: P1 critical
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-12-12 14:00 CET by Alexandre David
Modified: 2006-12-22 16:39 CET (History)
0 users

See Also:
Architecture:


Attachments
Test case (779 bytes, text/xml)
2006-12-22 15:48 CET, Gerd Behrmann
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Alexandre David 2006-12-12 14:00:32 CET
The implementation of stepBack does not take into account the pre and post assignments.
Comment 1 Gerd Behrmann 2006-12-22 15:48:14 CET
Created attachment 135 [details]
Test case

When generating a concrete trace (option -t0 of verifyta) to location l, the necessary delay of 20 is not generated.
Comment 2 Gerd Behrmann 2006-12-22 16:25:59 CET
Fixed on the trunk from rev. 2877.
Comment 3 Gerd Behrmann 2006-12-22 16:39:24 CET
Fixed on the 4.0 branch from rev. 2878.