如何证明或模型检查 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

转到 "Model Checking Results" 选项卡，并在 "Evaluate Constant Expression" 中引入 T，以便对其进行评估。

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

在 "normal use" 中，您想为 TLC 提供一个代表您的规范的时间公式（通常在规范文件中给出名称Spec）。您在 "what is the behaviour spec?" 下的 "model overview" 选项卡中介绍它。这就是 TLC 用来执行模型检查的内容。

在这种情况下，您没有。因此，只需保留选项 "no behaviour spec" 并如上所述，在 "Model Checking Results" 选项卡中指定要计算的常量表达式。

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

How to prove or model check a theorem in TLA+?

tla+