Hi Alok,
Thanks for the comments. Here are some quick replies to your points,
referenced by your item numbers.
1, 2. These are coding issues that I know nothing about. It would be
useful to know if anyone else has these problems.
3. What PlusCal documentation are you talking about? It sounds like
you're not using the HyperBook. All my documentation effort has been
going into the HyperBook, not things like the PlusCal manual.
Operators like # come from TLA+, which is the _expression_ language of
PlusCal. TLA+ is for writing mathematics, and if one designs a
language for writing mathematical expressions, C is among the worst
places to look for inspiration.
I don't know what you mean by PlusCal sometimes requiring ";" after
closing braces. Unlike in C, ";" is a separator, not a closing
symbol.
5. I think that what you mean is that the translator often does not
detect syntax errors in expressions--errors that are caught by SANY
when parsing the translation. Due to errors made long ago, it isn't
possible to use SANY to parse the expressions in a PlusCal algorithm.
It would be nice to have a parser for TLA+ expressions written in Java
that could do this and be used for some other things as well. Anyone
interested in writing one can contact me. Meanwhile, the PlusCal
translator uses a simple algorithm that will detect the end of a
syntactically correct TLA+ _expression_, but might do strange things
with incorrect expressions.
6. I know about the problem that, after the translator finds an
error, it sometimes requires translating twice to get a correct
translation. It's hard to reproduce the problem, and since it's just
a nuisance I've never been inspired to take the time to try debugging
it. I haven't seen alternating error messages, which is probably a
symptom of the same bug. Perhaps your example will make it easier to
find and correct the error.
7. I believe that Eclipse provides a file chooser with a "Save"
button, but that getting one with an "Open" button requires
implementing a chooser from scratch. Perhaps I'm wrong and someone
can figure out how to do it easily.
Cheers,
Leslie
On Sunday, August 16, 2015 at 6:09:46 PM UTC-7, Alok Menghrajani 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(<<3, 7,
"a">>)"/>
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!