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

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



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 <thomasgebert@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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
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/3C7DBF0C-D094-4360-97B0-C1BA42D07103%40gmail.com.