Почему в Alloy не встречается простой целочисленный контрпример? - PullRequest
Новая
       50

Почему в Alloy не встречается простой целочисленный контрпример?

0 голосов
/ 21 сентября 2018

Я пытаюсь смоделировать связь между числовой переменной и логической переменной, в которой, если числовая переменная находится в определенном диапазоне, тогда логическая переменная изменит значение.Я новичок в Alloy, и у меня возникают проблемы с пониманием того, как достаточно ограничить свою область видимости, чтобы получить очевидный контрпример.Мой код выглядит следующим образом: 

open util/boolean 

one sig Object {
    discrete : one Bool,
    integer : one Int
}

fact { all o : Object | o.integer > 0 and o.integer < 10 }
fact { all o : Object | o.integer > 5 iff o.discrete = False }

assert discreteCondition { all o : Object | o.discrete = True }

check discreteCondition for 1000

Поскольку o.integer имеет целочисленные значения и колеблется от 0 до 10, это может быть только один из 10 различных вариантов.И я указал, что у каждого Object должен быть только один integer и один discrete.Поэтому мне кажется разумным, что здесь нужно проверить только 10 случаев: один случай для каждого значения integer.И все же даже с 1000 делами я получаю

Контрпример не найден.

Если я удаляю переменную integer и связанные с ней факты, тогда он находит контрпример почти сразу,Я также пытался использовать другие решатели и увеличивать различные значения глубины и памяти в опциях, но это не помогло, поэтому ясно, что мой код ошибочен.

Как я могу ограничить область действия, чтобы Alloy нашел контрпример(перебирая возможные значения integer)?Спасибо!

1 Ответ

0 голосов
/ 21 сентября 2018

По умолчанию, битовая ширина, используемая для представления целых чисел, равна 4, поэтому во время генерации экземпляра учитывается только целое число в диапазоне [-8,7], и поэтому, из-за целочисленных переполнений, ваш первый факт является недействительным (так как 10за пределами этого диапазона).

Чтобы устранить проблему, увеличьте используемую битовую полосу как минимум до 5: 

check discreteCondition for 10 but 5 Int.

Обратите внимание, что диапазон 1000 не означает, что вы рассматриваете случай 1000 в вашеманализ.Область действия - это максимальное количество атомов, присутствующих в сгенерированном экземпляре, которое вводится после данной подписи.В вашем случае у вас есть только одна подпись с кратностью один.Таким образом, анализ вашей модели с диапазоном 1 или 10000 ничего не меняет.В сгенерированном экземпляре все еще будет только один атом Object.Вы можете проверить это Q / A, чтобы узнать больше об областях применения Указание области действия для Sig in Alloy

...