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

Bug 267 - Verifier does not terminate
Summary: Verifier does not terminate
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Alpha 4
Hardware: All Windows 2000
: P1 critical
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2006-02-13 17:27 CET by Gerd Behrmann
Modified: 2006-03-01 15:03 CET (History)
0 users

See Also:
Architecture:

Attachments
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 Gerd Behrmann 2006-02-13 17:27:34 CET 
On some models, the verifier does not terminate in windows. verifyta either keeps running (progress 
messages are updated) or hangs (progress message is not updated).

The models bug114, patricia and test from the regression test suite trigger this behaviour. This behaviour 
has not been observed under Linux.
Comment 1 Gerd Behrmann 2006-02-13 21:48:55 CET 
At least for the file bug114.xta, I have now tracked this regression to the checkin at revision 1288. This 
change fixed some bugs in compressed int storage; but it seems the fix also introduced some new 
problems. I noticed that all the three models I mentioned above only have on process. This fits well with a 
theory, that the problem was introduced by the aforementioned change. The change was made by 
Alexandre; I reassign the bug to him.
Comment 2 Gerd Behrmann 2006-02-14 15:07:04 CET 
For reference, the changee in question was introduced to fix bug 223.