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

[Frank Eaves <frankeaves72@xxxxxxxxx>]

Hi,

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.

Thanks,

-Frank

-- 
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.