[FEATURE] Easier debugging of TLA+ model using partial runs

Anecdotally, an important part of developing a TLA+ model and debugging it is using trace invariants to describe a sequence of transitions that should be possible under the model. Negating them and finding a counterexample would then confirm the intuition (whereas not finding it would suggest something was wrong).

As a convenience feature, Modelator could accept a simple representation of a run (perhaps in a JSON form, not necessarily with all variables set) and automate a couple of steps to produce a full run.

This feature is related to the idea of [runs](https://github.com/informalsystems/tnt/blob/igor/runs344/doc/lang.md#runs) and perhaps we could use some of the syntax (although, I'd prefer to keep it as simple as possible, since it is a debugging tool).