[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx>*Date*: Fri, 21 Aug 2020 09:58:06 -0700 (PDT)*References*: <6108b306-0d5a-4a0f-80bf-6c56ebefc51fn@googlegroups.com> <2DCACC85-ABF7-46A0-8718-40EE5785F56F@gmail.com>

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f9fd9da4-02b6-48fe-84b9-c79dab04bfacn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] When to prefer function or operator?***From:*Stephan Merz

**References**:**[tlaplus] When to prefer function or operator?***From:*thomas...@xxxxxxxxx

**Re: [tlaplus] When to prefer function or operator?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] When to prefer function or operator?** - Next by Date:
**Re: [tlaplus] When to prefer function or operator?** - Previous by thread:
**Re: [tlaplus] When to prefer function or operator?** - Next by thread:
**Re: [tlaplus] When to prefer function or operator?** - Index(es):