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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 3 Mar 2022 09:09:31 +0100*References*: <ef8335ae-08d3-42dc-a8e6-b37c5ef3d595n@googlegroups.com>

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

**References**:**[tlaplus] recursion***From:*jiaojiao cai

- Prev by Date:
**[tlaplus] recursion** - Next by Date:
**[tlaplus] TLA+-style Refinement vs. Backward and Forward Simulation** - Previous by thread:
**[tlaplus] recursion** - Next by thread:
**[tlaplus] TLA+-style Refinement vs. Backward and Forward Simulation** - Index(es):