TLA+ Toolbox unexpected exception

Question

I'm studying TLA+, and am running the lecture example code

EXTENDS Integers
VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)

Pick == /\ pc = "start"
        /\ i' \in 0..1000
        /\ pc' = "middle"

Add1 == /\ pc = "middle"
        /\ i' = i + 1
        /\ pc' = "done"

Next == Pick \/ Add1

but I'm running into unexpected exception errors like

unsuccessfully trying to load custom FPSet class: tlc2.tool.fp.OffHeapDiskFPSet TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.util.concurrent.ExecutionException : java.lang.NullPointerException

And User Output:

java.lang.reflect.InvocationTargetException
    at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
    at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(Unknown Source)
    at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(Unknown Source)
    at java.base/java.lang.reflect.Constructor.newInstance(Unknown Source)
    at tlc2.tool.fp.FPSetFactory.loadImplementation(FPSetFactory.java:206)
    at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:109)
    at tlc2.tool.fp.MultiFPSet.getNestedFPSets(MultiFPSet.java:68)
    at tlc2.tool.fp.MultiFPSet.<init>(MultiFPSet.java:61)
    at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:105)
    at tlc2.tool.fp.FPSetFactory$1.call(FPSetFactory.java:136)
    at tlc2.tool.fp.FPSetFactory$1.call(FPSetFactory.java:1)
    at java.base/java.util.concurrent.FutureTask.run(Unknown Source)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(Unknown Source)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(Unknown Source)
    at java.base/java.lang.Thread.run(Unknown Source)
Caused by: java.lang.OutOfMemoryError
    at java.base/jdk.internal.misc.Unsafe.allocateMemory(Unknown Source)
    at jdk.unsupported/sun.misc.Unsafe.allocateMemory(Unknown Source)
    at tlc2.tool.fp.LongArray.<init>(LongArray.java:79)
    at tlc2.tool.fp.OffHeapDiskFPSet.<init>(OffHeapDiskFPSet.java:138)
java.lang.reflect.InvocationTargetException
    at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
    at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(Unknown Source)
    at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(Unknown Source)
    at java.base/java.lang.reflect.Constructor.newInstance(Unknown Source)
    at tlc2.tool.fp.FPSetFactory.loadImplementation(FPSetFactory.java:206)
    at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:109)
    at tlc2.tool.fp.MultiFPSet.getNestedFPSets(MultiFPSet.java:68)
    at tlc2.tool.fp.MultiFPSet.<init>(MultiFPSet.java:61)
    at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:105)
    at tlc2.tool.fp.FPSetFactory$1.call(FPSetFactory.java:136)
    at tlc2.tool.fp.FPSetFactory$1.call(FPSetFactory.java:1)
    at java.base/java.util.concurrent.FutureTask.run(Unknown Source)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(Unknown Source)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(Unknown Source)
    at java.base/java.lang.Thread.run(Unknown Source)
Caused by: java.lang.OutOfMemoryError
    at java.base/jdk.internal.misc.Unsafe.allocateMemory(Unknown Source)
    at jdk.unsupported/sun.misc.Unsafe.allocateMemory(Unknown Source)
    at tlc2.tool.fp.LongArray.<init>(LongArray.java:79)
    at tlc2.tool.fp.OffHeapDiskFPSet.<init>(OffHeapDiskFPSet.java:138)
    ... 15 more

Does anyone know how to fix this?

update:

TLA+ toolbox version:

 This is Version 1.6.0 of 10 July 2019 and includes:
  - SANY Version 2.1 of 23 July 2017
  - TLC Version 2.14 of 10 July 2019
  - PlusCal Version 1.9 of 10 July 2019
  - TLATeX Version 1.0 of 20 September 2017

Answer 1

does your specification file begins with a module line? That is:

------------------------------- MODULE MySpec -------------------------------

if the file is MySpec.tla.

With this I could perform model-checking <>(pc = "done") using TLC both in the TLA+ toolbox version 1.6.1 and with TLC 2.14 from tla2tools.jar (command line). Nb: it fails due to stuttering.