States of (correct) validators.
Validators have internal states. For correct validators, i.e. the ones that follow the protocol, the internal states must contain certain information that is prescribed by the protocol, which we model here. For faulty validators, i.e. the ones that do not (always) follow the protcol, we do not need to model the internal state, because what matters in our model is only the effect that faulty validators may have on correct ones, via messages exchanged over the network.