On the Automated Implementation of Time-Based Paxos Using the IOA Compiler