If your algorithm does not at all depend on the result of division, you can replace it by a constant parameter Div(_,_). For theorem proving, you should then be able to prove the properties that you are interested in. For model checking, you will still need to provide an instance of that operator, sayDiv(x,y) == 42but you can run TLC with different definitions to become confident that the definition is indeed irrelevant. However, if this is true, it sounds like you could write an even more abstract specification, such as getting rid of variables to which division is applied.If your algorithm depends on certain properties of division but not the precise result you can state those in an ASSUME clause, say,ASSUME \A x,y \in Int : y # 0 => Div(x,y) \in Int /\ Div(x,y) < xStephanOn 23 Apr 2021, at 22:49, christin...@gmail.com <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.--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d4b24a56-e945-48b4-af19-b8a16872a87dn%40googlegroups.com.