如何实现一个数字序列，每对连续的数字加起来等于 4？

Question

我有一个数字序列 (seq)。

我希望每对连续的数字相加等于 4。

下面是我尝试实现的。但是，这是错误的。 Alloy 分析器通过生成此实例向我表明这是错误的：

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
在 Test.numbers.elems 中没有两个不相交的 n 和 n'（即 {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

如何实现一个数字序列，每对连续的数字加起来等于 4？

How to implement a sequence of numbers, each consecutive pair adds to 4?

alloy