операция xor в Alloy

Есть ли в сплаве операция xor, если нет, то как ее определить:

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

более подробно, если у меня есть P1 и P2, я знаю, что я могу определить P3 следующим образом:

pred P3(){
   (P1 and (not P2)) or ((not P1) and P2)
}

быть xor P1 и P2, но я хочу определить xor (или любые другие связки формул), поместить его в библиотеку и использовать их позже. поэтому я хотел бы, чтобы мой P3 получил предикаты в качестве аргумента. Это возможно?

Спасибо


alloy
person qartal    schedule 05.12.2014    source источник

Ответы (2)


arrow_upward
6
arrow_downward

Alloy, к сожалению, не имеет логического типа. Без правильного типа вы не можете объявить аргументы для своего предиката. Таким образом, ваш подход кажется безнадежным.

Я могу придумать два уродливых трюка, оба из которых включают использование util/boolean или ваше собственное логическое определение, чтобы все заработало.

В обоих случаях ваш предикат XOR должен принимать два логических аргумента.

pred xor[ x,y:Bool){
   x != y
}

В первом приеме представьте все свои предложения в виде одноэлементных сигнатур (например, P1 и P2), а не предикатов. Пусть эти подписи объявляют поле с логическим типом (например, bool) и устанавливают это поле в факте подписи, используя формулу, которую вы бы поместили в свои предикаты P1 и P2.

вызовите затем свой предикат xor следующим образом:

xor[P1.bool ,P2.bool]

Во втором трюке вы сохраняете свои предложения, представленные в виде предикатов (P1 и P2), но при вызове xor вам нужно будет «привести» истинностное значение этих предикатов к Bool.

xor[(P1 implies True else False ),(P2 implies True else False )]

Опять же, на мой взгляд, оба решения уродливы. Было бы неплохо иметь более широкое представление о том, чего вы хотели бы достичь, чтобы прийти к лучшему решению.

person Loïc Gammaitoni    schedule 05.12.2014

arrow_upward
6
arrow_downward

Операцию xor можно просто записать как iff not.

person CptHindsight    schedule 11.02.2016