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

Bug 223

Summary: Invalid verification results when using Compact Data Structure
Product: UPPAAL Reporter: John Håkansson <johnh>
Component: EngineAssignee: Alexandre David <adavid>
Severity: major    
Priority: P1    
Version: 3.6 Alpha 1   
Hardware: PC   
OS: Linux   
Attachments: system
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]
Comment 2 John Håkansson 2005-11-18 16:09:25 CET
Created attachment 71 [details]
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

Running verifyta in debug mode causes an exception failure in
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.