Hi Leslie,
- The class
tlatools/src/pcal/TLAtoPCalMapping.java
I have begun to read the code.
First of all, I had never noticed this feature in the menu. We should always read the code!
Maybe a ALT-F10 for a to-and-fro movement would be handy.
About the comments. Obviously those are some notes for yourself and they are sufficient for this purpose.
But if you want to help more the future reader, I advise you to add the paragrah about what is intended in
the "mapping" variable at the beginning of the source. Perhaps using the example that you give in the TLA+ code
for debugging with additional comments.
Otherwise it is not yet clear for me. But obviously the TLA+ code can be played in isolation and we
can get that way a dynamic view of the algorithm. I hope grasping everything then.
A general idea about specifications: pictures and screen capture always help. Wikis are perhaps not the
only media for specifications but it is a good one anyway.
As a rule I think that there is no ideal solution for specifications -- if by that word we mean the process of
understanding a piece of code. Several ways must be used: manuals,
pictures, comments, contracts, pseudo-code or TLA+ specification. And also tools: wiki, smart editors,
TLC and so on.
--
FL