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

Bug 376

Summary: Bug in stepBack
Product: UPPAAL Reporter: Alexandre David <adavid>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: RESOLVED FIXED    
Severity: critical    
Priority: P1    
Version: 4.0.3   
Hardware: All   
OS: All   
Architecture:
Attachments: Test case

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.