问题标签 [tla+]

我必须在 TLC 中使用 TLA+ 检查变量值。例如

Res_Word == {"_","N"}

变量 my_variable = "Some_valueONE"

检查 == my_variable \in Res_Word

* 表示检查变量是否包含集合中所需的某些特定值。

我试图在 TLA+ 中重现 Herlihy 的“多处理器编程艺术”中的死锁。在下面的代码中，当一个线程想要获取锁时，它会将自己标记为牺牲品，并且仅当另一个线程成为牺牲品时才继续。如果另一个线程永远不会出现，这里就会出现死锁。

TLA+ 规范如下：

TLA 规范在 Thread = {t1, t2} 中运行良好，其中 t1 和 t2 是模型值。

如何让TLA上报死锁？

我由 PlusCalc 编写的 TLA+ 规范编译为 TLA+ 成功，但解析失败：

规格：https ://justpaste.it/39pru

PlusCalc 中的错误位置在哪里？

谢谢！

我试图在 TLA+ 中指定一组存储单元，每个存储单元包含 256 个 32 位整数。我想指定在初始化时所有内存都清零。我直觉正确的方法类似于嵌套的 forall 语句，但我不知道如何在 TLA+ 中表达它。

我正在使用 VS Code 和 vscode-tlaplus 插件而不是 TLA+ Toolbox 来学习 TLA+。现在我有了这个 TLA 文件，我在其中定义了一些常量：

我想在 cfg 文件中设置以下内容：

但这会导致以下错误：

到目前为止，我只找到了这个解决方法：

.tla

.cfg

所以，定义一个 CONSTANT 似乎没用。

我做错了什么，或者这是预期的行为？

谢谢

有一个想法写这样的东西：

..但它不是那样工作的。

我开始了探索 TLA+ 和更正式的软件工程的旅程。我正在使用 TLA Toolbox 版本 1.6.0，但是，我注意到内置文档和在线文档都没有提供有关如何编辑或设置自动生成的修改历史日志中使用的默认“作者姓名”的任何提示。

例如，在我当前的机器上，日志采用以下形式...

那个“GAMER”是我想要修改的字符串——比如说，我的首字母。但是，尽管您可以手动编辑该名称内联 - 在模块编辑器中，当您保存此更改时，新的修改注释会插入到历史记录中，但之前的错误相同！

如何解决这个问题？使用了一些环境变量？配置文件或注册表值？我会理解它可能会读取系统用户信息左右，但这也不是我的系统用户名！

这可能是一个非常愚蠢的问题，但我还是会问。

我正在看 Leslie Lamport 关于 TLA+ 的视频。在名为“Die Hard”的视频四中，他给出了实施BigToSmall和SmallToBig公式的练习。长话短说：我们需要正确计算 3 加仑和 5 加仑的水壶从一个罐子倒到另一个罐子后的水量。

这是他的解决方案：

我尝试使用这个和/或列出一些东西：

但是当我运行它时，检查并没有终止，我不知道为什么。

我正在编写一个简单的客户端-服务器交互规范来学习 TLA+：

正如您所希望看到的，客户端可以对服务器运行一些查询，如果会话正常，它将得到一个结果，否则它会收到一条需要授权然后重试的消息。会话可以随时到期。

我想确保客户端最终会得到结果，所以我在属性中添加了这一行：

在模型检查时，我遇到了一个这样的反例：Init -> (Query -> Unauthorized -> Authorize -> Expire)，括号中的部分无限重复。我的第一个想法是对OKstep 提出强烈的公平要求。然而，问题是在这种情况下，OK步骤从未启用。

我可以添加诸如[]<><<OK>>_vars（其内容为“最终OK发生的情况总是如此”）之类的内容，但这感觉像是在作弊，并且从我收集到的内容中，使用任意时间公式指定活跃度——而不是弱公平或强公平——是不受欢迎的。

如何使用弱公平或强公平来保证查询最终会得到响应？还是我的模型不好？我没主意了...

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

但是我遇到了意外的异常错误，例如

尝试加载自定义 FPSet 类失败：tlc2.tool.fp.OffHeapDiskFPSet TLC 引发意外异常。这可能是由规格或模型中的错误引起的。请参阅用户输出或 TLC 控制台以获取有关发生情况的线索。异常是 java.util.concurrent.ExecutionException ： java.lang.NullPointerException

和用户输出：

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

更新：

TLA+ 工具箱版本：