Liveness specification - cold vs hot state

[fintara]

Per documentation, "properties like eventually something holds or every event X is eventually followed by Y or eventually the system enters a convergence state" can be marked as hot state, meaning we want the system eventually [to] end in a non-hot state.

I cannot find information what cold state means, though. I have looked into the "Two Phase Commit" tutorial too, but I can't deduce what the checker does for such states.

[timmyjose]

My understanding is this - to check for liveness, we need the machine to transition to a non-hot state, right? In a simple case, this might be sufficiently expressed by having a hot state (or states) and the checker verifies that at the end of a round of operations, the machine winds up in a state which is not "hot". However, we can also mark certain states as cold to provide better assertions and tighter constraints - meaning that at the end of the round of operations, the machine ends up in one of the cold states (so a stronger guarantee than simply being in a non-hot state). The Two-Phase commit example has precisely that in its spec.