Возможно написать такой запрос более высокого порядка (например, найти такой набор товаров, что никакой другой набор товаров не имеет более низкой общей цены< /em>), но невозможно автоматически решить ее. Однако есть несколько обходных путей.
Во-первых, вот как вы можете переписать свою модель, чтобы вам не приходилось вручную прописывать 10 различных сигм для цен от 1 до 10:
sig Item {
price: one Int
}
pred nItems[n: Int] {
#Item = n
all i: Int | (1 <= i && i <= n) => one price.i
}
fact { nItems[10] }
Теперь вы можете выразить вышеупомянутый запрос в Alloy следующим образом:
fun isum[iset: set Item]: Int {
sum item: iset | item.price
}
run {
some miniset: set Item |
#miniset = 3 and
no iset: set Item |
#iset = #miniset and
isum[iset] < isum[miniset]
} for 10 but 5 Int
но если вы попытаетесь запустить его, вы получите следующую ошибку:
Анализ не может быть выполнен, так как он требует количественной оценки более высокого порядка, которую нельзя сколемизировать.
Вместо этого вы можете проверить, существует ли набор товаров, общая цена которых ниже данной цены, например,
pred lowerThan[iset: set Item, num: Int, min: Int] {
#iset = num and
isum[iset] < min
}
check {
no iset: set Item |
iset.lowerThan[3, 7]
} for 10 but 5 Int
В этом примере нужно проверить следующее свойство: не существует набора ровно из 3 предметов, общая цена которых меньше 7. Если теперь вы попросите Alloy проверить это свойство, вы получите контрпример, в котором iset содержит ровно 3 товара с наименьшей ценой, и, следовательно, его общая цена равна 6. Затем, если вы измените приведенную выше команду проверки, чтобы спросить, существует ли набор из 3 предметов, общая цена которых меньше 6, вы не получите контрпример, а это означает, что 6 действительно самая низкая возможная цена. Как видите, вы не можете попросить Alloy сказать вам, что ответ равен 6 за один запуск, но вы можете запускать Alloy итеративно, чтобы прийти к такому же выводу.
person
Aleksandar Milicevic
schedule
02.09.2013
