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

Bug 646 - simulator overshoots the floating point constraints
Summary: simulator overshoots the floating point constraints
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.20
Hardware: PC Linux
: P5 enhancement
Assignee: Marius Mikučionis
Depends on:
Reported: 2017-11-02 14:26 CET by Marius Mikučionis
Modified: 2017-11-02 15:47 CET (History)
1 user (show)

See Also:


Note You need to log in before you can comment on or make changes to this bug.
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.