Re: [tlaplus] confusing crash when trying to use tla tool box on mac (most recent version 1.5.1)

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 01.10.2015 08:58, Stephan Merz wrote:
> a line starting with "===" is interpreted as the end of the module, so the TLA+ parser sees an empty module. That's why the Toolbox positions the cursor between the header line and that bottom line and inserts the "modification history" below it. (You may insert lines "------" if you want to have visual delimiters in your specification.)
> 
> I presume that you just tried running TLC by clicking on the green triangle without worrying about why the Toolbox told you that there was no behavior specification?
> 
> Indeed, TLC could fail more gracefully than by throwing a NullPointerException ...
> 
> If you remove the offending line, I believe that everything will work fine.

Hi Carter,

thanks for reporting. The next TLC release won't throw an NPE anymore.

Cheers
Markus