如何实现一个数字序列，每个连续的对增加到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