Some user feedback

[James Fisher]

I started to reply to a different thread, but it grew out of

control. I thought I would put down some of my experiences with TLA+

after a short time using it, in the hope that my user feedback is

helpful to goal of attracting new users.

A little about me: I am a professional programmer with an academic

background. I found out about TLA+ via a paper about its use at AWS,

then I watched Leslie's fantastic talk "Thinking for Programmers". I

was quickly attracted to TLA as a simple formalism which might help me

reason about my work in ways that other formalisms have not

particularly helped me. I was attracted to TLA+ for the model checker

and as a way to introduce formal specification into teams of

"practical" programmers (as I see AWS is doing). I work in

environments where even informal specification is unfashionable. I

have currently been reading about and playing with TLA+ for a few days

outside of work.

My first bad experience was visiting (what I thought was) the

"official" website to find that it is broken. I expect a lot of

curious readers would give up right here: it's a signal that the

project is small or dead. TLA+ needs to put the web first and sort out

the tlaplus.net domain. In the mind of the programmer, things without

a dedicated domain name barely qualify as existing. Even the most

obscure software tools have official websites with an element of

community-owned spirit. A domain name builds identity; a

"please-don't-copy-this-UUID" string doesn't.

My second bad experience was attempting to find the documentation. The

website must have HTML hyperlinked documentation. Not hyperlinked PDFs

which I have to download in a zip file and then open with a special

PDF reader. HTML and URLs are king; not PDFs and UUIDs. While I value

typesetting, I value the linkability of the web much more. (I should

emphasize that the *content* of all PDFs I have read has been first

rate: it's all superbly written.)

My third bad experience was with the command-line tools. It took time

and effort to install them: why a jar and a zip? Why do I have to do

some Java-specific stuff to use it; shouldn't their Java

implementation be an implementation detail? It then took time to work

out how to run the programs; I didn't even know how *find out* how to

use them. TLA+ needs to put the command-line tools first: in the

programmer's world, command-line tools are how we interact with our

files. In an ideal world this is how I would interact with TLA+:

    > sudo apt-get install tla

    > man tla  # if this doesn't work, try `tla --help` or just `tla`

    > tla repl  # play around building a spec

    > nano clock.tla  # eventually put it in a file

    > tla syntax-check clock.tla

    > nano clock.tlamodel

    > tla model-check clock.tlamodel > results.txt

    > git add clock.tla clock.tlamodel

    > git commit

    > git push

    [CI server runs tla model-check and rejects my commit if it finds errors]

TLA+ is not so different from real-world programming languages: we

write (abstract) programs, then we compile/typecheck them, we run

them, we debug them. The workflow for TLA+ should be similar to, say,

Haskell. GHC has a compiler, a REPL, and a few command-line tools. It

does not have an isolated IDE; nor does it need one.  Even tools like

Coq or Isabelle, which have their own little IDEs for interactive

proof assistants, are usually used via other generic IDEs like

Emacs.

After reading that the IDE was the recommended way to do things, I

installed it. I had a few bad experiences with it. Outright bugs are

the most obvious but I'll omit those. I found aspects of the IDE

confusing. "Save" to open a file?  Okay. This "Spec Explorer" thing:

where does this state live, and why do I have to import things into

it?  My *filesystem* should be my spec explorer. It took me a while to

discover those foo.toolbox directories containing my models, encoded

in some semi-human-readable format. I want my models to be

hand-written, first-class citizens that I can put where I want, add to

version control, etc. I want my model-checking results in a standard

format that can be consumed by a CI server, like my unit test results.

In short I think it would be a lot better use of time for TLA+ to

maintain some syntax-highlighting definitions for common editors, and

some idiomatic command-line tools, compared to maintaining a full IDE.

My final significant bad experiences were with reading the "fancy

format" PDFs. Here's what I found myself doing when learning TLA+: (1)

read fancy notation in a paper; (2) attempt to write it out in TLA+

Toolbox; (3) realize I don't know the plaintext notation for

something; (4) find and open Specifying Systems PDF; (5) find the

section in the TOC about syntax; (6) tell my PDF reader to go to that

page number; (7) realize my PDF reader's idea of page numbers is

different to the internal page numbers in the book; (8) scroll around

until I find the definition of the plaintext syntax; (9) scroll around

until I find the symbol that I'm looking for, which might take a

while; (10) type it into TLA+ Toolbox; (11) forgotten what I was doing

in the first place. I'm being picky, maybe; but I found myself getting

seriously annoyed by that workflow when I just wanted to concentrate

on the domain problem. Here's what the workflow would look like if the

tutorials just used the plaintext format: (1) read plaintext notation

in a paper; (2) copy it into TLA+ Toolbox. Sometimes I've found the

fancy format actively confusing. What's the difference between a bold

extential quantifier and a non-bold one? To my programmer mindset,

it's a formatting quirk, not a semantic difference. TLA+ needs to put

plaintext first. In the programmer's world, plaintext is an undisputed

king. We write plaintext, we think plaintext, we store plaintext on

disk, we store plaintext in version control, we copy and paste

plaintext on email/IM, we pipe plaintext from one program to another,

etc etc etc. The power of plaintext means that the fancy math format

for TLA+ will always be in the margins. Programmers don't want to have

to mentally translate between fancy math notation and real-world LaTeX

notation; they want a single plaintext notation. Programmers don't

want to have to compile their work to a PDF in order to read it or

communicate about it. Programmers don't want TLA+ to produce beautiful

books; they want TLA+ to help them _think_. At best, the fancy format

is a minor helpful tool for academics, like similar tools that will

fancy-print Haskell code. At worst, the fancy format is a barrier to

entry which serves to give the (wrong) impression that TLA+ sits in a

dry Platonic mathematical universe that us real-world programmers and

programs don't have easy access to. (Note that I say "plaintext", not

"ASCII". Unicode and UTF-8 are very common nowadays, and having

symbols like "∈" in our programs is okay, if unconventional for

historical reasons.)

Anyway, the above criticism is meant with the greatest of respect. TLA

strikes me as a beautiful mathematical tool; the TLA+ tools I have

found to be less so. Personally, I'm enthusiastic enough to continuing

to rough it out, but I expect a lot of other people would have dropped

off along the way. Also, as someone who works day-to-day with Java and

the web, I might at some point be available to help out with the

project, if others agree with me on the direction it should take.

James

[fl]

TLA+ is not so different from real-world programming languages: we

write (abstract) programs, then we compile/typecheck them, we run

them, we debug them. The workflow for TLA+ should be similar to, say,

Haskell. GHC has a compiler, a REPL, and a few command-line tools. It

does not have an isolated IDE; nor does it need one.  Even tools like

Coq or Isabelle, which have their own little IDEs for interactive

proof assistants, are usually used via other generic IDEs like

Emacs.

 

The IDE is not exactly isolated. It is a specialization of Eclipse.

 

And somebody one day may want to make a package for tlaplus in emacs.

 

And my experience is that when you suggest somebody to learn emacs he looks at you as if

you wanted to come back to the stone age. I disagree with that obviously but is there a way of

convincing somebody in a democracy?

 

--

FL

 

[fl]

The IDE is not exactly isolated. It is a specialization of Eclipse.

 

I use the IDE under linux and I've never experienced your problem of file opening. I

don't know why. Maybe the way I use it or the version of Eclipse used for the Linux box. 

 

--

FL

[James Fisher]

On Thursday, November 20, 2014 4:37:26 PM UTC, fl wrote:

The IDE is not exactly isolated. It is a specialization of Eclipse.

But that's an implementation detail. To the user (i.e. me), the TLA+ Toolbox has absolutely nothing to do with Eclipse.

And my experience is that when you suggest somebody to learn emacs he looks at you as if

you wanted to come back to the stone age. I disagree with that obviously but is there a way of

convincing somebody in a democracy?

The last thing I want here is a flame war. I'm not advocating for or against any particular editor. I'm advocating UNIX-style, composable, documented, command-line programs as the flagship software, instead of an all-in-one, hard-to-maintain, uncomposable GUI.

I use the IDE under linux and I've never experienced your problem of file opening. I

don't know why. Maybe the way I use it or the version of Eclipse used for the Linux box. 

It is possibly specific to OS X. Markus Kuppe's changes fixed this issue for me.

[Leslie Lamport]

Hi James,

Thanks for taking the time to write up your feedback.  And thanks also
for your offer to try to help solve some of the problems you found.  I
hope we'll be able to take you up on your offer.

Before getting to specifics, I want to say that I believe your desire
for the command-line interface to come first represents a small
minority view in the general programming community.  Gerard Holzmann,
the inventor of the Spin model checker, told me a while ago that when
he put a very simple GUI on Spin, the number of users increased by an
order of magnitude.  I have had a number of comments that the Toolbox
does not provide the power they have come to expect from the IDEs they
use to write programs.  Although others have complained about the
absence of good documentation for the command line interfaces, no one
else has ever said that the Toolbox should not be the principle method
of using the tools.

However, I have not based my career on copying what other people do.
I have always tried to find what works best, regardless of what others
think should work best.  I'm not a fan of screen flash.  I started
programming before there were even command-line interfaces.  I use
whatever I find most convenient.  For example, for manipulating files
I will use either the Windows File Explorer GUI or a Cygwin
command-line shell depending on what I'm doing.

If you think running the TLC model checker from a command line could
be better than running it from the Toolbox, then you do not appreciate
all that you can do from the Toolbox--perhaps because you have just
been writing simple specs and have not yet had serious debugging of
specs to do, and perhaps because of poor documentation.  And only a
blind person could prefer running the prover from a command line
rather than from the Toolbox.  (We don't have the resources to try to
provide interfaces for disabled people.)

So, we are not going to spend resources trying to improve command-line
interfaces.  However, they should be documented better than they are.
That's one of the many things I haven't had time to do and am not
likely to find time in the near future.  But the information is easily
accessible, so it's not rocket science.

I'm willing to devote some energy to helping someone produce better
documentation for the Toolbox.  I would appreciate any help you can
provide.  I suggest that you start by reading the Toolbox's help pages
and tell me what can be done to improve them.  What I would like is to
have the Toolbox read the user's mind and, when she doesn't know what
to do next, present her with the appropriate help page.  I don't know
how to implement that.  Simply presenting the information in a single,
logically structured document doesn't seem to work very well.  25
years ago I found that LaTeX users weren't very good at reading the
manual, and people have gotten a lot less willing to read than they
were then.

You wanted HTML documentation.  There are two things that need to be
documented: TLA+ and the tools.  I considered alternatives to
LaTeX-produced pdf when I started writing the Hyperbook.  HTML would
have been ten times harder to use to produce something that was a
tenth as good.  As for the "pretty-printed" version versus the ASCII,
a TLA+ user at Intel wrote that one of the good things about TLA+ is
that if he doesn't understand what a TLA+ construct means, he can
look it up in a math book.  Math books don't write math in ASCII, they
use standard mathematical symbols.  I want TLA+ users to think in
terms of math, which means thinking in terms of its symbols.  You will
soon get to be bilingual, reading math and its TLA+ ASCII versions
equally well.  And if you learn TLA+ by reading the Hyperbook, you
will find that the ASCII versions are all sitting there for you to
just copy into the Toolbox.

By the way, I believe the Hyperbook has a page with a table of ASCII
<-> Math translations.  It's part of the few-page summary of TLA+ in
Specifying Systems, which is also available as a separate pdf file.

As to the zip file, the only way to write hypertext in pdf is with
hundreds of separate files.  You want those files on your own machine;
you don't want to have to be going out over the web for every pop-up.
I don't know any alternative to a zip file.

As to documenting the tools, there seem to be two issues: the
mechanics of the various bells and whistles that the Toolbox provides,
and the more subtle issues that involve understanding TLA+.  For the
latter, the Hyperbook seems to be the best medium.  The former is what
the help pages try to document, but don't seem to be doing a good job.

Leslie

[Çağatay Kavukçuoğlu]

I've recently started using TLA+ and the toolbox; my experiences have some commonality with James's. 

I have found the hyperbook to be a good tutorial to start learning. I find that the math syntax is in most cases easier to understand and more expressive than plain ASCII text could hope to be; the PDF format definitely has that as a positive. On the other hand, I soon came to miss the ability to bookmark and search as I'm used to on the web, and I found Acrobat Reader to be fairly user hostile software in terms of usability. I think that given the documentation toolchains available today (Jekyll/Sphinx for building the docs, MathJax for typesetting, MultiMarkdown for authoring, Dash/Zeal/Velocity for offline docsets) and the current state of browser technology, HTML is a lot more feasible today that it would have been ten years ago. If the sources for the hyperbook and the PlusCal manual are available publicly with a creative commons license the community can experiment with pulling the documentation into a new form.

As I spent more time with TLA and PlusCal, the fractured nature of the documentation became a bigger hassle for me. I'm essentially dividing my attention between the Specifying Systems book, the hyperbook and the PlusCal manual. They are written clearly and I enjoyed reading them, but each of these have topics that only one of them covers, and they also repeat a significant deal of information between each other. One of the things that I hope would come out of an effort to improve documentation is one authoritative set of documents that can serve as a tutorial, user's guide and manual. As things stand today, it's easy for a newcomer to feel frustrated at the effort it takes to simply find the relevant information on how some feature works. For example, the Specifying Systems book explains recursive functions, but the hyperbook clarifies that TLA+ 2 has recursive operators as well, and the PlusCal manual explains how recursion works in that language. This topic would be better exposed under a single heading covering all cases in the ideal documentation. Similarly, various TLA expressions are explained in the PlusCal manual and the hyperbook, but only Specifying Systems book has the formal semantics of what TLA expressions entail and other important details such as how exactly TLC values are compared to each other. 

I'm a lot more positive about the emphasis on providing the toolbox; the integrated environment is an overall plus and helps a lot during debugging. The one thing I intensely long for is a REPL; the lack of an environment that I can use to build models incrementally with immediate feedback, in a language such as TLA+ (which would lend itself so well to it) makes me sad. I'm aware of the "evaluate constant expression" feature in the toolbox, but that is a clunky substitute a long way off from the seamless experience of a REPL.

In the last few months I've spent with it, I've found TLA to be a surprisingly useful tool that changed how I write software; thanks for making it available and working on it persistently. My efforts to sell it to colleagues would definitely be helped by a better website and consistent, online documentation. 

CK. 

[Chris Newcombe]

  >>The one thing I intensely long for is a REPL; the lack of an environment that I can use to build models incrementally with immediate feedback, in a language such as TLA+ (which would lend itself so well to it) makes me sad. I'm aware of the "evaluate constant expression" feature in the toolbox, but that is a clunky substitute a long way off from the seamless experience of a REPL.

Yes, a REPL would be terrific.  Until someone builds one, the closest thing I know is the partial support for TLA+ in the ProB Logic Calculator [1] (which was inspired by Leslie's notion of a logic calculator [2]).

Unfortunately, when I just tried to use the online version of the calculator [1], I found that it is not working ("The server is temporarily unable to service your request due to maintenance downtime or capacity problems. Please try again later.") 
But IIRC, the calculator is included with the downloadable (offline version) of the ProB Animator tool [3]. 

Note that the support for TLA+ is partial because TLA+ is essentially untyped but ProB is typed. See [4] for consequent limitations.

cheers,

Chris

[1] http://www.stups.uni-duesseldorf.de/ProB/index.php5/ProB_Logic_Calculator
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html
[3] http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA
[4] http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA#Limitations_of_the_translation

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Chris Newcombe]

Hi James,

Welcome to the group.  I'm glad that the AWS paper was useful to you.

On this:

  >>(3) realize I don't know the plaintext notation for something;
  >>(4) find and open Specifying Systems PDF;

You might find it more convenient to use the very short cheat-sheet for TLA+ [1].

Page 6 of the cheat-sheet gives the ASCII versions of symbols.

On this:

    >>What's the difference between a bold extential quantifier and a non-bold one?

I can say with high confidence that you will never need the bold existential or universal quantifiers (temporal quantification). The model checker doesn't support them.  I've only ever them used once, in the highest levels of the Wildfire Challenge spec [2] (which BTW is a very interesting read).

There are only a handful of ASCII representations that you'll actually need in practice. There is also one rule of indentation of bulleted conjunctions/disjunctions that has occasionally tripped me up [3]. (Leslie has since documented that point in the hyperbook.)

If you use PlusCal there are a few points of syntax (in particular around fairness & termination) that are quite easy to forget.  But I'm sure I would remember them if I used PlusCal as often as I use programming languages.

    >>TLA+ needs to put plaintext first. In the programmer's world, plaintext is an undisputedking.

I'm a programmer too. In my case, I found the ASCII notation for TLA+ very unfamiliar (not having used LaTeX before learning TLA+), but easier to learn the numerous arbitrary quirks of various programming language.  E.g. Perl, C++, Erlang, Clojure, Haskell all have odd syntax in places (including escape sequences).

The biggest problem I encountered in learning and using TLA+ was to re-wire my brain to think mathematically (e.g. declaratively) about computation and properties.  That problem far exceed any transient hiccups with syntax or tools. But that re-wiring of my brain turned out to be one of the biggest benefits I've received from TLA+.

   >>TLA+ needs to put the command-line tools first: in the programmer's world, command-line tools are how we interact with our files.

Your opinion is valid of course (by definition).  But programmers are a varied bunch, with different perspectives.  I've helped perhaps 15 programmers learn TLA+ now, and they've all been sufficiently happy with the IDE that they haven't even asked about command line tools.  In particular, once you start using multiple models (clones with different constants and TLC configuration), and the 'Trace Explorer' feature to debug specs, you'll probably want to stick to using the IDE.  The only time I've needed the command-line tools is to run slave nodes for the distributed model checker.

   >>This "Spec Explorer" thing: where does this state live, and why do I have to import things into it?

Have you tried looking in the online help, built into the IDE?  It's fairly comprehensive, and very useful. 

regards,
Chris

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/summary.pdf   Note: the cheat-sheet does not cover extensions in v2 ('TLA+2') of the language, e.g. the LAMBDA keyword.
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/wildfire-challenge.html

[3] This:

B ==  \/ TRUE
      \/ TRUE
      => FALSE         (* means (TRUE \/ TRUE) => FALSE,   so B = FALSE *)

is very different to this

B ==  \/ TRUE
      \/ TRUE
           => FALSE    (* means TRUE \/ (TRUE => FALSE),   so B = TRUE *)

I would occasionally type the second, when I intended (the meaning of) the first.

Note that the following means the same as the second statement above, _not_ the first.

B ==  \/ TRUE
      \/ TRUE
       => FALSE       (* means TRUE \/ (TRUE => FALSE),   so B = TRUE *)

[Leslie Lamport]

   I found Adobe Reader to be fairly user hostile software in terms of
   usability. 

There are other pdf readers.  I have found Foxit to be pretty good and
appears to have fewer bugs than Adobe Reader, but I find it somewhat
clunkier.

   I think that ... HTML is a lot more feasible today that it would have
   been ten years ago. 

If anyone knows of a better way to display the Hyperbook than pdf that
is easily available on the three supported platforms and is likely to
still work in 20 years, please let me know about it.

 If the sources for the hyperbook and the PlusCal manual are available
   publicly with a creative commons license the community can experiment
   with pulling the documentation into a new form.

I will be happy to assist anyone who wants to improve the
documentation, including by making the sources of the existing
documents available to them.  However, one requirement is that it must
not make it less convenient for me to continue modifying the
documents--especially the Hyperbook.  Since I have been developing my
personal LaTeX environment for the past 30 years, this is a
non-trivial requirement.

   As I spent more time with TLA and PlusCal, the fractured nature of the
   documentation became a bigger hassle for me. 

It has been my intention to make the Hyperbook replace at least the
first part of Specifying Systems.  Some "fracturing" of the
documentation is inevitable, since few people will want to read things
like the chapters of Specifying Systems on the semantics of TLA+, so
it's not worth the effort of making it as user-friendly as I want the
Hyperbook to be.

   The one thing I intensely long for is a REPL;

I don't know what kind of REPL for TLA+ you (and Chris) would like.
Please describe explicit scenarios that you would like to have
supported.  Be as fanciful as you like.  The only constraint is that
the E(valuate) has to be performed by the TLC model checker, so forget
about anything that involves instantly reporting all errors in a spec
with 10^27 reachable states.

Leslie

[fl]

I will be happy to assist anyone who wants to improve the
documentation, including by making the sources of the existing
documents available to them.

 

If you change your way of documenting tlaplus may I suggest that you don't make a documentation

that requires that one connects online to read it. I appreciate to work offline.

 

And it is very boring to be compelled to download a whole site (with all that garbage of insignificant pictures,

broken links and so on)  or to pick up one page after the other when you want to retrieve the documentation.

 

In that sense pdf format meets my needs : it is comprehensive and can be downloaded easily.

 

--

FL

[Leslie Lamport]

   If you change your way of documenting tlaplus may I suggest that you

   don't make a documentation that requires that one connects online to
   read it.

The only documentation to which this seems to apply is the
documentation of TLAPS.  I intend eventually to replace that with
additional material in the Hyperbook.  I trust you realize that the
Toolbox documentation on the Web consists of a copy of its help pages,
put there because help pages aren't going to help someone solve the
problem of the Toolbox not starting.

Leslie

[Chris Newcombe]

  >>I don't know what kind of REPL for TLA+ you (and Chris) would like.

(Priority-wise, I'd rank this far below improving TLAPS and the Hyperbook. Other people may reasonably disagree of course.)

I often find myself using TLC as a superset of a logic calculator, to help write & debug non-trivial operators/expressions.  When doing this, I don't check actions or behaviors, but I do need to check many possible states (inputs).
My main use-cases are:

 a. 'Exhaustive' testing of operators over some small finite sets of values for each of the various operator parameters _and_ (ideally) model constants.  I typically test properties of operators, and often, the semantic equivalence of two different definitions of an operator.

 b. Examining concrete counter-examples, when the testing fails.

I will often do this iteratively, changing various definitions as I go.
An example is testing the various definitions of TransitiveClosure that we discussed several years ago (on the old tlaplus.net forum and in email -- that prompted Leslie to write the TransitiveClosure module, and the section in the hyperbook).

I think I would work this may more often if the iterations were faster & less work.

When I first started using the IDE, I used the 'Evaluate Constant Expression' feature to do the above.  The expression would often become a large LET statement with many local definitions that I would copy/paste between the spec file and the edit window. This method was tedious because the editing window and output windows are too small and too fiddly to control. (And sometimes the whole eclipse window will scroll, instead of the edit or output window.)  Also there is no easily recalled history of expressions, making it difficult to change focus between expressions. To change focus I would sometimes have many expressions in the edit window and comment-out all but the statement of current interest (unfortunately this increased the need for scrolling around), or I would copy/paste expressions between the spec file and edit window. Eventually I realized I should just edit the expressions in the spec file, define a single 'ToEvaluate' symbol for the one I wanted, and just put that symbol in the edit window. But that didn't solve the problems with the output window (e.g. complex output was hard to read due to lack of a pretty-printer for values).

I found a better solution when I learned that TLC checks all ASSUME predicates before generating any states. (This feature is documented somewhere but I missed it repeatedly. Leslie pointed it out to me when I mentioned the above issues with 'Evaluate Constant Expression'.)

So now I mostly use (many) ASSUME statements. In those statements, I often use the Assert(_,_) and PrintT(_) operators (from the TLC standard module), and I evaluate them using a model that is configured to have no 'behavior spec', so TLC only checks ASSUME statements (and evaluates an optional constant expression).

The main problems using ASSUME statements for this purpose are:

   1. Speed of iteration.  This is a combination of sub-problems:
        a. GUI : each iteration requires switching between the spec and the model checker view, and often clicking around to alter various constants, start the model checker, scroll output etc. This is tedious and can become a distraction.

        b. 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.  This is probably the biggest obstacle to a fluid REPL.  An obvious possible solution would be to wrap TLC in a long-lived server that accepts commands and returns responses, but the amount of development work to implement that will heavily depend on the internals of TLC (e.g. how many globals/singletons are in the code). I haven't looked.
 
        c. TLC checks all ASSUME statements in every model. This is exactly the right thing to do for the intended purpose of ASSUME. But when ASSUME statements are being abused to check work-in-progress expressions that may take tens of seconds to evaluate, I find myself frequently commenting and uncommenting ASSUMEs .  It might be easy to avoid this by defining a constant to control evaluation (e.g. ASSUME WorkInProgressTestingIsEnabled => ...expensive test predicate...) but I have not yet tried that.

  2. Relatively poor error reporting by TLC in some circumstances. e.g. If an ASSUME fails, sometimes the error is cryptic. I find myself adding PrintT and Assert statements to diagnose the cause.

     E.g. For a simple test of the form
             ASSUME A = B   (* where A and B might be complex values *)
     ... TLC may say that predicate is false, but does not help understand why:
             Assumption line 17, col 8 to line 17, col 12 of module X is false.
    
     So I find myself writing statements such as
             ASSUME Assert(A = B, <<"A = B", A, B>>)
     to show the actual values of interest:
             ... snip ...
             The first argument of Assert evaluated to FALSE; the second argument was:
             <<"A = B", FALSE, TRUE>>
     This still has problem #4, listed next...

  3. Lack of a pretty-printer for complex expressions, e.g. nested sequences, records, functions.  I keep meaning to write a tool (analogous to http://jsonprettyprint.com/ for JSON) so that I can at least copy/paste to get a nicely formatted version, but I haven't had the time.

  4. The inability to temporarily override (shadow) the values of a CONSTANT, in an expression (it causes 'multiply-defined symbol' errors in the parser). This is ordinarily the desired behavior of course, but it makes it harder to test operators that refer to constants. To do such testing, I find myself making operators independent of constants by adding parameters to the operators and passing in the desired value -- either the intended constant or a bound (quantified) variable when testing. This makes the spec slightly more complicated. So an optional (very explicit) mechanism to allow shadowing of constants might be beneficial. But this is the smallest of the 'problems', and is almost certainly not worth complicating the parser to address.

Again, these are relatively low priority from my perspective. They might make nice projects for members of the community. Sadly I don't currently have the time.

regards,
Chris

[fl]

> The only documentation to which this seems to apply is the

> documentation of TLAPS.

Yes that's true; it's just in case you want to change your mind about your documentation policy.
The current one meets my needs.

--
FL

[Leslie Lamport]

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

[Chris Newcombe]

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

[Markus Alexander Kuppe]

On 23.11.2014 23:42, Leslie Lamport wrote:
>> 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.

Hi,

for those interested, distributed TLC worker use a technique based on
OSGi's [1] bundle re-installing that makes it possible to reuse the same
VM for multiple TLC model checker invocations. The same technique could
be used here.

Markus

[1] http://www.osgi.org/javadoc/r4v43/core/org/osgi/framework/Bundle.html

[Michael Leuschel]

Hi,

I find this discussion very interesting and also relevant for other formal methods communities and tools.

We have also added a REPL to ProB some time ago, but it is far from complete (e.g., one can introduce local variables using let but one cannot construct new specifications inside the REPL yet).

As such, I am very interested in feature requests and usage scenarios as well.

On 23 Nov 2014, at 23:42, Leslie Lamport <tlapl...@gmail.com> wrote:

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.  

You can find one particular scenario using the current ProB REPL here:

     http://www.stups.uni-duesseldorf.de/ProB/index.php5/Sudoku_Solved_in_the_ProB_REPL

I find the REPL very useful for debugging models and also for developing certain parts of a model from scratch.

The REPL is also very useful to test the kernel of our tool (there is actually a “hidden” command to add the last expression/predicate as a unit test for ProB).

Finally, for teaching, I find the REPL very handy to explain the various B operators during lectures (but maybe the students are of a different opinion ;-)).

If there is interest from the TLA community, one could consider using this REPL as a starting point for a REPL for TLA.

Indeed, probcli can already load TLA specifications via SANY (see log below). However, beware of the following:

 - our translator from TLA to B has certain limitations (http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA).

 - one currently has to use B syntax in the REPL; this could be remedied with moderate effort by using SANY in place of our B parser.

 - the output is printed in B syntax; this would take a bit more effort to adapt for TLA (storing TLA type information in the abstract syntax tree and adapting the pretty-printer),

 - one could call TLC from within the REPL, we already do so for model checking (http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLC). For evaluation, there is the issue of JVM startup time, already discussed in previous messages of this thread.

Best regards,

Michael Leuschel

PS: Here the log showing how the current REPL can be used for a simple TLA specification:

$ rlwrap probcli clock.tla -init -repl

Parsing file /Users/leuschel/TLA/Full_Clock/clock.tla

Parsing file /var/folders/j4/cxrp94290tdg3mgpvg8yjfdc0000/T/Naturals.tla

Semantic processing of module Naturals

Semantic processing of module clock

B-Machine /Users/leuschel/TLA/Full_Clock/clock_tla.mch created.

/Users/leuschel/TLA/Full_Clock/clock.prob created.

ProB Interactive Expression and Predicate Evaluator 

Type ":help" for more information.

>>> (hours,minutes,seconds)

Expression Value = 

((0|->0)|->0)

>>> -animate 58

Executing probcli command: [cli_random_animate(58,true)]

ALL OPERATIONS COVERED

finished_random_animate(58,[runtime/20,total_runtime/20,walltime/20])

>>> (hours,minutes,seconds)

Expression Value = 

((0|->0)|->58)

>>> -animate 2

Executing probcli command: [cli_random_animate(2,true)]

finished_random_animate(2,[runtime/10,total_runtime/10,walltime/0])

>>> (hours,minutes,seconds)

Expression Value = 

((0|->1)|->0)

>>> card({h,m,s| h:0..23 & m:0..59 & s:0..59})

Expression Value = 

86400

>>> h:0..23 & m:0..59 & s: 0..59 & h*60*60+m*60+s = 1000

Existentially Quantified Predicate over h,m,s is TRUE

Solution: 

       h = 0 &

       m = 16 &

       s = 40

>>> h:0..23 & m:0..59 & s: 0..59 & h*60*60+m*60+s = 10000

Existentially Quantified Predicate over h,m,s is TRUE

Solution: 

       h = 2 &

       m = 46 &

       s = 40

>>> :stats

% Type: pred

% Eval Time: 0 ms (0 ms walltime)

$ more clock.tla

---------------------- MODULE clock ----------------------

EXTENDS Naturals

VARIABLES

  hours,

  minutes,

  seconds

Init  ==    hours \in (0 .. 23)

               /\ minutes \in (0 .. 59)

               /\ seconds \in (0 .. 59) 

Next  ==    hours' = (IF minutes # 59 THEN hours ELSE (hours + 1) % 24)

               /\ minutes' = (IF seconds # 59 THEN minutes ELSE (minutes + 1) % 60)

               /\ seconds' = (seconds + 1) % 60

Clock  ==  Init /\ [][Next]_{seconds}

--------------------------------------------------------------

THEOREM  Clock => []Init

==============================================================

[Markus Alexander Kuppe]

On 20.11.2014 00:07, James Fisher wrote:
> My third bad experience was with the command-line tools. It took time
> and effort to install them: why a jar and a zip? Why do I have to do
> some Java-specific stuff to use it; shouldn't their Java
> implementation be an implementation detail? It then took time to work
> out how to run the programs; I didn't even know how *find out* how to
> use them. TLA+ needs to put the command-line tools first: in the
> programmer's world, command-line tools are how we interact with our
> files. In an ideal world this is how I would interact with TLA+:
>
> > sudo apt-get install tla
> > man tla # if this doesn't work, try `tla --help` or just `tla`
> > tla repl # play around building a spec
> > nano clock.tla # eventually put it in a file
> > tla syntax-check clock.tla
> > nano clock.tlamodel
> > tla model-check clock.tlamodel > results.txt
> > git add clock.tla clock.tlamodel
> > git commit
> > git push
> [CI server runs tla model-check and rejects my commit if it finds
> errors]

I do have a similar setup based on Jenkins that I used for my
performance analysis of the tools.

However, I am not sure the regular TLA workflow benefits much from
continuous integration. Maybe Chris Newcombe can share how Amazon's
workflow looked like for large groups of people.

> I want my models to be
> hand-written, first-class citizens that I can put where I want, add to
> version control, etc. I want my model-checking results in a standard
> format that can be consumed by a CI server, like my unit test results.

A model is a first class citizen. The .toolbox folder and .launch files
just have meaning for the Toolbox itself. You only need the .tla and
.cfg files. E.g. see
https://github.com/lemmy/tlc-perf/tree/master/models for a SCM
controlled folder with a bunch of specs and even more models.

Markus

[Leslie Lamport]

Hi Chris,

You write that a REPL should:

 - Allow ... constants and variables to be declared.

 - Allow operators to be defined and re-defined...

 - Provide a command to display the definition of any symbol. 

A set of declarations and definitions is a specification.  I therefore
infer that a REPL would maintain a Current Specification that is
modified and viewed by command-line commands.

The first text editor I can remember using was called TECO. In those
days, video displays were too expensive for common use, so one
interacted with a computer using a teletype-style device with a
keyboard and a roll of paper.  TECO maintained a current cursor
position, and one edited a file by keyboard commands to move the
cursor and to insert or delete characters at the cursor position.  To
see the actual contents of the file, you executed a command to print
part of it--usually a few lines containing the cursor.  When CRT
displays became common in the 1970s, they were first used as "glass
teletypes", treating the screen as a virtual roll of paper.  People
soon switched to visual editors that made the screen a window on the
file that you edited visually--e.g., Emacs (which was first built on
top of TECO). 

Your REPL seems to be a specification editor based on the TECO model,
treating the screen as a glass teletype.  (Instead of viewing a few
lines around the cursor, the user displays an individual definition.)
However, unlike text files, specs have a logical structure.  So, what
happens if you try to add a syntactically incorrect definition?  One
possibility is to produce a syntactically incorrect spec, which you
then fix by actual TECO-style editing commands.  However, I presume
that you intend the definition command to fail, so the user would have
to issue a whole new command to add the definition.  Since you are
using a virtual paper roll rather than real paper, this is not hard to
do with copy/paste/edit starting from the incorrect command.

People who want a REPL interface apparently think it's a great step
forward to return to the 1960s.  I lived through the 60s and I don't
think they were that great (except for the music).  So, I will have no
part in implementing a REPL interface for TLA+.  If I want to edit a
Current Specification, I will do it by putting the specification in a
buffer and editing it with something like Emacs, not something like
TECO.  And TLA+ already provides a syntax for displaying a
specification in that buffer.

I couldn't tell if the Current Specification in your proposal is
actually what the Toolbox thinks is the current spec, so your REPL
command to modify a definition actually changes the .tla file.  I
suspect it isn't.  In that case, the Current Specification should have
its own buffer.  This allows you to play with potential changes to the
spec--or make changes just for debugging purposes--without affecting
the official spec.  There are any number of ways of doing this--for
example, with an easy to use repository.  With a REPL, if you want to
change a definition in the spec to a modified version that you've
since changed, you will have to search back in the scroll for the
command that created it.  With a repository, you could make lots of
checkpoints and go to the appropriate one.  Another alternative is to
create new models instead of new checkpoints.  As part of a model, the
Toolbox keeps the entire spec that was last checked by the model.  I
believe you can open that spec in a read-only editor, but I don't
remember how.  (I've never used it.)  But it should be easy to add
Toolbox commands to allow the user to edit that saved version and
rerun TLC on it.

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

That shouldn't be hard to add to the Toolbox, if clicking on a button
is too much work.  Since you can have more than one model executing at
a time, there might be some problem in determining which one gets
interrupted.

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

I don't know what that means.  A model requires you to "bind" CONSTANT
parameters and allows you to redefine defined operators.  Presumably you

have something else in mind.

   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.

Your recollection is probably correct.  I have to do that sometimes.
No pretty-printer can automatically display a complex value the way I
want to see it because how I want to see the value depends on what I'm
looking for.  So I might want the same value to de displayed in two
different ways.  Mark's algorithm is not very sophisticated, so it can
probably be improved.  But I doubt if it will be easy to make it very
much better.

   Using TLC currently requires using the mouse quite a lot, whereas
   using TLAPS can be done mostly from the keyboard.

There are many more things you can do with TLC than with TLAPS, so
doing everything with keyboard commands would be pretty complicated.
However, I believe that once a window is selected, any click of a
button on that window could be implemented as a keyboard command.  I
don't know how to attach keyboard commands to individual windows.
Anyone who knows how can easily do it; they just have to coordinate
with me.

Cheers,

Leslie

[Chris Newcombe]

Hi Leslie,

  >>Your REPL seems to be a specification editor based on the TECO model,
  >>treating the screen as a glass teletype.

It's more than that, because of
   - the ability to very easily evaluate expressions at any time, using the definitions you've built up so far.

   - the speed of iteration (including staying focused on the keyboard, rarely using the mouse).

I agree that from the outside it looks like it could be a step backwards. But I suspect that fans of REPLs would claim that the resulting experience is more than the sum of its parts.

As I said, I don't have a strong personal need for this, because I use ASSUME commands to evaluate expressions using definitions I've built up so far, and I've learned to live with the current speed of iteration. (The speed of iteration seems to be a bit better since I recently switched to using a laptop with an SSD and more ram.) An improved 'logic/expression calculator' would be very nice, but not at the expense of the other things I listed.

However, I do know some programmers who really like working in a REPL; they describe it as being more intense and immersive than the conventional edit/compile/debug cycle. A REPL may or may not produce better end-results for them (I have no idea), but it does involve a different style of interaction with the tools. As long as the style of interaction with the tools does not interfere with thinking mathematically then it seems like a matter of personal preference in user interface. I expect that we'll see a broader spectrum of personal preferences as TLA+ gains adoption among new groups of people.

I should mention that there are many forms of modern REPL.  E.g.
 http://gorilla-repl.org/

   "You can think of it like a pretty REPL that can plot graphs and draw tables, or you can think of it as an editor for rich documents that can contain interactive Clojure code, graphs, tables, notes, LaTeX formulae."

My own speculative personal preference for user-interface would be for something closer to Don Knuth's 'Literate Programming' system. I'd like to write a spec "in order of clearest explanation" (as Knuth says), primarily in prose like a technical paper, then refining the prose into formal definitions. I'd then like to have the spec automatically rearranged into the form necessary for the model-checker (basically macro-expansion). This reflects how I work now, but I'm currently lacking the automated tool or the ability to maintain both versions. I've mentioned this in several talks (e.g. [2]) but haven't had time to try writing or adapting a tool[1].

regards,
Chris

[1] http://www.literateprogramming.com/tools.html
[2] From slide 22 of http://tla2012.loria.fr/contributed/newcombe-slides.pdf
         Donald Knuth wrote

“Some of my major programs ... could not have

been written with any other methodology that I’ve

ever heard of. The complexity was simply too

daunting for my limited brain to handle; without

literate programming, the whole enterprise would

have flopped miserably.”

...

“Literate programming is what you need to rise

above the ordinary level of achievement"

--

[Çağatay Kavukçuoğlu]

On Friday, November 21, 2014 7:22:46 PM UTC-5, Leslie Lamport wrote:

I don't know what kind of REPL for TLA+ you (and Chris) would like.

Please describe explicit scenarios that you would like to have
supported.  Be as fanciful as you like.  The only constraint is that
the E(valuate) has to be performed by the TLC model checker, so forget
about anything that involves instantly reporting all errors in a spec
with 10^27 reachable states.

What I expect from the REPL is effortless and always-on evaluation of expressions. This can be in the form of a console-style interface that's typical of the REPL's out there, but I'm more fond of the notebook-style interfaces that Mathematica or more dynamic variants of this UI style, such as Light Table (http://lighttable.com), exemplify. 

For example, if I have three expressions on my notebook using various definitions from the specification this notebook is based on, I would expect their results to be updated without any explicit action by me when I change the specification. The notebook itself would have an editor-like UI, with expressions and the results of the their evaluation presented inline. I would want to use the REPL notebook in a two-column layout with the specification editor within the toolbox.

It should be possible to define and redefine operators, variables, constants and model values within the notebook. If a symbol is redefined, the new definition's effects should be immediately visible on all usages of that symbol transitively.

I expect to have three major ways to launch the REPL notebook:

• Based on a specification: This is perhaps the simplest way; right-clicking on a specification (or using a menu item) should open a REPL notebook where all definitions and declarations made in the specification are in scope. This is where I expect to spend most of my time, using it as a sandbox and building up parts of a specification incrementally. This alternative also fits the "logic calculator" use case, assuming the specification can be optional, with an empty one (suitably importing a default set of useful standard modules) substituted at runtime in a notebook that's not based on an existing specification.
• Based on a state in the error trace: Right-clicking on a state in the error trace should provide an UI action to create a REPL notebook with the initial state set to and all definitions/declarations in scope at that point. I should be able to write expressions in the notebook and see their result as they would be evaluated in those exact conditions. It would be nice if this included ENABLED expressions too. I suspect more interesting ways to push this style of interaction are possible if one were to consider interactively guiding the model checker along a particular behavior, but this encroaches on debugger territory (which is interesting for a runtime such as TLC).
• Based on a model of the spec: Right clicking on a model should give me the ability to create a REPL notebook based on the initial state and all other overrides/settings/declarations in that model.

In all of these alternatives, it should be possible to create a model out of a notebook, with all the redefinitions, constants and other details outside of the specification the notebook is based on being reproduced in the new model. Among making it simple to move parts between notebooks and models, this allows a nice workflow during debugging; I could start a notebook from a particular error state, make changes, create a new model out of the notebook that reproduced my changes (including the variable state as the new initial state), and see their effect. Of course, I would only observe the effect on the small subset of the state space as pruned by the given initial state, which I think is fine in order to check the effects of a change on a specific set of behaviors. This sort of incremental checking is too cumbersome to use today.

There are of course a lot more details to figure out about the user interaction, but I think what I describe above would be a significant factor to ease the learning curve of TLA; my main motivation is to shorten the feedback loop between making a change and seeing its effects, which makes the interaction between my thinking and the reality as shown by TLA/TLC more frictionless, and that is a boost to how fast I can learn.

[Leslie Lamport]

Hi Chris,

You wrote (approximately):

  >>Your REPL seems to be a specification editor based on the TECO model,
  >>treating the screen as a glass teletype.
   It's more than that, because of

   (1) the ability to very easily evaluate expressions at any time, using

       the definitions you've built up so far.

   (2) the speed of iteration (including staying focused on the keyboard,
       rarely using the mouse).

This REPL business is a time-wasting distraction.  Anyone who would
rather write a specification (or a program) in TECO rather than in
Emacs is so many standard deviations outside of normal that I'm not
concerned with his or her preferences.  Emacs is not a REPL, but when
I use it I rarely use the mouse.  I'm not focused on the keyboard; I'm
focused on the document I'm writing--something that would be hard to
do if I couldn't see it.  (I've used a REPL theorem prover.  It was a
nightmare because I was creating a current state with my typing, but
there was no easy way to see that state because all I could do was
type commands that would show me little pieces of it--like individual
definitions.)

So, whatever specification a user creates will be by editing the .tla
file using a window on the file, as in Emacs.  So, lets consider (1).
After setting up a suitable model, when editing in the Toolbox, at any
time with two mouse clicks you can go to the Evaluate Constant
Expression part of a model, type an expression, run it (one more mouse
click), and read its value.  This is not what I'd call difficult.  As
for (2), iteration consists of going back to where I was in the
spec--1 mouse click.  The speed of iteration is a problem because the
only way to evaluate an expression is by running TLC, which requires
starting a new JVM.  No interface change is going to eliminate that
problem.  Fixing it requires a significant rewrite of TLC, and perhaps
of SANY if you want to avoid reparsing the entire spec--or use of
another tool.

So, all a REPL buys you is eliminating three mouse clicks with a
little typing.  Even I could probably figure out how to replace those
mouse clicks with keystrokes--if someone can specify precisely what
those keystrokes should do.  (For example, what if there are multiple
models open?) 

So far, I don't think that the current discussion has revealed any
gaps in the functionality that the Toolbox provides.  It has pointed
out two problems:

   1. The functionality is not well document.
   2. It should be possible to use keystrokes instead of some
      mouse clicks.
   3. Evaluation with TLC takes too long.

I'm open to precise, well thought-out suggestions for improving 1 and
2.  It would be great if someone would volunteer to solve 3, now that
Markus has suggested how it might be done.

Leslie

[Leslie Lamport]

Dear Çagatay,

Thanks for taking the time to write down your ideas.  What I will do
now is show you how to do what I think you want in the current
Toolbox.  It won't be nearly as convenient as you want, but I think it
will show that we don't need any fundamental change to the logical
structure of the Toolbox.  If I'm right, then you can get what you
want by improving the Toolbox interface.

First of all, your proposal is based on a misconception of what is
required to evaluate an expression.  In general, evaluating an
expression requires a model to specify the values of declared
constants and a pair of states to specify the values of primed and
unprimed declared variables.  Constant expressions can be evaluated on
a model.  Expressions with constants and unprimed variables can be
evaluated on a state in a model.  (The state may contain model
values.)  You cannot evaluate anything on "the initial state" of a
specification because a specification can permit many initial states
(often infinitely many).  It follows from this that your notebook must
exist within a model of a specification.

I believe you have a single specification--the one you're writing--and
you want to be able to open multiple notebooks on it.  Let's call that
single specification S. Make each notebook a separate specification.
The root module EXTENDS S and contains any definitions and
declarations you want to add.  The interface you described has a
single model for this notebook specification, although you can have
multiple models.  The notebook's changes to the definitions of S are
made in the model (see the Advanced Model page). 

Put the constant expressions you want evaluated in the notebook as the
elements of a tuple in the model's Evaluate Constant Expression
section.  Arbitrary expressions (including primed expressions) can be
evaluated on error traces in the Error-Trace Exploration section of
the TLC Errors window.  (You need to have the error window to enter
those expressions, but once entered they appear whenever the error
window is opened.)

I don't claim that this is a very convenient way to do what you want
to do.  However, if it does what you want, then I believe it will

require only simple changes to make it convenient enough.  For example:

- Instead of making a notebook a new specification, perhaps
  it could be the copy of the spec saved with a model, as I
  suggested in a response to Chris.

- The method of entering and displaying the values of
  constant expressions and non-constant expressions could be
  made more consistent--e.g., multiple constant expressions
  enabled by check boxes.

- Some mouse clicking should be replaced by keystrokes.

As I've indicated before, instant evaluation won't be possible without
significant changes to TLC. You'll probably have to click or type a
command to re-evaluate expressions when the spec changes, although
it's possible to do it when you save changes to the spec.  Moreover,
if evaluation of one expression fails with an error, then the
evaluation of everything will probably fail.

However, before worrying about convenience, you should try this method
of implementing what I think you want to do.  The design of the
Toolbox was based on 10 years of experience using TLA+ and TLC.
Using the Toolbox this way will let you see if you really want
to do what you now think you do.  And let us know what you find out.

Leslie

[Çağatay Kavukçuoğlu]

On Monday, November 24, 2014 10:23:46 PM UTC-5, Leslie Lamport wrote:

Dear Çagatay,

Thanks for taking the time to write down your ideas.  What I will do
now is show you how to do what I think you want in the current
Toolbox.  It won't be nearly as convenient as you want, but I think it
will show that we don't need any fundamental change to the logical
structure of the Toolbox.  If I'm right, then you can get what you
want by improving the Toolbox interface.

Thanks for the explanation of a useful workflow. My current way of working is not far from what you outline here; I'm relieved that I haven't missed anything glaringly obvious up to now. I know that I fibbed some terminology in my description; your explanation is accurate in its details. 

One thing that I should emphasize is that there's a difference between how a feature behaves as far as the user is concerned and how its implementation works. Technically, it is true that there must always be a model for TLC to evaluate anything, but you can easily make the argument that the implementation of a notebook would use a default (empty) model and a hidden specification extending the original, suitably and transparently maintained as necessary (as you and others have noted, this is similar to how the toolbox works today). This can be an implementation detail; the toolbox is free to provide an option to create "a notebook based on a specification" while making sure that all the technical needs for that notebook to work are satisfied under the covers. I tried to focus on how things would work from the perspective of a user, not from the perspective of the implementor of those features.

Arbitrary expressions (including primed expressions) can be
evaluated on error traces in the Error-Trace Exploration section of
the TLC Errors window.

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. This requires me to write expressions that can evaluate successfully at every point of the trace, which makes them more unwieldy. For example, I could just refer to a particular element in a sequence at a given state with "log[1]" which I can't do in the current way expressions are evaluated. Maybe the useful thing for the toolbox to do here is to politely keep evaluating expressions that can be evaluated and simply display an inline error for expressions that fail, like a lot of other debuggers do. From what you say about how TLC fails during expression evaluation, I suspect this is currently harder to implement that it should be.

However, before worrying about convenience, you should try this method
of implementing what I think you want to do.  The design of the
Toolbox was based on 10 years of experience using TLA+ and TLC. 
Using the Toolbox this way will let you see if you really want
to do what you now think you do.

I'm under no illusions that what I describe would be seen unanimously as a better way of working than what the creators of the TLA, TLC and the toolbox have generously done up to now. These are the wishes and grumbles of a busy engineer after a few months of working and mostly succeeding to do something useful with TLA. I like tools that make short work of seeing the results of a change, even when it is true that most of the time we spend goes toward thinking about what to change. For a lot of people, it is the closed loop of making a small change and seeing a reward at the end that most helps when they are learning something new.

I think that as you get more experience, the need to illuminate the effects of the potential small steps ahead of you diminishes, and the value expert users perceive from tools that provide immediate feedback drop accordingly. Newcomers that are going through a steep learning curve have a different utility function for some of these features. I hope you continue to hear them when they speak up.

[Leslie Lamport]

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