TLA+ basic question

[Gunnar Ludwig]

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 TCommit

TPTypeOK ==
    /\ 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

[Stephan Merz]

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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/33c802e4-11d9-4222-9bd4-e0912181b1b3n%40googlegroups.com.

[Gunnar Ludwig]

Hello Stephan,

thanks a lot for your quick answer. I appreciate your patients and time to ramp up beginner on the topic. It was really a great help for me.

Best,

Gunnar