Понимание мощности сплава

Question

Я не смог понять силу сплава. Я уменьшил мой код до этого простейшего примера, которого сплав не может найти экземпляр для:

sig A {} 
sig B { s: set A} 

fact x { one n: Int | all b: B | #(b.s) = n } 
run {} for 10 

А именно, что мощность Bs должна быть одинаковой для всех членов B. Почему сплав не может найти пример этого?

Answer 1

Если вы изменили команду run на run {} for 10 but 5 int, вы должны начать просмотр экземпляров.

Это не совсем удовлетворительный ответ (я надеюсь, что один из членов команды Alloy может сделать лучше), но похоже, что непосредственной проблемой является то, что, хотя Int встроен, он не всегда создается , Когда нет экземпляров Int, этот факт не может быть удовлетворен. (Прокомментируйте факт, внесите экземпляр, а затем попросите Оценщика оценить выражение Int. Когда я это сделал, оценщик вернул {}.)

Я бы с удовольствием объяснил это лучше, но мне это не удалось находить или открывать правила, определяющие, когда атомы Int генерируются, а когда нет.

Answer 2

В разделе «Параметры» вы можете установить многословие сообщений на Высокий. Там, когда вы запускаете команду, вы увидите, что битовая ширина (которая определяет max Int для Alloy) равна 0. Это по умолчанию было 4, я не уверен, что происходит.

Как было предложено другим ответом, установка Int на некоторое значение увеличивает битрейт и, следовательно, увеличивает максимум Int, разрешенный 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 

я добавил кое-что к заявлению перспективе просто увидеть некоторые интересные экземпляры