| Summary: | Invalid verification results when using Compact Data Structure | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | John Håkansson <johnh> |
| Component: | Engine | Assignee: | 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
Created attachment 70 [details]
system
Created attachment 71 [details]
Query
Confirmed. Very interesting. 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. 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.
Created attachment 73 [details]
A simpler test case (model).
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. A fix is in CVS. |