剩餘類型的合金語法？

Question

是否有直接的方式來表示Alloy中的餘數類型，而不是必須顯式減去union all的所有子類型？例如，在：

sig Test {} 
one sig A, B extends Test {}  

我希望能夠通過速記並不需要改變每次Test獲得由新SIG延伸到指表達Test-(A+B)。雖然這隻會是語法糖，但它可以幫助我在重構模型時避免錯誤。

Answer 1

你可以介紹一組表示剩餘如下：

abstract sig Test {} 
sig Remainder extends Test {} 
one sig A, B extends Test {} 

這將設定Test原子劃分爲三個子集，與Remainder等同於Test - (A + B)。如果您稍後決定通過添加one sig C來擴展Test，例如Remainder仍然會給您餘下的設置。

Answer 2

我有一段時間沒有使用合金，但我不認爲這是可能的你想要的方式。但是，您可以將該聯合重構爲模型中的一個位置。例如：

sig Test {} 
one sig A, B extends Test {} 

fun Remainder : set Test { 
    Test - (A+B) 
} 

run { some Remainder } for 5 

您定義的關係，使用功能，這裏叫做Remainder，由從基類中減去所有亞型的聯合限定。
每當您爲模型添加一個新的子類型時，請記住將其添加到Remainder的定義中，並且您很好。

整個模型，你可以參考Remainder讓所有純Test原子，正如我在匿名謂詞應用於run命令。

Answer 3

如果你想定義持有任何延長Test都推出了新的SIGS，你可以使用合金的鮮爲人知meta capabilities，使您可以通過SIGS通過一組特殊的sig$迭代。

例如，你可以這樣做：

fun Remainder [] : set Test { 
    {t : Test | all sig : sig$ | sig = Test$ || t not in sig.value} 
}