如何訪問由Alloy函數返回的集合中的元素？

Question

我有一個鋁合金的功能在我的模型，如：

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 
    { 
    ... 
    } 
} 

甚至當我改變爲「設置字段」的函數的返回，錯誤「這種表達沒有被類型檢查「出現。我只想獲得由函數返回的集合的第一個元素，有什麼幫助？

Answer 1

在這種情況下，訂單真的很重要嗎？如果是的話，你應該在這個看一看：seq

在下面的例子中，每個人P， 「p.books」 是一個序列書 ：

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

...所以，如果s是書的序列，那麼第一個元素是S [0] ...

seq現在是一個保留字，但只不過是一個關係Int -> Elem更多。

---

如果沒關係，你可以使用適當的量詞，例如：

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

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