在Alloy

Question

中強加一個孤立的屬性我想知道是否有辦法強制簽名的屬性爲空。我想這樣，但似乎不起作用：

sig C { 
myattribute: lone Type 
} 

SIG類型{ ATT1：詮釋 ATT2：.....等。 }

fact { 
    all c: C| 
     (my condition) 
     <=> 
     (
      no c.myattribute 
     ) 
} 

至於現在，我們可以只想想defing與抽象簽名的結構是這樣的：

abstract sig GeneralType {} 
one sig Empty extends GeneralType {} 
sig NotEmpty extends GeneralType {...arguments (att1,2....} 

Answer 1

現有的代碼應該已經做工給予正確my condition。 （wmeyer確實是在提示正確的。）

您可以測試你的約束，以確保它表現爲你所期望的：

sig Type { } 

sig C { 
    myattribute: lone Type 
} 

fact { 
    all c: C | no c.myattribute 
} 

run { } for 5 

check { 
    all c: C | no c.myattribute 
} for 5