| Hello, I am not sure I fully understand what you are trying to achieve (also, your data structure really appears to be a sequence, not a set, because you assume an order on the entries). Here is a suggestion for part of your problem: given an index i into the sequence, find the closest index for which the associated entry has its flag set to true, otherwise return 0 (which is not a valid sequence index). I presume that this should help you write the function that you are actually interested in. \* the smallest integer in S, 0 if S is empty Least(S) == IF S = {} THEN 0 ELSE CHOOSE i \in S : \A j \in S : i <= j FindNextTrueEntry(seq, i) == Least({j \in i+1 .. Len(seq) : seq[j].flag}) Note that the Community modules [1] contain the definition of Min, which is similar to Least above, except it assumes that the set is non-empty. You could write a recursive definition of the operator, but a purely set-theoretic definition like the above is often easier to read. Hope this helps, Stephan [1] https://github.com/tlaplus/CommunityModules/blob/master/modules/FiniteSetsExt.tla
--
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/854D0551-F606-420C-B3B1-4467F6AEE0BB%40gmail.com. |