1

我正在学习 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

有谁知道如何解决这一问题？

更新： TLC 选项

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
4

1 回答 1

0

您的规范文件是否以模块行开头？那是：

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

如果文件是 MySpec.tla。

有了这个，我可以在 TLA+ 工具箱 1.6.1 版和 tla2tools.jar（命令行）中使用 TLC 2.14 中的 TLC 执行模型检查 <>(pc = "done")。Nb：由于口吃而失败。

于 2020-04-16T21:25:06.500 回答