合金関数によって返されたセット内の要素にアクセスする方法は？

Question

Iは次のように私のモデルにおける合金機能を有する：関数の戻り値であるが {$ 1のフィールド、フィールド$ 0} ：この関数は私のモデルで動作しているとなどの要素の集合を返すことができる

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

"フィールドを設定"しないでください。私はすでに合金評価ツール（alloy4.2.jarで利用可能）を通じてこれを見ていました。どのような私は、例えば、別の述語でこのセットの最初の要素を取得してやろうとしています：私は、「フィールドの設定」する機能のリターンを変更する場合でも、エラーが「この表現はに失敗した

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

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

be typechecked "と表示されます。私は、関数、任意の助けによって返されるセットの最初の要素を取得したいですか？

Answer 1

この場合、注文は本当に問題になりますか？もしそうなら、あなたはこれを見て取る必要があります。一人一人pに対して、次の例ではseq

を、 "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 ... 
    } 
} 

を使用することができます