tla+ - 在 TLA+ 中如何表达一个命题是独立的？

Question

假设以下内容不正确

THEOREM Spec => []P \* Not correct!

也就是有一些不满足Spec的行为表现出来[]P。我如何在 TLA+ 中表达这一点？

如果我使用简单的否定，我最终得到

THEOREM Spec /\ <>~P \* Also not correct!

然而，这个定理也有可能是不正确的！特别是，即使有一些行为不满足Spec，[]P也可能有一些行为满足，并且这种行为会反驳这个新定理。

是否有某种方式来表达“这个定理对于某些行为是不正确的”的想法，即对行为进行量化？

编辑：在考虑了我所要求的确切性质之后，我真的在问是否有一种[]P独立于注释的方法Spec？

score 0 · Accepted Answer

执行此操作的常用方法是编写THEOREM ~(Spec => []P)一个[]P临时属性，并告诉人们如果该属性失败，规范是正确的。

score 0 · Accepted Answer

如果将属性参数化为带参数的运算符，则可以表示存在满足Spec(x)但违反的行为[]P(x)。使用存在时间量化 ( \EE)，这可以表示如下

Spec(x) == ...  (* a suitable definition here *)
P(x) == ...  (* a suitable definition here *)

THEOREM \EE x:  Spec(x) /\ ~ []P(x)

我们假设在运算符Spec(x)和的定义中没有变量出现P(x)。

我们也可以表示同时存在满足的行为Spec(x) /\ []P(x)和满足的行为，Spec(x) /\ ~ []P(x)如下所示

THEOREM /\ \EE x:  Spec(x) /\ []P(x)
        /\ \EE x:  Spec(x) /\ ~ []P(x)

score 0 · Accepted Answer

我们在经典逻辑中，这[]P \/ ~[]P是有效的。你重述了第二部分，这样我们就有了[]P \/ <>~P。因此，对于 any P，两者之一将是正确的。

3 回答 3