Re: [tlaplus] Re: TLA+ Toolbox 1.5.5 release - please update

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

On 08.01.2018 22:33, Andrew Helwer wrote:
> After update, when running the model checker I get a modal dialog box
> pop up saying "TLC run for Model_1 has encountered a problem. An
> internal error occurred during: TLC run for Model_1" with detail:
>
> An internal error occurred during: "TLC run for Model_1".
> tlc2.tool.fp.OffHeapDiskFPSet.isSupported()Z
>
> I've attached all relevant files. Toolbox version:
>
> This is Version 1.5.5 of 05 January 2018 and includes:
>   - SANY Version 2.1 of 23 July 2017
>   - TLC Version 2.11 of 05 January 2018
>   - PlusCal Version 1.8 of 07 December 2015
>   - TLATeX Version 1.0 of 20 September 2017
>
> I'm on Windows 10 with the following Java version:
>
> java version "1.8.0_151"
> Java(TM) SE Runtime Environment (build 1.8.0_151-b12)
> Java HotSpot(TM) 64-Bit Server VM (build 25.151-b12, mixed mode)

Hi,

we track this issue [1] over at Github.

(Everybody, feel free to send me comments via email if you don't have
and want a Github account.)

Thanks

Markus

[1] https://github.com/tlaplus/tlaplus/issues/133