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

*From*: Thomas Gebert <thomasgebert@xxxxxxxxx>*Date*: Mon, 23 Dec 2019 13:02:23 -0800 (PST)*References*: <076e423b-fe5b-4046-a9c4-bb7077e80f01@googlegroups.com> <3C7DBF0C-D094-4360-97B0-C1BA42D07103@gmail.com>

In this case the function space is rather large; how would i go about doing a sort on a function? The keys are in no particular order; is there a simple enough way to turn a function into a sequence of tuples (<<key,value>>)?

On Monday, December 23, 2019 at 6:22:53 AM UTC-5, Stephan Merz wrote:

-- On Monday, December 23, 2019 at 6:22:53 AM UTC-5, Stephan Merz wrote:

Hello,using the generic definitionsRange(f) == { f[x] : x \in DOMAIN f }Min(S) == CHOOSE s \in S : \A t \in S : s <= tyou can write Min(Range(f)) to denote the minimum value that a function f takes, and TLC will be able to evaluate that _expression_ as long as the domain of f is non-empty and finite. The generalization to find the N smallest values is left as an exercise to the reader. :-)Evaluating the above definitions takes quadratic time in the domain of the function. If your function has a somewhat big domain and if both domain and co-domain are ordered, it may be worthwhile to sort the array (function) first.Hope this helps,StephanOn 23 Dec 2019, at 06:24, Thomas Gebert <thomas...@xxxxxxxxx> wrote:Hello!I am currently trying to find the minimum value in a function; is there a relatively easy way to do this in TLA+?Also, is there a way to get the N smallest values in a function?--

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 tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/076e423b-fe5b- .4046-a9c4-bb7077e80f01% 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/67e9079a-443d-4b28-a9f2-36ac7378d36f%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] TLA+ minimum of function/sequence***From:*Stephan Merz

**References**:**[tlaplus] TLA+ minimum of function/sequence***From:*Thomas Gebert

**Re: [tlaplus] TLA+ minimum of function/sequence***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLA+ minimum of function/sequence** - Next by Date:
**Re: [tlaplus] TLA+ minimum of function/sequence** - Previous by thread:
**Re: [tlaplus] TLA+ minimum of function/sequence** - Next by thread:
**Re: [tlaplus] TLA+ minimum of function/sequence** - Index(es):