Open bts opened 8 years ago
Hi Brian,
May be too late an reply. I am using following model: Replicas <- {0, 1, 2} \* Can be any set. Do make sure the number is consistent with 2f + 1 rule
Commands <- {10, 20, 30} \* can be any set of commands
FastQuorums(r) <- {a \in SUBSET Replicas: r \in a /\ Cardinality(a) = ((Cardinality(Replicas) \div 2) + ((Cardinality(Replicas) \div 2) + 1) \div 2)}
SlowQuorums(r) <- {a \in SUBSET Replicas: r \in a /\ Cardinality(a) = ((Cardinality(Replicas) \div 2) + 1) }
MaxBallot <- 10 \* can be any number greater than 1
Hi there,
I'm working through understanding the TLA+ verification, and I was wondering if you could help with some information (e.g. some valid inputs) for the constants to instantiate the model?
Thanks! Brian