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

[tlaplus] [Newbie Question] Engineer trying to get maths meaning


I'm trying to understand this part of the paxos specification. I'm not trying to understand how paxos works, I get that, I'm just trying to understand how to read and understand this part of the specification. 

01  /\ \E Q \in Quorum :
02        LET Q1b == {m \in msgs : /\ m.type = "1b"
03                                 /\ m.acc \in Q
04                                 /\ m.bal = b}
05            Q1bv == {m \in Q1b : m.mbal \geq 0}
06        IN  /\ \A a \in Q : \E m \in Q1b : m.acc = a 
07            /\ \/ Q1bv = {}
08               \/ \E m \in Q1bv : 
09                    /\ m.mval = v
10                    /\ \A mm \in Q1bv : m.mbal \geq mm.mbal 

On line 01 you define that Q is in set of Quorum and then lines 02-10 define what Q will be. My confusion is on Line 03 Q is referenced. How can you reference something that hasn't been assigned a value yet. 

I may very well be suffering from "... brain washing done by years of C programming".

Any help that I could get in understanding this would be greatly appreciated. Also, is there a place on the web were I can better familiarize my self with such concepts.



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/3db0a094-02e8-484b-9aae-eb2930f4e269n%40googlegroups.com.