Как вернуть единственное значение для функции в Alloy?

Question

найти много трудностей в поиске хороших ресурсов на функции в сплаве. Я успешно создал функцию, которая возвращает набор значений (т. Е. Имеет возвращаемый тип "set"), но я не могу понять, как написать функцию, которая возвращает единственное значение. я. у них есть

open util/ordering[Time]   // enforces total order on Time

sig Time {}                // instances denote timestamps

sig File {
   time : Time             // every file has exactly one timestamp
}

fun getTime[F : set File] : Time {
     {one t : Time | some f : F | all g : F | f.time = t && gte[f.time,g.time]}
}

Функция getTime принимает набор файлов и возвращает самую последнюю отметку файла (атрибут наибольшего времени всех файлов в F), однако, независимо от того, каким образом я ее записываю, я получаю неправильный возвратошибка типа (Primitive Boolean) или другая ошибка. Как я могу вернуть что-то типа времени?

Answer 1

Вы получаете логический тип возврата из-за ключевого слова one. Этот квантификатор обеспечивает возвращение true тогда и только тогда, когда существует ровно один Time t, удовлетворяющий следующему предикату.

Без какого-либо квантификатора выражение в вашей функции было бы тем, что мы называем пониманием множеств, то естьмножество, содержащее каждый раз атомы, удовлетворяющие следующему предикату, будет возвращено

fun getTime[F : set File] : Time {
     {t : Time | some f : F | all g : F | f.time = t && gte[f.time,g.time]}
}