TLA+工具箱意外异常

Question

我正在学习TLA+，并运行讲座示例代码

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

但是我遇到了意想不到的异常错误，比如

试图加载自定义FPSet类失败: tlc2.tool.fp.OffHeapDiskFPSet TLC抛出了一个意外异常。这可能是由规范或模型中的错误引起的。请参阅用户输出或TLC控制台，以了解发生了什么。例外是java.util.concurrent.ExecutionException : java.lang.NullPointerException

和用户输出：

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

有人知道怎么解决这个问题吗？

最新情况：

​

TLA+工具箱版本：

 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

您的规范文件是否以模块行开始？这就是：

--模块MySpec

如果文件是MySpec.tla。

这样，我就可以在<>工具箱1.6.1版和tla2tools.jar (命令行)的TLC 2.14中使用TLC执行模型检查(pc= "done")。注:因为口吃而失败。