Re: [tlaplus] TLA+ minimum of function/sequence

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:

Hello,

using the generic definitions

Range(f) == { f[x] : x \in DOMAIN f }
Min(S) == CHOOSE s \in S : \A t \in S : s <= t

you 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,
Stephan

On 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.