Использование понимания множества в бинарных отношениях в Alloy

У меня есть следующие подписи:

sig Id, Grade {}

sig Foo {
    result : Id -> Grade
}

Теперь я хочу создать функцию, которая принимает переменную foo и возвращает все связанные отношения Foo -> Grade:

fun results[ id : Id ]: Foo -> Grade {
    //return all Foo->Grade binary relationships such that "id -> grade" in Foo.result
}

i.e.

Итак, если отношение «результат» такое:

(foo0, id0, grade0)
(foo0, id1, grade0)
(foo0, id2, grade1)
(foo1, id0, grade2)
(foo1, id3, grade3)
(foo2, id0, grade0)

и я запускаю функцию "результаты [id0]", я бы получил:

(foo0, grade0)
(foo1, grade2)
(foo2, grade0)

Теперь я думаю, что я бы использовал какое-то понимание набора, но проблема в том, что понимание набора работает только с унарными наборами, а не с бинарными наборами.


alloy
person Yahya Uddin    schedule 07.03.2015    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Теперь я думаю, что я бы использовал какое-то понимание набора, но проблема в том, что понимание набора работает только с унарными наборами, а не с бинарными наборами.

Правильно в первый раз (да, используйте понимание множества), не совсем правильно во второй (понимание множества прекрасно работает с отношениями). См. раздел B.8 справочника по языку или 3.5.5 документа Абстракции программного обеспечения.

Попробуйте что-то вроде этого (не проверено!):

fun results[ id : Id ]: Foo -> Grade {
/* return all Foo->Grade binary relationships
   such that "id -> grade" in Foo.result */
   { f : Foo, g : Grade 
     | f -> id -> g in result } 
   /* not Foo.result, that was a slip */
}

Может быть умный способ написать требуемый набор без понимания, просто используя соединения коробки и соединения точками, но если он есть, на данный момент он ускользает от меня. Самое близкое, что я получаю, это

{ f : Foo, g : Grade | f.result.g = id }
person C. M. Sperberg-McQueen    schedule 08.03.2015
comment
О большое спасибо! Но разве это не было бы так: { f : Foo, g : Grade | f -> id -> g в результате }, а не Foo.result, поскольку Foo.result возвращает Id-›Grade, а просто результат дает полный Foo-›Id-›Grade - person Yahya Uddin; 08.03.2015
comment
Хороший улов! (Я рад, что предупредил вас, что не проверял это.) Я исправил код в ответе. - person C. M. Sperberg-McQueen; 08.03.2015