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

Bug 600 - Dynamic creation of process do not cooperate with floating point type
Summary: Dynamic creation of process do not cooperate with floating point type
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.19
Hardware: PC All
: P5 normal
Assignee: Marius Mikučionis
Depends on:
Reported: 2015-10-22 14:46 CEST by Daishengxin
Modified: 2019-03-23 12:16 CET (History)
2 users (show)

See Also:

Model to produce the bug (2.02 KB, text/xml)
2015-10-22 14:46 CEST, Daishengxin
Minimal Example (1.11 KB, text/xml)
2015-10-23 12:02 CEST, Danny Bøgsted Poulsen

Note You need to log in before you can comment on or make changes to this bug.
Description Daishengxin 2015-10-22 14:46:59 CEST
Created attachment 282 [details]
Model to produce the bug

Hi There:
 I am trying to uilize the Dynamic creation of process feature, and find this feature can not deal with the floating point variable.
 Open the attached model.
 I modeled a generator Gen,which periodically generates Dyn. And in Dyn, a variable named t is used to bound the time delay. The problem comes like this:
 If t is declared as double and the decimal place is zero e.g. 4.0, the model works fine, however, if the decimal place is not zero e.g. 4.3, a time-locked is reported when the time is infinitely close to 4.3 e.g. 4.299999999.....
 If t is declared as hybrid clock, an invariant t'==0 is added in Gen, the problem is the same, if the decimal place is zero, the model works fine, but if it is not, an error "Sucessor state does not satisfy invariant" is reported.
 I am not sure this is a bug or dynamic creation was desined to not work with floating point type.
Comment 1 Marius Mikučionis 2015-10-22 14:53:15 CEST
Thanks for the report.
I'll assign this to Danny.
Comment 2 Danny Bøgsted Poulsen 2015-10-23 12:02:57 CEST
Created attachment 283 [details]
Minimal Example

The problem is not related to dynamic process instantiation but due to the mix of equality, urgent channel and floating points. 

Attached is a minimal example with no dynamic processes which exhibits the behaviour. 

After some investigations it appears the problem is due to the following: in the initial state, when selectinga delay, Uppaal will select a value between 0 and 4.3 (and disregard the fact that the urgency of urg! should enforce the delay to be selected between 0 and 2.65). This means Uppaal quite often (almost guaranteed)  will overshoot and not find the time x==2.65 thus the urgent edge will never be followed- In consequence, Uppaal delays till  x == 4.3 and exhibits a time lock.

So why does it work if t = 4.0? The discretisation step of Uppaal "fixes" the problem here! Since t is a floating point variable then the system is marked as hybrid enforcing Uppaal to select delays of at most d (where d is given by the user) - this ensures that Uppaal will reach the time point where x==2 and the urgent edge is enabled. Changing d to 0.3 triggers here as well.
Comment 3 Marius Mikučionis 2019-03-23 12:16:24 CET
I'll take this, the issue is with the precision of floating point operations:

1) one should not expect absolute precision with floating point numbers i.e. the floating point numbers are not real and thus it is unrealistic to expect precise values.
In practice it means that one should allow some epsilon neighbourhood, and in this case change to greater than or equal solves the issue (the transition is urgent anyway).

2) it would be nice to implement approximate equality checks in the engine natively with specific precision.
The original model does not seem to show this issue anymore with 4.1.20 release, but Danny's model still trigger it.