tla+ - 如何证明或模型检查 TLA+ 中的定理？

Question

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

--------------------------- MODULE TestModule ---------------------------
EXTENDS Naturals

CONSTANT input

Numbers == { n \in Nat : n > 9 /\ n < 100 }

DividesBy2(n) == (n % 2) = 0

DividesBy2Once(n) == DividesBy2(n) /\  ~DividesBy2(n \div 2)

NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) }

THEOREM input \subseteq NumbersThatDivideBy2Once

=======================

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

Answer 1

给你的定理一个名字，

THEOREM T == input \subseteq NumbersThatDivideBy2Once

转到“模型检查结果”选项卡，并在“评估常量表达式”中引入T，以便对其进行评估。

---

您的模型检查器需要被告知如何处理规范文件，该文件本质上只是数学定义的集合。

在“正常使用”中，您希望向 TLC 提供一个表示您的规范的时间公式（通常Spec在规范文件中给出名称）。您在“什么是行为规范？”下的“模型概述”选项卡中介绍它。这就是 TLC 用来执行模型检查的方法。

在这种情况下，你没有那个。因此，只需保留“无行为规范”选项，并如上所述，在“模型检查结果”选项卡中指定要评估的常量表达式。