Я не смог понять кардинальность сплава. Я сократил свой код до этого тривиального примера, для которого Alloy не может найти экземпляр:
sig A {}
sig B { s: set A}
fact x { one n: Int | all b: B | #(b.s) = n }
run {} for 10
А именно, что мощность B.s должна быть одинаковой для всех членов B. Почему Alloy не может найти пример этого?
Если вы измените свою команду run на run {} for 10 but 5 int, вы должны начать видеть экземпляры.
На самом деле это не удовлетворительный ответ (я надеюсь, что один из членов команды Alloy справится лучше), но похоже, что непосредственная проблема заключается в том, что, хотя Int встроен, он не всегда создается. Когда нет экземпляров Int, факт не может быть удовлетворен. (Закомментируйте факт, сгенерируйте экземпляр, а затем попросите оценщика оценить выражение Int. Когда я это сделал, оценщик вернул {}.)
Я бы с удовольствием объяснил это лучше, но мне не удалось найти или открыть правила, определяющие, когда атомы Int генерируются, а когда нет.
В настройках вы можете установить уровень детализации сообщений на высокий. Там, когда вы запустите команду, вы увидите, что битовая ширина (которая определяет максимальное значение Int для Alloy) равна 0. Раньше по умолчанию было 4, я не уверен, что происходит.
Как было предложено в другом ответе, установка Int на некоторое значение увеличивает битовую ширину и, следовательно, увеличивает максимальный Int, разрешенный Alloy.
В Alloy очень не рекомендуется работать с Int. Вот способ написать тот же оператор, избегая Int:
sig A {}
sig B { s: set A}
fact x { all b,b2: B | #(b.s) = #(b2.s) }
run { some B.s and #B>1} for 10
Я добавил кое-что в оператор запуска, чтобы увидеть несколько интересных примеров.
