我正在编写一个简单的合金代码，但我无法理解我怎么能说AT一个A与p.D相关（因此AT MOST将是一个或零） . 所以我编写了下面的代码，但是断言提供了 no counter-example ，其实例为P1而没有D.你能帮助我如何定义我的事实，就是让我有一个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
1 回答
你的规范（sig P1的介绍）说P1中的每个p总是与d相关，恰好是A中的一个a . 你的事实是多余的（“0或1”暗示为“总是1”） .
你可以声明“sig P1扩展P（D：孤独A}” . （事实仍然是多余的 . ）
另请注意，事实和断言中的“＆A”是多余的 .
你可能认为事实是{孤独的P1.D}，它说所有与A相关的P1实例都与相同的A.有关 .