It is generally difficult to determine which events/states are fair without the very solid understanding of the model. It can even become impossible when the model is big. Therefore, the process level fairness becomes more useful and intuitive.

For the partial order reduction, we only implemented for the weak fairness.

We introduce 3 different process level fairness: global fairness, strong fairness and weak fairness (where Spin can cover only part of weak fairness). The definitions of the 3 fairness can be found in the following paper:
M. J. Fischer and H. Jiang. Self-stabilizing leader election in networks of finite-state anonymous agents. In Proc. 10th Conference on Principles of Distributed Systems, volume 4305 of LNCS, pages 395-409. Springer, 2006.