[tlaplus] TLA+ basic question

[Gunnar Ludwig <h19900401@xxxxxxxxx>]

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

-- 
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/33c802e4-11d9-4222-9bd4-e0912181b1b3n%40googlegroups.com.