INIT Init
NEXT Next

CONSTANT
  Nodes = {"Node1", "Node2"}
  Clients = {"Client1", "Client2", "Client3"}
  MaxVersion = 5
  MaxWrites = 10