Re: [tlaplus] Problem with instance substitutions

["Rodrigo Q. Saramago" <deepma...@xxxxxxxxx>]

Please consider the spec below, the previous one had a mistake in Init step, due to some tests that I'm doing here.

------
VARIABLE maxVBalPerInst,maxValPerInst,msgsPerInst

MPaxos(i) == INSTANCE Paxos WITH maxVBal  <- maxVBalPerInst[i],
                                 maxVal   <- maxValPerInst[i],
                                 msgs     <- msgsPerInst[i]
...
Init == /\ maxVBalPerInst  = [i \in Instances |-> [a \in Acceptor |-> -1]]
        /\ maxValPerInst   = [i \in Instances |-> [a \in Acceptor |-> None]]
        /\ msgsPerInst    = [i \in Instances |-> {}]
...
Phase1b(a) == \A i \in Instances: MPaxos(i)!Phase1b(a)
...
------