合金4.2的語義變化對合金書的練習A.1.6的影響？

Question

根據合金4.2的release notes，存在與整數有關的語義變化。這些變化似乎對合金書的練習A.1.6有影響。

在本練習中，以下代碼作爲基礎給出（我在最後添加了「Int」以顯示我的問題）。當運行「顯示」謂詞時，可視化工具將顯示一個實例，但除了整數外，此實例還包含另外兩個原子「Univ0」和「Univ1」。

module exercises/spanning 

pred isTree(r: univ->univ) {} 
pred spans(r1, r2: univ->univ) {} 

pred show(r, t1, t2: univ->univ) { 
    spans[t1,r] and isTree[t1] 
    spans[t2,r] and isTree[t2] 
    t1 != t2 
} 
run show for 3 Int 

這兩個原子「Univ0」和「Univ1」是什麼意思？他們爲什麼在那裏？它們沒有在合金4.1.10上執行相同的代碼。

Answer 1

當沒有用戶定義的sigs時，Alloy自動合成一個名爲「Univ」的新信號。這是一個非常方便的功能，因爲它可以讓您在整個宇宙中編寫公式，而無需引入任何sigs。

當你明確地爲Int提供一個範圍時，宇宙將肯定包含給定範圍內的所有Int原子。如果另外還有沒有用戶定義的sig，你最終會得到合成的Univ sig。當明確使用Int範圍時，綜合Univ sig是否合理是值得商榷的。

要解決你的問題，你有幾種選擇：

1. 如果你不在乎你是什麼圖形節點（即你不明確希望的節點是一個int類型），那麼你可以簡單地改變運行命令來說

   run show for 3而不是run show for 3 Int。

   如果你這樣做，你將沒有詮釋原子，只有大學原子。如果您不喜歡Univ標誌，只需引入一個新的標誌，例如sig Node {}，在這種情況下，所有原子的類型將爲Node。

2. 如果您確實希望您的圖形只能超過Ints，則可以在所有謂詞中將univ->univ更改爲Int->Int。

3. 如果您確實希望您的Universe只包含Int原子（在這種情況下，您可以在謂詞中保留univ->univ），那麼可以引入一個虛擬簽名並添加一個確保其基數爲零的事實。

   sig Dummy {} 
   fact { no Dummy } 
   

   這個小小的變化將確保Univ sig不會自動合成，並且不會影響模型的其餘部分。

希望這會有所幫助。