ceph.cfg

CONSTANTS
m1 = m1
m2 = m2
m3 = m3

CONSTANTS
v1 = v1
v2 = v2

CONSTANT
Monitors = {m1,m2,m3}
Value_set = {v1, v2}

SYMMETRY SYMM

CONSTANT
Nil = Nil

CONSTANT
OP_COLLECT = OP_COLLECT
OP_LAST = OP_LAST
OP_BEGIN = OP_BEGIN
OP_ACCEPT = OP_ACCEPT
OP_COMMIT = OP_COMMIT
OP_LEASE = OP_LEASE
OP_LEASE_ACK = OP_LEASE_ACK

CONSTANT
STATE_RECOVERING = STATE_RECOVERING
STATE_ACTIVE = STATE_ACTIVE
STATE_UPDATING = STATE_UPDATING
STATE_UPDATING_PREVIOUS = STATE_UPDATING_PREVIOUS
STATE_WRITING = STATE_WRITING
STATE_WRITING_PREVIOUS = STATE_WRITING_PREVIOUS
STATE_REFRESH = STATE_REFRESH
STATE_SHUTDOWN = STATE_SHUTDOWN

CONSTANT
PHASE_ELECTION = PHASE_ELECTION
PHASE_SEND_COLLECT = PHASE_SEND_COLLECT
PHASE_COLLECT = PHASE_COLLECT
PHASE_LEASE = PHASE_LEASE
PHASE_LEASE_DONE = PHASE_LEASE_DONE
PHASE_BEGIN = PHASE_BEGIN
PHASE_COMMIT = PHASE_COMMIT

CHECK_DEADLOCK FALSE
INVARIANT Inv
INIT Init
NEXT Next
VIEW view