0

我正在编写一个简单的合金代码，但我不明白我怎么能说最多一个 A 与 pD 相关联（所以最多是一或零）。所以我写了下面的代码，但断言没有给出没有 D 的 P1 实例的反例。你能帮我吗？我如何定义我的事实，即在最多有一个 pD 实例的情况下，我可以看到一个反例p 与它的 D 没有任何联系。

abstract sig A {}
sig A1,A2,A3 extends A{}
abstract sig P {}
sig P1 extends P {D: A}

fact
{
all p: P1 | lone (p.D & A)
}

assert asr 
{no p: P1 | no (p.D & A)}
check asr for 5
4

1 回答 1

2

您的规范（sig P1 的介绍）说，对于 P1 中的每个 p 总是由 d 与 A 中的一个 a 相关联。您的事实是多余的（“始终为 1”暗示“0 或 1”）。

您可以声明“sig P1 extends P (D : lone A}”。（事实仍然是多余的。）

另请注意，您的事实和断言中的“& A”是多余的。

你可能认为事实是事实{lone P1.D}，它表示所有与 A 相关的 P1 实例都与同一个 A 相关。

于 2013-09-23T05:08:48.007 回答