合金 - 单独实例

Question

我正在编写一个简单的合金代码，但我不明白我怎么能说最多一个 A 与 p.D 相关联（所以最多是一或零）。所以我写了下面的代码，但是断言提出了 no counter-example 有一个没有 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

Answer 1

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

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

还要注意，事实和断言中的“& A”是多余的。

你的意思可能是事实 事实{孤独的 P1.D} 这表示所有与 A 相关的 P1 实例都与同一个 A 相关。