Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM