How we designed and model checked MongoDB reconfiguration protocol