| Summary: | There is no intersection check for inequalities involving integers and their ranges in verifier | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Juhan Ernits <juhan> |
| Component: | Engine | Assignee: | Gerd Behrmann <behrmann> |
| Status: | ASSIGNED --- | ||
| Severity: | enhancement | ||
| Priority: | P4 | ||
| Version: | 3.5.7 | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
Moving bug to 3.5.7, as this is an enhancement bug and only bug fixes are allowed on 3.4. |
Given an integer variable x with range [l,h] and a property involving x x ¤ Const (where ¤ in {<,>,>=,<=,==}) The verifier should check if the intersection between the range of the integer variable and the inequality yields a non-empty set of integers. If it yields an empty set, then a _warning_ should be issued, indicating that it is likely that there is some lack of conformity between the model and the specification. In any case, such inequality can be syntactically replaced by "false" in the property specification, thus simplifying the property to be checked. In the case of "x != Const", if Const is not in [l,h] then the inequality can be syntactically replaced by "true". Again, a warning should be issued to the user.