Split hot method ModelChecker#doNext into smaller chunks to facilitate runtime inlining.
Split hot method ModelChecker#doNext into smaller chunks to facilitate
runtime inlining.

Part I: Extract error handling into methods

[Refactor][TLC]

lemmy/tlaplus,lemmy/tlaplus,tlaplus/tlaplus,lemmy/tlaplus,lemmy/tlaplus,tlaplus/tlaplus,tlaplus/tlaplus,tlaplus/tlaplus