70
2003-12-03 23:13:44 +0100
There is no intersection check for inequalities involving integers and their ranges in verifier
2005-11-06 18:23:01 +0100
1
1
1
Unclassified
UPPAAL
Engine
3.5.7
All
All
ASSIGNED
P4
enhancement
---
1
juhan
behrmann
oldest_to_newest
165
0
juhan
2003-12-03 23:13:44 +0100
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.
521
1
behrmann
2005-06-29 21:11:37 +0200
Moving bug to 3.5.7, as this is an enhancement bug and only bug fixes are allowed on 3.4.