合金 - 孤立實例

我正在寫一個簡單的合金代碼，但我不明白我怎麼能說大多數一個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

合金 - 孤立實例

回答

相關問題