Синтаксис ограничений в предикате и в утверждении

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

Ограничение все disj x1,x2:X | x1 =x2 дает разные результаты при выполнении в предикате и в утверждении.

Например, предположим следующую модель:

sig A {}

sig B {x: one A}

assert S1 
{all x1,x2: x | x1 = x2}

проверить S1 на 2 - контрпримеры как неэквивалентные экземпляры x1 и x2

assert S2
{! (all x1,x2: x | x1 = x2)}

проверьте S2 на 2 -- ошибка количественного определения более высокого порядка

pred P1 
{(all x1,x2: x | x1 = x2)}

run P1 for 2 -- higher-order quantification error

pred P2
{! (all x1,x2: x | x1 = x2)}

run p2 for 2 -- генерирует неэквивалентные экземпляры x1 и x2

почему некоторые ограничения поддаются количественной оценке, а их отрицание — нет, и наоборот!

спасибо

Абдалла Райхан


alloy
person user3252138    schedule 30.01.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Во всех 4 из этих примеров у вас есть квантификатор более высокого порядка: вы пытаетесь количественно оценить двоичное поле (x: A -> B), поэтому, когда вы говорите all x1, x2: x | ..., это означает «для всех двоичных кортежей x1 и x2, взятых из двоичного отношения x ". Сплав относится к первому порядку и обычно не может обрабатывать материалы более высокого порядка. Причина, по которой он не жалуется в некоторых из этих случаев, заключается в том, что он может «сколемизовать» квантификатор, так что ему не нужно ничего проверять для всех кортежей с арностью больше 1. .

Например, когда вы говорите check S1, вы спрашиваете Alloy, верно ли, что что-то верно для всех двоичных кортежей; поскольку Alloy является ограниченным искателем модели, он попытается опровергнуть это, найдя один такой кортеж, для которого тело не выполняется --- там нет ничего более высокого порядка, поэтому этот случай будет Работа. Когда вы говорите «проверить S2», вы спрашиваете Alloy, не правда ли, что что-то верно для всех двоичных кортежей, поэтому, чтобы опровергнуть это, Alloy фактически должен проверить, что тело выполняется для каждого такого двоичного файла. tuple --- это более высокий порядок, и Alloy не может этого сделать.

Я не знаю, было ли ваше намерение изначально иметь количественную оценку более высокого порядка. Просто догадываюсь, может быть, вы хотели иметь просто all b: B, a: b.x | ..., что является первым порядком и будет работать нормально.

person Aleksandar Milicevic    schedule 30.01.2014