Bug 223

Summary: Invalid verification results when using Compact Data Structure
Product: UPPAAL Reporter: John Håkansson <johnh>
Component: EngineAssignee: Alexandre David <adavid>
Status: RESOLVED FIXED    
Severity: major    
Priority: P1    
Version: 3.6 Alpha 1   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: system
Query
A simpler test case (model).
A simpler test case (model).

Description John Håkansson 2005-11-18 16:07:17 CET
 
Comment 1 John Håkansson 2005-11-18 16:08:36 CET
Created attachment 70 [details]
system
Comment 2 John Håkansson 2005-11-18 16:09:25 CET
Created attachment 71 [details]
Query
Comment 3 Gerd Behrmann 2005-11-19 18:37:57 CET
Confirmed. Very interesting.
Comment 4 Gerd Behrmann 2005-11-19 18:44:42 CET
UPPAAL provides the wrong answer when verifying the attached system with the
Compact Data Structure option (which is the default for verifyta and not for the
GUI).

Running verifyta in debug mode causes an exception failure in
CompressIntStorage.cpp.
Comment 5 Gerd Behrmann 2005-11-19 18:48:30 CET
Created attachment 72 [details]
A simpler test case (model).

I have attached a simpler model. The bug does not depend on the use of an
array, hence I removed the array from the test case.
Comment 6 Gerd Behrmann 2005-11-19 18:49:29 CET
Created attachment 73 [details]
A simpler test case (model).
Comment 7 Gerd Behrmann 2005-11-19 18:58:02 CET
Alexandre, I get an assertion failure at line 905 in CompressIntStorage.cpp when
verifying the attached model with the use of compact data storage (no options on
verifyta). It seems that the CompressIntStorage cannot handle a vector of length
1 containing the value -1. Can you check it out? Thanks.
Comment 8 Gerd Behrmann 2005-11-21 21:29:33 CET
A fix is in CVS.