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
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Alpha 1
Hardware: PC Linux
: P1 major
Assignee: Alexandre David
Depends on:
Reported: 2005-11-18 16:07 CET by John Håkansson
Modified: 2005-11-21 21:29 CET (History)
0 users

See Also:

system (606 bytes, text/plain)
2005-11-18 16:08 CET, John Håkansson
Query (20 bytes, text/plain)
2005-11-18 16:09 CET, John Håkansson
A simpler test case (model). (638 bytes, text/xml)
2005-11-19 18:48 CET, Gerd Behrmann
A simpler test case (model). (630 bytes, text/xml)
2005-11-19 18:49 CET, Gerd Behrmann

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]
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.