Hello Gunnar,\geq is an infix operator in the TLA+ language. For integers (and reals), it is interpreted as the usual "greater or equal" relation.Max is defined as a recursive function that takes as argument a set T \subseteq S of integers and returns the largest element of T, or -1 if T is empty. In particular, \geq is used to compare an element n \in T and the maximum of the set T \ {n}, so it compares integers, not sets.For your second question, SUBSET S denotes the set of all subsets of the set S. Therefore, writing T \subseteq S or T \in SUBSET S is semantically equivalent. There are some places where you must use the second form: for example, TLC will interpret x’ \in SUBSET {1,2,3} specially and generate a successor state for every subset S of {1,2,3} in which x = S (if this is the first "assignment" to x that it encounters in evaluating an action). Also, recursive function definitions such as Max expect their domain as being indicated in the form f[x \in D] == …, and therefore you must write f[x \in SUBSET S] == … when defining a recursive function that takes set arguments.Hope this helps,StephanOn 3 Apr 2025, at 19:49, Gunnar Ludwig <h199...@xxxxxxxxx> wrote:Dear TLA+ community,I try to understand PaxosCommit. There are some questions I hope you could point me to where to find an answer.# How does \geq work?Taken from the PaxosCommit there is a \geq on sets:LET Max[T \in SUBSET S] ==
IF T = {} THEN -1
ELSE LET n == CHOOSE n \in T : TRUE
rmax == Max[T \ {n}]
IN IF n \geq rmax THEN n ELSE rmax <=====
IN Max[S]As far as I get it this can be something like:{1, 2} \geq {1, 2, 3}What would be the result?# Why the difference?Taken form PaxosCommit:
PCTypeOK ==
/\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
/\ aState \in [RM -> [Acceptor -> [mbal : Ballot,
bal : Ballot \cup {-1},
val : {"prepared", "aborted", "none"}]]]
/\ msgs \in SUBSET Message <======Taken from TCommitTPTypeOK ==
/\ rmState \in [r \in RM |-> {"working", "prepared", "comitted", "aborted"}]
/\ tmState \in {"init", "done"}
/\ tmPrepared \subseteq RM
/\ msgs \subseteq Messages <========What are the results of using it with SUBSET and with out?Thanks for your help.Best,Gunnar--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/33c802e4-11d9-4222-9bd4-e0912181b1b3n%40googlegroups.com.