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

Bug 532 - The verification of a "sup" property based on a clock value does not terminate
Summary: The verification of a "sup" property based on a clock value does not terminate
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.3
Hardware: Macintosh Mac OS
: P2 normal
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2012-01-19 12:10 CET by Hang Yin
Modified: 2012-01-19 12:23 CET (History)
0 users

See Also:
Architecture:


Attachments
The xml and q files of the model (2.87 KB, application/zip)
2012-01-19 12:22 CET, Hang Yin
Details
The xml and q files of the model (2.87 KB, application/zip)
2012-01-19 12:23 CET, Hang Yin
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Hang Yin 2012-01-19 12:10:46 CET
By using traditional UPPAAL modeling and verifying techniques (the second property in the property list), it can be found that the maximal clock value in state "Waiting" of "MSTS" is 12. But the property "sup{MSTS.Waiting}: MSTS.x" does not terminate. It is expected that the same value 12 should be obtained from its verification result. The "sup" property works fine in some other states of other templates, but the reason why it does not terminate in x.N is unknown.
Comment 1 Hang Yin 2012-01-19 12:22:28 CET
Created attachment 252 [details]
The xml and q files of the model
Comment 2 Hang Yin 2012-01-19 12:23:42 CET
Created attachment 253 [details]
The xml and q files of the model