Это ошибка оценщика сплавов?

Учитывая приведенный ниже простой тест, в некоторых случаях Оценщик дает отрицательное количество элементов.

sig A{}
pred show{}
run show

// 2nd instance
univ          {A$0}
#univ         -1

// 3rd instance
univ          {A$0, A$1}
#univ         -2

// 4th instance
univ          {A$0, A$1, A$2}
#univ         3

alloy
person Attila Karoly    schedule 29.01.2015    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Возможно. Но если вы явно добавляете целые числа в юниверс, он возвращает допустимое число. Я имею в виду что-то вроде run show for 3 Int

person user3013493    schedule 29.01.2015
comment
С добавлением целых чисел во вселенную я получаю: univ: {-1, -2, -3, -4, 0, 1, 2, 3, A$0, A$1}, #univ-›univ: -4 - person Attila Karoly; 30.01.2015
comment
кардинальность univ->univ в вашем случае (когда размер вселенной равен 10) равна 100; 100 в двоичном формате — это 1100100; в вашем случае битовая ширина равна 3, поэтому только последние 3 бита 1100100 (100) берутся и интерпретируются в дополнении до двух, что дает -4. - person Aleksandar Milicevic; 30.01.2015
comment
Как и в последнем случае, во Вселенной нет атома, представляющего число 4, поэтому происходит переполнение. Если вы хотите, чтобы во вселенной было 4, добавьте больше целых чисел. run for 4 Int добавляет целые числа в [-2^4,2^4) к юниверсу. - person user3013493; 30.01.2015
comment
независимо от того, какая разрядность целого числа установлена ​​(т. е. сколько еще целых чисел вы добавите), univ->univ всегда будет содержать больше элементов, чем целых чисел в вашей вселенной, поэтому #univ->univ всегда будет переполняться. - person Aleksandar Milicevic; 30.01.2015
comment
Спасибо большое. Имеет ли битовая ширина тот же эффект в выражениях в предикатах и ​​т. Д. При выполнении команды «выполнить» или «подтвердить»? - person Attila Karoly; 30.01.2015
comment
Да, битовая ширина важна для всех целочисленных выражений (целочисленных констант, арифметических операторов и оператора мощности), независимо от того, где они встречаются; для реляционных выражений битовая ширина не имеет значения. - person Aleksandar Milicevic; 30.01.2015
comment
Я вижу, что #univ->univ должно быть больше, чем битовая ширина, но Alloy Evaluator не считает целые числа для кардинальности. В этом примере, если во вселенной существуют два атома A, оценщик возвращает 2 для #univ и 4 для #univ-›univ, если битовая ширина установлена ​​правильно. - person user3013493; 31.01.2015
comment
Я понимаю, что происходит целочисленное переполнение. Тем не менее, я не понимаю, что -1 когда univ содержит только один элемент. Как получилось -1? это не часть целочисленной полосы пропускания, как 1 ... нет? - person bilboul boulbil; 02.02.2015