Итак, у меня есть предикат, который принимает набор в качестве аргумента, и поэтому я могу сделать это:
all disj t1, t2, t3: set Thing | predicate[t1+t2+t3]
Мне было интересно, можно ли это сделать, просто указав размер набора, так что что-то вроде
all ts: set of 4 Thing | predicate[ts]
Что я в конечном итоге хотел бы сделать, так это найти минимальное целое число, для которого действителен предикат. Это как-то возможно?
Количественное определение высокого порядка часто не рекомендуется, поскольку, насколько я понимаю, анализатор сплавов не всегда может с ними справиться. (для избавления от них используется сколемизация, но ее не всегда можно применить)
Таким образом, я бы упростил вашу модель следующим образом:
sig Thing{
}
run predicate for exactly 4 Thing
В pred predicate оцените интересующее вас свойство на полном наборе Thing (ограничено содержать ровно 4 атома) напрямую, например. Вещь.поле= ....
Кстати, я не думаю, что all disj t1, t2, t3: set Thing | predicate[t1+t2+t3] делает то, что вы от него ожидаете. В самом деле, t1 t2 и t3 — все множества Вещи со свойством непересекающихся множеств. Таким образом, t1+t2+t3 не обязательно будет производить набор из 3 вещей.
Не уверен, чего вы пытаетесь достичь здесь, но прямое выражение того, о чем вы, кажется, просите
all ts: set of 4 Thing | predicate[ts] -- not Alloy
было бы
all ts: set Thing | #ts = 4 implies predicate[ts]
