比較謂詞

Question

海報問如何比較Alloy中的函數。在測試一個小例子（比較謂詞而不是函數）來回答這個問題時，我注意到了下面的行爲，這讓我很困惑。

只要檢查命令的邊界高於3且事實'f1'處於活動狀態，分析儀就不會找到反例。激活事實，分析儀按預期工作。爲什麼冗餘事實'f1'修改分析儀的操作，以及爲什麼在邊界高於3的情況下？

open util/ordering [V] 
sig V {} 

fact f1 { 
    # V > 0 
} 

pred p1 [x: V] { 
    x = last 
} 

pred p2 [x: V] { 
    x = first 
} 

assert a1 { 
    all x: V | p1[x] <=> p2[x] 
} 

check a1 for 3 

似乎只要檢查邊界是4或更高，並且'f1'處於活動狀態，分析儀就會報告'0變量。 0個主要變量。 0條款。「

Answer 1

我目前無法查看詳細信息，但看起來您可能會看到溢出行爲，部分原因是Alloy的整數非常窄（默認情況下爲4位，我相信？）二進制補碼整數，所以溢出定期發生。

幾個變化可能是有益的，分別或一起，看看他們是否會影響行爲。

• 替換事實F1與some V
• 接通「禁止溢出」選項
• 使用scope命令（其他簽名關於INT提供一個明確的比特寬度，範圍數字指定實例的最大數目;對於詮釋它指定一個位寬）

由於盧瓦克Gammaitoni已經把它放在另一個問題在這裏「你應該在合金玩數字遊戲時，一定要加倍小心。」