3_CommitPointPropagationLiveness.cfg

CONSTANT Follower = Follower
CONSTANT Leader = Leader
CONSTANT Nil = Nil
CONSTANT Candidate = Candidate
CONSTANT Server = {n1, n2, n3}
CONSTANT CommitPointAction <- LearnCommitPointFromSyncSourceAction
CONSTRAINT StateConstraint
SPECIFICATION Spec
PROPERTY CommitPointEventuallyPropagates