What are valid values for instantiating the TLA+ model?

[bts]

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

[nibeshrestha]

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