合金阵列模型

Question

我刚开始学习合金模型语言，并试图在合金中编写自己的数组模型。但是，我无法从关系中提取索引。这是我的信号和事实：

sig Element {}

one sig Array {
  // Map index to element
  IdxEle: Int -> Element,
  // Length of the array.
  length: Int
}

fact Index {
    all r : IdxEle | r.Int >= 0 and r.Int < length
}

我得到的错误是

This must be an integer expression.
Instead, it has the following possible type(s):
{none->none}

我查看了参考指南，但找不到提取关系的 idx 字段的方法。有人可以帮帮我吗？ 谢谢

Answer 1

首先，您的模型中的 r 是 Array->Int->Element 类型，因此无法计算 (Array->Int->Element).Int，因为元组中的最后一列是 Element 类型，而不是您似乎期望的 Int 类型。 （加入Alloy时，左侧最后一列必须与右侧第一列类型相同。）

其次，有更简单、更灵活、更易读的方式来表达你想要的：

sig Element {}

let range[start,end] = {  i : Int | i >= start and i < end }

one sig Array { index : Int -> Element } {
    index.Element = range[ 0, len[this] ]
}

fun len[ array : Array ] : Int { # array.index }

第三...有一个内置类型为你称为seq。它拥有您想要的一切，甚至更多。