TLA+ | The way to specify

First of all, thanks for this! It looks great.

I get a Null Pointer exception every time I try to run TLC on any model (i.e., click the Green run model button). I'm not sure what all information you need, but I'm on a Mac and this is the toolbox version:

This is Version 1.3.1 of 5 April 2011 and includes:
- SANY Version 2.1 of 10 February 2011
- TLC Version 2.03 of 26 May 2010
- PlusCal Version 1.5 of 19 March 2011
- TLATeX Version .9 of 19 September 2007

and this is my machine and Java versions:

$ uname -a
Darwin Michael-OConnors-MacBook-Pro.local 10.8.0 Darwin Kernel Version 10.8.0: Tue Jun 7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386 i386
$ java -version
java version "1.6.0_26"
Java(TM) SE Runtime Environment (build 1.6.0_26-b03-384-10M3425)
Java HotSpot(TM) 64-Bit Server VM (build 20.1-b02-384, mixed mode)

Thanks!

Hi mkoconnor,

what does the actual stack trace look like? Can you post it here?

Since you are on Mac, you might be hit by bug #111 (https://bugzilla.tlaplus.net/show_bug.cgi?id=111) which is going to be fixed in the next Toolbox release.

Markus