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