| Summary: | Dynamic creation of process do not cooperate with floating point type | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Daishengxin <daishengxin> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | normal | CC: | adavid, marius |
| Priority: | P5 | ||
| Version: | 4.1.19 | ||
| Hardware: | PC | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: |
Model to produce the bug
Minimal Example |
||
Thanks for the report. I'll assign this to Danny. 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.
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. |
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. Thanks.