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

[ivan-gavran]

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 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).

[ivan-gavran]

@angbrav , would a feature like that be useful for you? (looking back on your modelling experience)

[angbrav]

@angbrav , would a feature like that be useful for you? (looking back on your modelling experience)

Sure, I think it is a good idea.