我是新TLA+用户。我读到该TLA工具箱允许我们在模型检查完成后可视化状态图。

为此，我需要安装 dot 。但我不知道如何启动可视化。我可以使用 GUI 购买还是需要使用专用命令行？

谢谢

目前正在学习 TLA+，并且一直坚持使用这种简单的方法来从注册表中删除一个人。从我所见，问题似乎与许可状态有关。

我的 TLA+ 函数看起来像这样，它会从注册表中删除一个人以及权限。

我正在检查的 typeok 具有以下限制

我收到违反 typeOK 的模型错误。在堆栈跟踪中，错误看起来像这样

感谢您的任何见解

编辑：

以前的状态可能有一些用处

这个问题是关于 TLA+ 使用工具箱（https://github.com/tlaplus/tlaplus/releases）的，我找不到任何关于它的标签。对于那个很抱歉。这就是为什么我只用 Primes 标记的原因。如果我遗漏了什么，请善意添加更好的标签或创建缺失的标签。

这是问题

GCD 有一个众所周知的函数和算法。这里是。

这是一个众所周知的解决方案，它正在发挥作用。

我现在正在尝试使用这个编写一个 isPrime 函数。但我认为我的做法是错误的。我想知道你是否有想法。

谢谢

我有一个 TLA+ 模块，总结起来是这样的：

当我尝试使用 TLC 对此进行模型检查时，我收到以下错误：

TLC 引发了意外的异常。这可能是由规格或模型中的错误引起的。请参阅用户输出或 TLC 控制台以获取有关发生情况的线索。异常是 java.lang.RuntimeException：TLC 无法处理规范的这种结合：第 X 行，Y 行到 Z 行，模块组的 T 行

...指向Next.

我相信我Next的写得很好，因为这是一个与Next我的非常相似的示例模型：https ://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110

此外，Leslie Lamport指定系统的第 14.2.2 节说：

只有当表达式等于有限集[...]时，TLC 才能评估集值表达式。只有当 TLC 可以枚举集合S时，TLC 才会评估以下形式的表达式：

并提供“ S中存在x使得p ”的例子。

我该如何解决这个错误？

我有以下规格：

（我将这个规范简化到它没有做任何有用的事情的地步。）

当我尝试通过 TLC 运行它时，我收到以下错误：

在评估中，标识符成员要么未定义，要么不是运算符。

错误指向该Init行。

当我将Init行更改为：

它验证得很好。

我想要前一个功能，因为我的意思是members成为一个人的集合，而不是一个人。

根据Leslie Lamport's Specifying Systems的第 16.1.6 节，“TLA+ 在集合上提供了以下运算符：”并列出了\in和\subseteq。

为什么 TLA+ 不让我使用\subseteq？

下面的模块声明了一组 10 到 99 范围内的数字，它们只能被 2 整除一次并调用它NumbersThatDivideBy2Once。最后它声明了一个定理，即常数input是 的子集NumbersThatDivideBy2Once。

我如何检查这个定理是否适用于给定的输入？如果我使用提供的一组数字作为 运行模型检查input，即使其中一些数字不属于NumbersThatDivideBy2Once我仍然没有错误。

模块重载机制在此处的河内塔示例中进行了说明。它使您能够在 Java 中实现 TLA+ 运算符，以提高模型检查性能。

我一直在努力在 TLA+ 中定义一个有用的哈希函数（不，身份函数不适用于我的目的）并且我认为模块重载可能是实现它的方法。散列函数将接受一个 TLA+ 对象（例如，一条记录），并使用 JavahashCode()对对象的字符串表示的方法来确定性地导出其散列值。该值将返回给 TLA+ 规范。

这可能吗？Java 覆盖代码是什么样的？是否存在任何其他模块覆盖代码示例？

我有一个 TLA+ 规范，我想断言一个列表只会在长度上增长（如果它在口吃时保持不变就很好。）

现在我有这样的事情，但我确定这是不对的：

我什至不确定要在这里搜索什么，我确定我错过了一些非常明显的东西！

问题

我正在玩TLA+，并认为我会在 PlusCal 中编写以下明显错误的规范：

在检查IsStackAlwaysUnitLength为要报告的时间属性之一后，我希望 TLA+ 将此属性标记为失败。

但是，所有州都通过了！为什么它没有失败？

调试尝试

在使用语句进行调试时print，我注意到以下奇怪的行为：

调试面板中的产量

我不确定为什么stack := Append(stack, Len(stack));并且stack := Tail(stack);没有更新全局stack变量。

生成完整的 TLA 规范

我在 PlusCal 中的基本代码如下。

线IsFive(5)在工具箱中突出显示，当我尝试运行模型时，我收到一个错误，即宏 IsFive 未定义。

在类似的注释中，https ://learntla.com/tla/operators/说操作符是函数，然后在接下来的章节中继续定义函数。

假设我需要检查验证参数是否为 5 的功能。我应该使用什么，运算符或函数？