CONSTANTS
  Shards = {s1, s2, s3}
  Vnodes = {1, 2, 3, 4, 5}
  Nodes = {n1, n2}
  MaxVnode = 5
  Nil = Nil

INIT Init
NEXT Next

CHECK_DEADLOCK FALSE

INVARIANTS
  TypeOk
  VirtualNodeMapping
  NodeAssignmentConsistency
  VnodeOrdering
SYMMETRY Symmetry