Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox

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

On 24.11.2015 17:11, Jaak Ristioja wrote:
> Sometimes when I run the PlusCal translator in the Toolbox, a progress
> information window quickly flashes, and I'm back to the editor with
> nothing inbetween the \* BEGIN/END TRANSLATION lines. No error is displayed.
> 
> This seems to be specific to some .tla files and not others. Is my
> 800-line PlusCal source too long?
> 
> How do I debug this?

Hi Jaak,

is there anything related in the .log file in the workspace/.metadata/
directory?

I'm not aware of a spec length restriction.

Cheers
Markus