約束語法謂詞和聲明

Question

我想知道如果在謂詞中使用約束語法，而不是在斷言中使用約束語法。

約束all disj x1，x2：X | x1 = x2在謂詞和斷言中執行時會給出不同的結果。

例如，假定下面的模型：

sig A {} 

sig B {x: one A} 

assert S1 
{all x1,x2: x | x1 = x2} 

檢查S1 2 - 作爲反例x1和x2

assert S2 
{! (all x1,x2: x | x1 = x2)} 

檢查S2的2非等效實例 - 較高階量化錯誤

pred P1 
{(all x1,x2: x | x1 = x2)} 

run P1 for 2 -- higher-order quantification error 

pred P2 
{! (all x1,x2: x | x1 = x2)} 

run p2 for 2 --generates non equivalent instances of x1 and x2

爲什麼有些約束是可以量化的，而它們的否定不是，反之亦然！

感謝

阿卜杜拉Rayhan的

Answer 1

在這些例子全部4你有一個高階量詞：你想的二進制字段（x: A -> B）量化過來的，所以當你說all x1, x2: x | ...，它意思是「對於從二元關係x繪製的所有二元元組x1和x2」。合金是一階的，一般不能處理更高階的東西。它在某些情況下沒有抱怨的原因是它能夠「量化」量詞，因此它不需要檢查任何東西全部元組大於1.

例如，當你說check S1時，如果對於所有二進制元組來說，事情是成立的，你就問合金;因爲Alloy是一個有界的模型尋找器，所以它會試圖通過找到一個這樣的元組來反駁這個元組，而這個元組沒有持有---這裏沒有更高的順序，所以這種情況將會起作用。當你說「檢查S2」時，如果對於所有的二元元組來說都是不成立的，你就問合金，所以要反駁合金實際上必須檢查每個這個二元元組的是更高的順序和合金不能做到這一點。

我不知道你的意圖是否首先要進行這種高階量化。只是猜測，也許你想要的只是all b: B, a: b.x | ...，這是一階，並會正常工作。