| Summary: | The verification of a "sup" property based on a clock value does not terminate | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Hang Yin <young.hang.yin> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | normal | ||
| Priority: | P2 | ||
| Version: | 4.1.3 | ||
| Hardware: | Macintosh | ||
| OS: | Mac OS | ||
| Architecture: | |||
| Attachments: |
The xml and q files of the model
The xml and q files of the model |
||
Created attachment 252 [details]
The xml and q files of the model
Created attachment 253 [details]
The xml and q files of the model
|
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.