如何實現一個數字序列，每個連續的對增加到4？

Question

我有一個序列（seq）的數字。

我想每增加一個連續的對數字的平等4

下面是我在實施這一嘗試。但是，這是錯誤的。該合金分析表明我這是錯誤的，通過生成這種情況下：

2, 2, -2, 4 

第一對增加4（2 + 2 = 4）

第二對沒有。 （2 + -2 = 0）

什麼是正確的實現方式？注意：我需要使用序列（seq），所以請不要更改簽名或其字段。我希望你能告訴我正確的方式來表達fact。或者，告訴我，如果使用seq，則不可能實施。

one sig Test { 
    numbers: seq Int 
} 

fact { 
    all disj n, n': Test.numbers.elems { 
     (plus[Test.numbers.idxOf[n], 1] = Test.numbers.idxOf[n']) => 
      plus[n, n'] = 4 
    } 
} 

run {#Test.numbers.indsOf[2] > 1} 

Answer 1

要解釋爲什麼你的事實是不正確，請考慮以下的反例：在Test.numbers序列2, 2, 2, 4。

在該反：

• Test.numbers.elems評估爲2, 4
• Test.numbers.idxOf[2]是0（元件2的第一索引）
• Test.numbers.idxOf[4]是3
• 沒有兩個不相交的n和n'在Test.numbers.elems（即，{2, 4}）這樣plus[Test.numbers.idxOf[n], 1] = Test.numbers.idxOf[n']所以事實平凡。

以下事實應該正確表達你想要的屬性：

fact { 
    all i: Test.numbers.inds - (#Test.numbers).prev | 
     plus[Test.numbers[i], Test.numbers[i.next]] = 4 
} 

• mySeq.inds計算結果爲序列mySeq
• i.next評估爲i + 1
• i.prev的指數計算結果爲i - 1