Re: [tlaplus] Re: Some user feedback

Hi Leslie,

>>I asked for explicit scenarios that you would like implemented--that
>>is, exactly what keystrokes and button pushes you would perform to
>>achieve the desired tasks. I want suggestions, not complaints.

I'm not complaining. My method of using ASSUME works well enough for me to be productive. I described it because I suspect that some people might not know about it. I described the current less-than-optimal aspects just in case someone happens to work on improvements. But such improvements would be "nice to haves" IMO -- much less important than, say, better support in TLAPS for sequences, or fixes/improvements to TLC's liveness checking, or more tutorials on how to develop the skill of finding inductive invariants.

I can't currently give a detailed scenario because I'm not currently writing a spec, and I know that memory plays tricks with details -- e.g. edits out most of the frustrations.

A basic REPL would presumably include features such as:

- Provide a scrolling history of commands and responses. This would take place in an environment like an Eclipse editor window -- i.e. allowing full navigation with the keyboard, including scrolling, and good control over selection and copy/paste (both of commands and printed output). It would also support Eclipse's useful column-oriented editing mode, just as the Toolbox already does when editing a spec. In all cases, bullet-lists of conjunctions and disjunctions would have the correct semantics.

- Be logged to a file on the fly, for posterity.

   - Allow modules to be extended and instantiated, and constants and variables to be declared.

   - Allow operators to be defined and re-defined. A re-definition would immediately affect any other existing operators which use (directly or indirectly) the symbol that has been changed. Comments in definitions would be preserved.

   - Provide a way to associate a top-level comment with each operator.

- Provide a command to display the definition of any symbol. Comments in definitions would be preserved.

- Provide a command to dump the declarations & definitions of all current symbols to a file in appropriate order. Comments in definitions would be preserved.

- Allow expressions to be evaluated.

- Allow a key-press (presumably Ctrl-C) to promptly interrupt a long-running evaluation.

- Allow explicit temporary local binding (shadowing) of constants and variables, to test operators. This would only be allowed in commands that did not have side-effects. i.e. It would not be allowed when defining or redefining a symbol.

- Feel very responsive for all commands other than non-trivial evaluations.

I'm sure that modern REPLs have a laundry list of other features that might be adapted.

>>TLC pretty-prints all values that it outputs.

I didn't realize that. My recollection is that output from Assert(_,_) and PrintT(_) of complex nested structures would occasionally be so hard to read that I would copy/paste it into a text editor and manual reformat it a bit, to clarify a problem. It's been a while since I've had to do that though, so my memory is hazy.

A structured viewer would be very welcome of course. Ideally such a viewer could be used from the keyboard alone, avoiding the mouse. Indeed, avoiding use of the mouse would be a good high-level goal. Using TLC currently requires using the mouse quite a lot, whereas using TLAPS can be done mostly from the keyboard.

regards,
Chris

[1] http://java.dzone.com/articles/eclipses-awesome-block

On Sun, Nov 23, 2014 at 2:42 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

Hi Chris,
I asked for explicit scenarios that you would like implemented--that
is, exactly what keystrokes and button pushes you would perform to
achieve the desired tasks. I want suggestions, not complaints.
   Time taken to start TLC. I assume most of the cost is due to spawning
   a new JVM on every invocation, and most JVMs are very slow to start.
Simon Zambrovski tried to run TLC inside the Toolbox's JVM, but
failed. He was unable to write the appropriate code to re-initialize
everything so a single instance of TLC could be run more than once.
My memory says that he re-initialized everything he could find to
re-initialize, but it still didn't work.
   Lack of a pretty-printer for complex expressions
TLC pretty-prints all values that it outputs. If you think you can do
a better job, it should be easy to find and replace the existing
pretty-printer. In fact, the current one was written by Mark Tuttle
because he didn't like the way Yuan's code was printing values.
However, Mark is a pretty bright guy and I suspect that you wouldn't
do much better. I think you'd find that every change you made to make
it work better on some output will make it do worse on other output.
You might be happier with a structured viewer like the one for values
of variables in the trace explorer.
Leslie

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.