Expose simulator state in the REPL

[shonfeder]

@plafer's excellent feedback in https://github.com/informalsystems/tnt/discussions/435#discussioncomment-4422672 have highlighted some of the pitfalls new comers might hit as they learn to work with actions and state variables in the REPL.

One thing we can do to help build up intuitions about how the simulator is working is to expose it in the repl. Here are a few ideas (enumerated as bullet points so we can easily factor out into smaller issues):

• [ ] keep a counter of which state frame you are in, and increment it every time a transition is applied
• [ ] add a command like .state that would print all current state variables
• [ ] add commands .next and .prev that will advance or retract the to move forward or backwards in a stack of states
• [ ] give a warning when we move into a state with undefined variables?

Here's a mock interaction, just to sketch out the ideas, not to push a particular rendering:

[0]>>> var x: int

[0]>>> var y: str

[0]>>> val r = {x: x, y: y}

[0]>>> all {x' = 1, y' = "foo"}
true

[1]>>> .state
var x = 1
var y = "foo"

[1]>>> all {x' = x + 1, y' = "bar"}
true

[2]>>> .state
var x = 2
var y = "bar"

[2]>>> .prev
true

[1]>>> .state
var x = 1
var y = "foo"

[1]>>> x' = 0
true
warning: variable `y` is undefined in the current state s2

[2]>>> .state
val x = 1
var y = <undefined>

It would also be slick to eventually support some amount of branching and choice, but I think for now we can just keep it linear, and accept that applying new actions in a state n via det or non-det means will just truncate any states > n.

[plafer]

Yes, any kind of introspection into the REPL is a great idea for debugging and learning the language!