如何访问合金函数返回的集合中的元素？

Question

我的模型中有一个 Alloy 函数，例如：

fun whichFieldIs[p:Program, fId:FieldId, c:Class] : Field{
     {f:Field | f in c.*(extend.(p.classDeclarations)).fields && f.id = fId}    
}

此函数在我的模型中运行，可以返回一组元素，例如： {字段$0，字段$1} 虽然函数返回不是“设置字段”。我已经通过合金评估工具（alloy4.2.jar 中提供）看到了这一点。我想要做的是在另一个谓词中获取这个集合的第一个元素，例如：

pred expVarTypeIsOfA[p:Program, exprName:FieldId, mClass:Class, a:ClassId]{

    let field = whichFieldIs[p, exprName, mClass],
         fieldType = field[0].type 
    {
     ...
    }
}

即使我将函数的返回更改为“set Field”，也会出现错误“This expression failed to be typechecked”。我只想获取函数返回的集合的第一个元素，有什么帮助吗？

Answer 1

在这种情况下，顺序真的很重要吗？如果是这样，你应该看看这个：seq

在以下示例中，对于每个人 p，“p.books”是一个序列 书籍：

sig Book { }
  sig Person {
      books: seq Book
  }

...所以如果s是Book的序列，那么第一个元素就是s[0]...

seq 现在是保留字，但只不过是关系Int -> Elem。

---

如果没关系，你可以使用适当的量词，例如：

pred expVarTypeIsOfA[p:Program, exprName:FieldId, mClass:Class, a:ClassId]{

    some field: whichFieldIs[p, exprName, mClass] | {
         field.type ...
    }
}