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

Bug 223 - Invalid verification results when using Compact Data Structure
Summary: Invalid verification results when using Compact Data Structure
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Alpha 1
Hardware: PC Linux
: P1 major
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2005-11-18 16:07 CET by John Håkansson
Modified: 2005-11-21 21:29 CET (History)
0 users

See Also:
Architecture:

Attachments
system (606 bytes, text/plain)
2005-11-18 16:08 CET, John Håkansson 		Details
Query (20 bytes, text/plain)
2005-11-18 16:09 CET, John Håkansson 		Details
A simpler test case (model). (638 bytes, text/xml)
2005-11-19 18:48 CET, Gerd Behrmann 		Details
A simpler test case (model). (630 bytes, text/xml)
2005-11-19 18:49 CET, Gerd Behrmann 		Details
Show Obsolete (2) Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
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.