646
2017-11-02 14:26:23 +0100
simulator overshoots the floating point constraints
2017-11-02 15:47:34 +0100
1
1
1
Unclassified
UPPAAL
Engine
4.1.20
PC
Linux
ASSIGNED
P5
enhancement
---
1
marius
marius
adavid
oldest_to_newest
2079
0
marius
2017-11-02 14:26:23 +0100
Given that x is a clock, the following queries yield contradicting results:
Pr [<=100] (<> (x>0 && x<=2)) => [0.9026,1]
Pr [<=100] (<> (x>0.0 && x<=2.0)) => [0, 0.097]
The first query is analysed as constraints and is correct.
In the second query the simulator fails to detect constraints and produces unbounded delays, thus overshooting the point 2.0 and the property becomes unsatisfiable.
This particular case is simple enough to recognize the constraint and perhaps solve it like one, but in general expressions like f(x)<2.0 are not solvable, therefore an integration step should be used instead in cases where f depends on a clock.
The issue was brought up by Gabriel Domingo Vilallonga.