Рассмотрим следующую спецификацию в Alloy:
sig Books {}
fun f[b:Books] : Books {
{b':Books | b' = Books -b }
}
run show {}
Предположим, у нас есть экземпляр, для которого $univ = {Books$0, Books$1, Books$2}$. Вычисление функции f с $Books$0$ дает пустой набор вместо ${Books$1, Books$2}$:
f[Books$0]
{}
Есть идеи, почему?
Это из-за того, как работает понимание множества.
{b':Books | b' = Books - b }
Это выражение возвращает все одиночные подмножества Books, равные Books - b. Но Books - b — это набор из двух элементов. Таким образом, ни один одноэлементный набор не равен ему, и общий результат равен {}.
Вы, вероятно, просто хотите:
fun f[b:Books] : Books {
Books - b
}
