Hello,indeed, assuming that you are not interested in making explicit the domain of the function, there is no big difference between the two. You shouldn't see any noticeable difference when using TLC or TLAPS either.Regards,StephanOn 21 Aug 2020, at 18:58, thomas...@gmail.com <thomas...@xxxxxxxxx> wrote:Thanks for getting back to me.So in my example, from a direct specification perspective, it doesn't matter much; does it affect anything in regards to TLC or TLAPS? Does using an operator perform better during model checking?On Friday, August 21, 2020 at 10:41:26 AM UTC-4 Stephan Merz wrote:Section 6.4 of Specifying Systems has a thorough discussion of the tradeoffs between functions and operators [1]. The conclusion is as follows:When defining an object V, you may have to decide whether to make V an operator that takes an argument or a function. The differences between operators and functions will often determine the decision. [...] If these differences don’t determine whether to use an operator or a function, then the choice is a matter of taste. I usually prefer operators.Regards,Stephan[1] Since the publication of Specifying Systems, recursive operator definitions have been added to TLA+ and therefore the arguments about recursive definitions no longer apply.On 21 Aug 2020, at 16:34, thomas...@gmail.com <thomas...@xxxxxxxxx> wrote:There are cases when either a function or operator will solve a task more-or-less equivalently.For example, both this function and operator accomplish a roughly-equivalent result:addOne[x \in Nat] == x + 1
addOneOperator(x) == x + 1
My question is: when either an operator or function will accomplish a job, which one would you prefer? What are the tradeoffs?--
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/6108b306-0d5a-4a0f-80bf-6c56ebefc51fn%40googlegroups.com.
--
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/f9fd9da4-02b6-48fe-84b9-c79dab04bfacn%40googlegroups.com.