Accept has not ever been enabled with model "2P2B2V" in UniversalPaxosStore

[hengxin]

Module: UniversalPaxosStore
Model: 2P2B2V
Result: 9 diameter, 218 states, 37 distinct states

Problem: Accept has not ever been enabled

TODO:

• Confirm the model checking result
• Is it normal for "2P2B2V"? Find bugs or Explain it.

[hengxin]

This is an error in spec:

Quorum == {Q \in SUBSET Participant : Cardinality(Q) * 2 = NP + 1}

should be

Quorum == {Q \in SUBSET Participant : Cardinality(Q) * 2 >= NP + 1}