合金 - 孤立实例

我正在写一个简单的合金代码，但我不明白我怎么能说大多数一个A与p.D（所以大多数将是一个或零）关联。所以我写了下面的代码，但断言呈现没有反例与P1没有D的实例。你能帮我怎么定义我的事实在AT MOST一个实例，我可以看到一个计数器例如是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

来源

2013-09-22 user1021110

你的规范没有连接（导入SIG P1的）表示，对在P1每个p总是由d到恰好一个相关一在A.你实际上是多余的（” 0或1“暗示为”始终1“）。

你可以宣布“SIG P1延伸P（d：孤独的A}”。（事实上仍然是多余的）

还要注意的是，“& A”在你的事实，并断言是多余的。

您可能意味着一个事实是事实{孤独P1.D} 它说，所有这些都与一个A P1的情况下，都与同一A.

来源

2013-09-23 05:08:48 user1513683

是的，你是对的我忘记了默认的多重性是“一”，我同意你关于代码中的冗余，但它不会影响结果。 – user1021110

合金 - 孤立实例

回答

相关问题