Ограничения кардинальности неудовлетворительные
У меня проблемы с получением кардинального оператора Alloy (#) работает как положено даже на простых примерах.
Например, следующий файл Alloy...
sig Y {}
sig X {r : Y -> Y} {
//#r = 2
}
run {} for exactly 1 X, 3 Y
... дает мне решение, которое содержит 2 rкромки (см. рисунок ниже). Однако, если я раскомментирую #r = 2 линия, Alloy не может найти решения! Что я делаю неправильно?
Редактировать. Я обнаружил, что эта проблема затрагивает только AlloyStar (в отличие от ванильного сплава). При использовании AlloyStar (версия 0.2) я получаю
Выполнение "Run run$1 ровно для 1 X, 3 Y"
Solver = minisatprover (jni) Бит пропускная способность =1 MaxSeq=0 Симметрия = 20
69 вар. 12 первичных перемен. 167 статей. 923ms.
Экземпляр найден. Предикат последовательный. 21ms.
но когда я раскомментирую #r = 2, Я получил
Выполнение "Run run$1 ровно для 1 X, 3 Y"
Solver = minisatprover (jni) Бит пропускная способность =1 MaxSeq=0 Симметрия = 20
0 вар. 0 первичных перемен. 1 пункты. 15мс.
Экземпляр не найден. Предикат может быть противоречивым. 1мс.
Поэтому я думаю, что этот вопрос стал отчетом об ошибках для разработчиков AlloyStar!
2 ответа
Спасибо за сообщение об ошибке. Здесь происходит несколько вещей. По сути, все, что сказал Даниэльп, правильно, но полный ответ немного более нюансирован.
Прежде всего, я предполагаю, что у вас для параметра "Запретить переполнение" установлено значение true, потому что в противном случае вы получите экземпляр независимо от заданной области (битовой ширины) для целых чисел.
Далее, давайте не будем использовать "добавленные факты", потому что добавленные факты могут иметь различную семантику в зависимости от того, включена ли опция "Включить неявное это". Итак, давайте предположим следующую модель Alloy:
sig Y {}
sig X {r: Y -> Y}
fact { #r = 2 }
run {} for exactly 1 X, 3 Y
Теперь в Alloy4.2, когда целочисленная граница не указана, битовая ширина по умолчанию, используемая механизмом для представления целочисленных выражений (например, выражений мощности множества, целочисленных констант и т. Д.), Равна 5; поскольку константа 2 представлена в 5 битах, переполнения не происходит, и экземпляр найден.
В Alloy*, с другой стороны, битовая ширина по умолчанию равна 1, что недостаточно для представления константы 2, следовательно, происходит переполнение, и экземпляр не найден. Почему битовая ширина 1 была выбрана по умолчанию? Я не уверен на 100%, но, возможно, это произошло потому, что была добавлена поддержка битовых векторов, а также некоторые тесты синтеза с использованием битовых векторов, поэтому на момент написания статьи было удобно это сделать.
Кажется, вам нужно настроить битовую пропускную способность:
Выполнение "Run run$1 ровно для 1 X, 3 Y"
Solver = minisatprover (jni) Бит пропускная способность = 1 MaxSeq = 0 Симметрия = 20
0 вар. 0 первичных перемен. 1 пункты. 15мс.
Экземпляр не найден. Предикат может быть противоречивым. 1мс.
Число 2 не может быть представлено с битовой шириной 1. Я предполагаю, что пример работает в стандартном Alloy, потому что там битовая пропускная способность по умолчанию выше.