基數限制令人無法容忍

Question

即使在簡單的示例中，我也無法使Alloy的基數運算符（#）按預期工作。

例如，下面的合金文件...

sig Y {} 

sig X {r : Y -> Y} { 
//#r = 2 
} 

run {} for exactly 1 X, 3 Y 

...給我，恰好包含2個r -edges溶液（見下圖）。但是，如果我取消#r = 2這一行的註釋，Alloy就不會找到解決方案！我究竟做錯了什麼？

---

編輯。我發現這個問題隻影響AlloyStar（與香草合金相反）。當使用AlloyStar（0.2版本），我得到

執行 「運行運行$ 1整整1 X，3 Y」

求解= minisatprover（JNI）位寬= 1 MaxSeq = 0對稱= 20

69變異。 12個主要變量。 167條款。 923ms。

發現實例。謂詞是一致的。 21ms。

但是當我取消對#r = 2，我得到

執行 「運行運行$ 1整整1 X，3 Y」

求解= minisatprover（JNI）位寬= 1 MaxSeq = 0對稱= 20

0變量。 0個主要變量。 1條款。爲15ms。

找不到實例。謂詞可能不一致。 1毫秒。

所以我想這個問題已經成爲AlloyStar開發者的錯誤報告！

Answer 1

感謝您的錯誤報告。這裏有幾件事情正在進行。實質上，所有的danielp都是正確的，但是完整的答案有點微妙。

首先，我假設你已將「禁止溢出」選項設置爲true，否則無論指定整數範圍（位寬）如何，您都將獲得實例。

接下來，我們不要使用「附加事實」，因爲附加事實可以具有不同的語義，具體取決於是否啓用了「啓用隱式此選項」選項。因此，讓我們假設以下合金型號：

sig Y {} 
sig X {r: Y -> Y} 

fact { #r = 2 } 

run {} for exactly 1 X, 3 Y 

現在，在Alloy4.2，在沒有約束整數指定，使用的發動機代表整數表達式默認的位寬（例如，基數表達式，整型常量等。）是5;因爲常數2可以用5位表示，所以不會發生溢出並找到一個實例。

另一方面，在Alloy *中，默認位寬爲1，不足以表示常數2，因此發生溢出並且未找到實例。爲什麼選擇bitwidth 1作爲默認值？我不是100％確定的，但可能是因爲增加了對位向量的支持以及使用位向量的一些綜合基準，所以在編寫時很方便。

Answer 2

看來你必須配置位寬：

執行 「運行運行$ 1整整1 X，3 Y」

求解= minisatprover（JNI）位寬= 1 MaxSeq = 0對稱= 20

0變量。 0個主要變量。 1條款。爲15ms。

找不到實例。謂詞可能不一致。 1毫秒。

數字2不能用位寬1表示。我想這個例子在標準合金中工作，因爲默認的位寬在那裏更高。