Precision bug, rounding error in int/real mixed expressions
Marcel Steinmetz (@steinmetz) and me are working on a Jani model of the race track domain. In Modest the positions in the grid are not calculated correctly. We suppose that there is a precision bug, a rounding error or a problem with mixed int/real expressions. The critical action seems to be around line 455 in this file: rt.jani. All varaibles involved in the calculations are integers and the result should again be an integer. In our case the result for one of the coordinates is -2 instead of -1. To make sure that the problem is not caused by a modelling error in the Jani file, we removed the 2D arrays not supported by Storm and hardcoded these information. In this case Storm returns the correct results.
If needed, we can try to find a minimal example where this error occurs but we are not sure how large this will be. The domain represented in the file above looks like this:
dimensions: 1 3
start empty_location goal