Difference between hot, warm?, hot states in monitors

[nvartolomei]

The documentation mentions just the hot state. Nothing is said about cold state. This discussion was helpful in describing the requirements of a spec when a cold state is defined. Seems like I grok it a little bit, but not fully.

I'm writing a toy spec involving 3 machines, client, server, partition. Client sends a message to the server, server forwards it to partition, partition responds directly to the client.

The spec below validates without any problems. However, if I remove the cold keyword from the Init state it will fails all schedules. What's special in this case about the cold state?

<ErrorLog> PImplementation.AllProduceRequestsAreHandled detected potential liveness bug in hot state 'PendingRequests'.

spec AllProduceRequestsAreHandled observes eProduceReq, eProduceResp {
    var pendingRequests: int;

    start cold state Init {
        on eProduceReq goto PendingRequests with (req: tProduceReq) {
            pendingRequests = pendingRequests + 1;
        }
    }

    hot state PendingRequests {
        on eProduceReq goto PendingRequests with (req: tProduceReq) {
            pendingRequests = pendingRequests + 1;
        }

        on eProduceResp do (resp: tProduceResp) {
            pendingRequests = pendingRequests - 1;

            if (pendingRequests == 0) {
                goto Init;
            }
        }
    }
}