Re: [tlaplus] Some feedback from a new user

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello Alok,

thanks for your feedback! Leslie already answered the main points, I'll just add two bits specific to MacOS X since that's also my main platform. 

I've mainly seen the spinning beachball when Eclipse is performing a garbage collection, and I've been able to drastically reduce the number of occasions when this happens by increasing the Java heap size: add something like -Xmx2000m to the options in toolbox.app/Contents/MacOS/toolbox.ini. 

The use of the "wrong" file selector dialog (the "Save" dialog instead of "Open") is indeed a little annoying. I'm told this is so because in the Mac version of Eclipse it is the only one that allows you to type in a new file name in case you want to create a new module. Your suggestion to have two different menu items may be a good idea -- but apparently it's less of an issue on other platforms. As you say, one gets used to this kind of little annoyances over time and doesn't really notice any more. 

Best regards 
Stephan

--
Stephan Merz

> On 17 Aug 2015, at 03:09, Alok Menghrajani <al...@xxxxxxxxxxxx> wrote:
> 
> 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!
> 
> -- 
> 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.