Bug 646

Summary: simulator overshoots the floating point constraints
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: enhancement CC: adavid
Priority: P5    
Version: 4.1.20   
Hardware: PC   
OS: Linux   

Description Marius Mikučionis 2017-11-02 14:26:23 CET
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.