Home Articles

合金 - 孤独的实例

Asked
Viewed 1766 times
0

我正在编写一个简单的合金代码,但我无法理解我怎么能说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 Answer

  • 2

    你的规范(sig P1的介绍)说P1中的每个p总是与d相关,恰好是A中的一个a . 你的事实是多余的(“0或1”暗示为“总是1”) .

    你可以声明“sig P1扩展P(D:孤独A}” . (事实仍然是多余的 . )

    另请注意,事实和断言中的“&A”是多余的 .

    你可能认为事实是{孤独的P1.D},它说所有与A相关的P1实例都与相同的A.有关 .

Related