В модели, которую я начал рисовать в Alloy на днях, я получаю следующее сообщение, когда пытаюсь найти экземпляр определенного предиката:
Объем перевода превышен. В этом контексте Вселенная содержит 34 атома и отношения арности 12 не могут быть представлены. Посетите http://alloy.mit.edu/, чтобы получить рекомендации по рефакторингу.
Любые предложения о том, где на сайте Alloy.mit.edu искать? Я не нашел ничего с очевидным ярлыком вроде «Модели рефакторинга, которые превышают возможности перевода».
Это существенный вопрос.
[Постскриптум: причиной моей проблемы, по-видимому, была неправильная начальная формулировка объявлений количественных переменных, которые я использовал в предикате; проблема исчезла, как только я правильно понял синтаксис объявлений. Полная информация недостаточно информативна, чтобы ее стоило записывать, поэтому я опускаю первоначальное описание деталей. Краткая версия такова: чтобы получить экземпляр конкретного конкретного примера, я изначально написал предикат в форме
pred m {
one t1 : table,
r1, r2, r3 : row,
c1, c2 : column,
c11, c21 : headingcell,
c12, c22, c13, c23 : datacell | {
... // description of the example here
}
}
one охватывает все двенадцать переменных и [как мне сказали из надежных источников] внутренне переводится в понимание множества, определяемое отношением арности 12. Я хотел сказать нечто более похожее на следующее, что не вызывает проблема с возможностями перевода:
pred m {
some t1 : table |
some disj r1, r2, r3 : row |
some disj c1, c2 : column |
some disj c11, c21 : headingcell |
some disj c12, c22, c13, c23 : datacell | {
...
}
}
Итак: один из способов исправить некоторые модели, которые вызывают сообщение об ошибке способности к переводу, — очистить количественную оценку переменных.
Однако основной вопрос сохраняет интерес: когда модель выдает сообщение об ошибке возможности перевода, а квантификаторы уже чисты и правильны, есть ли документ для чтения?]
