Есть ли прямой способ представить тип остатка в Alloy вместо того, чтобы явно вычитать объединение всех подтипов? Например, в:
sig Test {}
one sig A, B extends Test {}
Я хотел бы иметь возможность ссылаться на выражение Test-(A+B) с помощью сокращенной записи, которую не нужно менять каждый раз, когда Test расширяется новым знаком. Хотя это будет всего лишь синтаксический сахар, это может помочь мне избежать ошибок при рефакторинге моделей.
Вы можете ввести набор, представляющий остаток, следующим образом:
abstract sig Test {}
sig Remainder extends Test {}
one sig A, B extends Test {}
Это разделит набор из Test атомов на три подмножества, где Remainder будет эквивалентно Test - (A + B). Если вы позже решите расширить Test, добавив, например, one sig C, Remainder все равно даст вам оставшийся набор.
Я давно не использовал Alloy, но не думаю, что это возможно так, как вы этого хотите. Однако вы можете преобразовать объединение только в одно место в модели. Пример:
sig Test {}
one sig A, B extends Test {}
fun Remainder : set Test {
Test - (A+B)
}
run { some Remainder } for 5
Вы определяете отношение с помощью функции, называемой здесь Remainder, которая определяется путем вычитания объединения всех подтипов из базового типа.
Каждый раз, когда вы добавляете новый подтип в модель, просто не забывайте добавлять его в определение Remainder тоже, и все готово.
Во всей модели вы можете просто ссылаться на Remainder, чтобы получить все чистые Test атомы, как я использовал в анонимном предикате в команде run.
Если вы хотите, чтобы это определение содержало любые новые символы, расширяющие Test, вы можете использовать малоизвестный мета-возможности, которые позволяют перебирать подписи через специальный набор sig$.
Например, вы можете сделать что-то вроде:
fun Remainder [] : set Test {
{t : Test | all sig : sig$ | sig = Test$ || t not in sig.value}
}
