7.2 Example: 1-Bit clock in TLA+