Translate ReplicaEngine model from PlusCal code

The previous commit had the finished PlusCal code but the translated
model was from a much older version in its history. This commit updates
it so they are in sync.

Author: DaveCTurner