The following SAL files illustrate the application of calendar automata to the modeling of real-time systems. Both are inspired from the TTA fault-tolerant startup protocol. The verification builds an abstraction of the protocol that is proved correct using the SAL infinite-state, bounded model checker. A correctness property is then derived from the abstraction.