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

Bug 70

Summary: There is no intersection check for inequalities involving integers and their ranges in verifier
Product: UPPAAL Reporter: Juhan Ernits <juhan>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: ASSIGNED ---    
Severity: enhancement    
Priority: P4    
Version: 3.5.7   
Hardware: All   
OS: All   
Architecture:

Description Juhan Ernits 2003-12-03 23:13:44 CET
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.
Comment 1 Gerd Behrmann 2005-06-29 21:11:37 CEST
Moving bug to 3.5.7, as this is an enhancement bug and only bug fixes are allowed on 3.4.