Some feedback from a new user

[Alok Menghrajani <al...@xxxxxxxxxxxx>]

Hello,

I am a relatively new to this community. I was able to successfully
model (using PlusCal) some simple algorithms (things like leader
election in a ring) and last week I was also able to model a real
world algorithm I am working on.

First and foremost, I would like to thank everyone who has contributed
to this project. I feel it's the first time that formal methods are
available in a form which developers who don't have a strong
mathematical background can use. As more engineers adopt formal
methods, the quality of software across the board will improve.


I have some feedback about my experience so far. I am using the
ToolBox (version 1.51) on Mac OS X. I hope my feedback is useful. As
people get used to a given piece of software, they stop noticing some
of the pain points.

1. About 3-4 times per day, I end up with an unresponsive ToolBox
(cursor is a spinning wheel for a long time or forever). I usually
kill the ToolBox and launch it again. I feel this mostly happens when
I'm editing the source and the model is open in another tab. My work
around is to close the model tab when I'm not using it. Is this a
known issue or something other people run into?

In one instance, the ToolBox was completely failing to load. I
debugged the issue to the following line in the .launch file:
<stringAttribute key="modelExpressionEval" value="Tail(&lt;&lt;3, 7,
&quot;a&quot;&gt;&gt;)"/>

which I replaced with:
<stringAttribute key="modelExpressionEval" value=""/>

2. After unziping the ToolBox
(https://tlaplus.codeplex.com/releases/view/614836), there is a unix
executable called "toolbox" and an application "toolbox.app". Trying
to run the executable results in the following error: "The Toolbox
executable launcher was unable to locate its companion shared
library.". It still unclear what this binary is supposed to do but it
could perhaps be renamed to something else or moved inside one of the
folders?

3. I find PlusCal and the documentation could be more friendly.

For example, the math notation makes it hard to copy-paste examples or
to search (Preview, the default pdf reader for OSX, doesn't handle
searching some of the math symbols). Perhaps it would be possible to
host a version of the documentation which contains only ascii (or
contains both versions of each snippet of code)?

PlusCal deviates from standard C operators, e.g. # vs !=. The language
also requires ; after closing braces in some cases. I understand the
reason for these choices, I think it's a little unfortunate. PlusCal
lowers the bar to get started with TLA+. Things could still be made
easier.

On the other hand, having some learning curve does weed out people.
It's maybe not a bad idea and certainly not the end of the world.

5. In some cases, error messages point to the generated TLA+ code
instead of the PlusCal source. It's not a big deal, but takes some
getting used to.

Simple example:

    ----------------------------- MODULE alok_test -----------------------------

    EXTENDS Integers, TLC

    (* --algorithm alok_test {
      variables a = 1;
      {
          print <<"hello", a==1>>;
      }
    } *)

    \* BEGIN TRANSLATION
    \* END TRANSLATION

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

Results in a parse error at line 22. The error message points to the
generated code.

In a similar way, an invalid invariant (e.g. "a==1" instead of "a=1")
leads to a parse error which isn't always very clear:
Was expecting "Expression or Instance"
Encountered "Beginning of definition" in Invariants at line 1

6. The translator sometimes alternates between two error messages. You
can see this in action by translating the following code multiple
times.

    ----------------------------- MODULE alok_test -----------------------------

    EXTENDS Integers, TLC

    (* --algorithm alok_test {
      {
        print "hello"
        print "world"
      }
    } *)

    \* BEGIN TRANSLATION
    \* END TRANSLATION

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

Will result in either:
Missing `;' before line 8, column 11

Or:
Expected "begin" but found "alok_test" line 5, column 20

I have ran into cases where the code is correct but the translator
incorrectly complains about an error. My current work around is to
always translate twice.

7. The flow to open an existing spec could be improved: the file
browser shows the .tla files as grayed out, so it's not immediately
clear if a .tla file or a .toolbox folder needs to be selected. The
action button reads "Save" instead of "Open". Perhaps File->Open
Spec...->Add New Spec.. could be replaced with two actions: "Import
existing spec..." and "Create new spec...".

Thanks,
Alok

P.S. If anyone in SF/bay area is interested to talk about TLA let me
know, beer/<your favorite drink> is on me!