Dear Çagatay,
I don't have time to answer your email now, but I just want to point out one thing.
True, but one problem
is that these expressions are evaluated at *every state* of the trace, and the
whole trace disappears in a huff if the _expression_ fails at any state.
First, I hope your realize that you can make the trace reappear by clicking on "Restore". Here's how you can evaluate an _expression_ on an individual state in a trace. Clicking on the state displays a TLA+ formula describing the state. Copy it into your (notebook) spec and use it as the initial state of a specification. Define a next-state action that will produce an error when evaluated--for example,
Next == 0 = x'
if x is a variable of the spec. Running TLC on that initial predicate / next-state relation will produce an error trace consisting of the one state you're interested in. You can explore that one-state trace at will. Of course, I'm not saying that you should have to do all that. This is just a way of simulating the functionality that you want so you can see how often you want to use it. None of the things that you and others would like to see are going to be implemented soon, since there is no one to implement them. So, we have plenty of time to figure out what should be implemented.
And I suggest that you stop thinking in terms of typing. People don't want to type
eval some-complex-_expression_ on log[14]
onto a roll of virtual paper. For one thing, they don't want to have to copy and paste the _expression_ every time they want to evaluate it. And they don't want to have to remember that it's "eval ... on log[14]" and not "evalute ... on state[14]". They want to type the _expression_ into something like the Error-Trace Exploration window,then right-click on state 14 and choose "evaluate on state".
Cheers,
Leslie