Re: Some user feedback

[Chris Newcombe <chris.n...@xxxxxxxxx>]

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


On Friday, November 21, 2014 4:22:46 PM UTC-8, Leslie Lamport wrote:

   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