| 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: | |||
By using traditional UPPAAL modeling and verifying techniques, it can be found that the maximal clock value in state A of template x is N. But the property "sup{x.A}: x.N" does not terminate. It is expected that the same value N should be provided 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. I don't know how to upload the UPPAAL files, otherwise it is easier to demonstrate this problem.