One way to do this is to implement a Rationals module, and define your algorithm to work over the Rationals instead of the Reals. This would be amenable to finite model checking. Or, if your problem is amenable to it, define your algorithm inputs such that integer division will always give the same answer as division over the Reals.
Using floating point with model checking is difficult because you can't easily check equality between two states due to accumulation of errors.
On Friday, April 23, 2021 at 4:49:12 PM UTC-4 christin...@xxxxxxxxx wrote:
I know that TLA+ does not reason about real numbers, but can we model an algorithm which does ?
For example, if the algorithm we want to verify contains a division, and only integer division is supported in TLA+, can we go ahead and model it anyway (if we are interested in other things about it), even though the numerical answer will be wrong? My instinct is that this should not be a problem but I am not 100% sure.