1_LearnCommitPointFromSyncSource_5_node.cfg

CONSTANT Follower = Follower
CONSTANT Leader = Leader
CONSTANT Nil = Nil
CONSTANT Candidate = Candidate
CONSTANT Server = {n1, n2, n3, n4, n5}
SYMMETRY Symmetry
CONSTANT CommitPointAction <- LearnCommitPointFromSyncSourceAction
CONSTRAINT StateConstraint
SPECIFICATION Spec
INVARIANT NeverRollbackBeforeCommitPoint