UPPAALModelChecker / UPPAAL-Meta

This is the offcial meta repo for issue reporting, feature request and public roadmap for the development of UPPAAL.
http://www.uppaal.org
1 stars 0 forks source link

Rounding when passing array of double by value #244

Open mikucionisaau opened 10 months ago

mikucionisaau commented 10 months ago

Describe the bug Floating point values get rounded when a function is called and an array of doubles is passed by value.

To Reproduce Consider declarations:

typedef double input_t[2];
input_t in = { 1.5, 2.5 };

double f0(input_t &t) { return t[0]; }

double f1(input_t t){ return t[1]; }

double res0;
double res_f0;

double res1;
double res_f1;

And automaton: image

Switch to Concrete Simulator and observe the state of variables after the transition: image

Similarly the query simulate [<=20000; 1] { res0, res_f0, res1, res_f1 }: image

Expected behavior The value of res_f1 is expected to 2.5, but the simulator shows 2.0.

Version(s) of UPPAAL tested

UPPAAL 5.0.0 (rev. 714BA9DB36F49691), 2023-06-21 UPPAAL 5.1.0-beta5 (rev. C7C01B0740E14075), 2023-12-11

Additional context Passing by reference works correctly. It looks like the fractions get lost upon array assignment during passing-by-value.

The model attached: problem_with_double_arrays_functions.xml.zip

Originally reported by Ulrik Mathias Nyman.