pcal.trans error not shown in IDE

[Yan Li]

Hi,

I’ve seen a mysterious problem where translating +Cal in IDE stopped working. After pressing Ctrl-T, a dialog showed up but swiftly disappeared, leaving no error message (and of course no TLA+ code produced). I’ve managed to track this problem down by running pcal.trans on the command line. It was caused by a missing procedure name as shown below.

> java -cp c:\tools\TLAToolbox-1.5.1-win32.win32.x86_64\toolbox\plugins\org.lamport.tlatools_1.0.0.201506011130 pcal.trans ObjBackend.tla
pcal.trans Version 1.8 of 2 Apr 2013
Parsing completed.
Warning: symbols were renamed.

Unrecoverable error:
-- Could not find procedure name `BackgroundProcessingThread' in method FixMultiprocess.

Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: -1
at pcal.PcalFixIDs.FixMultiprocess(PcalFixIDs.java:194)
at pcal.PcalFixIDs.FixSym(PcalFixIDs.java:41)
at pcal.PcalFixIDs.Fix(PcalFixIDs.java:31)
at pcal.PCalTLAGenerator.removeNameConflicts(PCalTLAGenerator.java:55)
at pcal.trans.runMe(trans.java:710)
at pcal.trans.main(trans.java:260)

The error was caused by a typo in the procedure name. The problem is that this error message from pcal.trans is not parsed and shown correctly in the IDE, which makes debugging this kind of error very hard.

Not sure if this is a known problem. I think it’s fairly easy to reproduce. If you need a minimal working sample, let me know.

—
Elliot

[Leslie Lamport]

Hi Elliot,

Thanks for reporting the bug.  I fixed it in the code available on the CodePlex site.  The fix will appear in the next release.

Leslie

[Yan Li]

Awesome. Thanks, Leslie! Can’t wait to test it.

—

Elliot