| 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, 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 visit https://groups.google.com/d/msgid/tlaplus/FBACDC83-3D69-419D-866D-A3639EA8A3DB%40gmail.com. |