时间戳

首页 > 解决方案 > 合金阵列模型

testing - 合金阵列模型

问题描述

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

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 字段的方法。有人可以帮帮我吗？谢谢

标签： testingmodelingalloy

解决方案

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

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

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。它拥有您想要的一切以及更多。

推荐阅读