Learning fun things like that the TLA+ model checker call stack for evaluating a next state predicate goes:
ITool#getNextStates()
Tool#getNextStatesImpl()
Tool#getNextStatesAppl()
Tool#getNextStatesApplImpl()
Tool#getNextStatesApplImplSwitch()

#TLAPlus