starter.tla has a Spec with a bug: click Check Syntax first, and
you'll see it reports nothing wrong. Now click Run Model Checker — TLC
will refuse it with TLC cannot handle this conjunct of the spec.
Fix Spec so it's a proper always-formula TLC can use to generate an
entire behavior, not just a single-step fact. The fix is one character.