Блог

У меня есть спецификация сплава, представляющая правила преобразования модели.. В спецификации я использую количественную оценку более высокого порядка для указания соответствия правилу. Одна странная вещь заключается в том, что анализатор работает по-разному с «некоторыми» и «одним», чего я не могу понять.

Например, в pred rule_enter[trans:Trans](см. Строку 240) я использую два квантования более высокого порядка для кодирования соответствия левой и правой части правила преобразования графа. ********************* ПРИМЕР**************************************

 some e_check0:Acheckamp;trans.darrows, e_TP0:ATPamp;(trans.source.arrows-trans.darrows), e_PF10:APF1amp;trans.darrows, e_TR0:ATRamp;(trans.source.arrows-trans.darrows), e_F1R0:AF1Ramp;trans.darrows |
let n_P0 = e_check0.src, n_T0 = e_TP0.src, n_R0 = e_TR0.trg, n_F10 = e_PF10.trg |
(n_P0 = e_check0.trg and n_P0 = e_TP0.trg and n_P0 = e_PF10.src and n_T0 = e_TR0.src and n_F10 = e_F1R0.src and n_R0 = e_F1R0.trg  and
n_F10 in NF1amp;trans.dnodes and
n_P0 in NPamp;(trans.source.nodes-trans.dnodes) and n_T0 in NTamp;(trans.source.nodes-trans.dnodes) and n_R0 in NRamp;(trans.source.nodes-trans.dnodes))

some e_crit0:Acritamp;trans.aarrows, e_TP0:ATPamp;(trans.source.arrows-trans.darrows), e_PF20:APF2amp;trans.aarrows, e_TR0:ATRamp;(trans.source.arrows-trans.darrows), e_F2R0:AF2Ramp;trans.aarrows |
let n_P0 = e_crit0.src, n_T0 = e_TP0.src, n_R0 = e_TR0.trg, n_F20 = e_PF20.trg |
(n_P0 = e_crit0.trg and n_P0 = e_TP0.trg and n_P0 = e_PF20.src and n_T0 = e_TR0.src and n_F20 = e_F2R0.src and n_R0 = e_F2R0.trg  and
n_F20 in NF2amp;trans.anodes and
n_P0 in NPamp;(trans.source.nodes-trans.dnodes) and n_T0 in NTamp;(trans.source.nodes-trans.dnodes) and n_R0 in NRamp;(trans.source.nodes-trans.dnodes))
 

Здесь я использую ключевое слово «некоторые». Анализатор может работать с областью 10.

Но если я использую ключевое слово «one», анализатор сообщает о следующей ошибке с областью действия 5: ********************* ПРИМЕР**************************************

 Executing "Check check$1 for 5 but exactly 1 Trans, exactly 2 Graph, exactly 1 Rule"
  Solver=minisat(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
  Generating CNF...
.
Translation capacity exceeded.
In this scope, universe contains 89 atoms
and relations of arity 5 cannot be represented.
Visit http://alloy.mit.edu/ for advice on refactoring. 
 

МОЙ ВОПРОС в том, почему две количественные оценки имеют разные характеристики?

one в сплаве кодируется с использованием понимания набора и оператора мощности, например,

 one s: S | p[s]
 

преобразуется в

 #{s: S | p[s]} = 1
 

Понимание множества не может быть сколемизировано, поэтому, когда рассматриваемый квантификатор имеет более высокий порядок, Alloy просто сдается.

Количественные оценки более высокого порядка, как правило, не допускаются в сплаве. Однако некоторые экзистенциальные квантификации (т. Е. Некоторые) Могут быть преобразованы в разрешимые процедуры с помощью процесса, известного как сколемизация, который, я полагаю, не применяется к квантификациям уникальности (т. Е. Единице). Процесс кратко описан здесь для (первого порядка) Пример сплава.

Я не смог обработать ваш пример (извините), но я бы предположил, что это один из таких случаев.

У меня нет конкретного ответа для вашего примера, но, как правило, его сложнее кодировать one , чем some : Предположим, у вас есть набор S, который может максимально содержать элементы a, b, c.

Сплав переводит проблему в проблему SAT. Вы можете закодировать S в задаче SAT с помощью 3 логических переменных xa , xb , xc где xa=TRUE (соответственно FALSE ) означает, что a находится в S (соответственно). не в S).

Теперь это утверждение some S можно легко закодировать в виде формулы

 xa / xb / xc
 

(с / логическим или).

С другой стороны, для one вас необходимо дополнительно закодировать, что если одна из переменных xa , xb , xc истинна, остальные являются ложными. Например.

 xa / xb / xc
xa => not( xb / xc )
xb => not( xa / xc )
xc => not( xa / xb )
 

В конъюнктивной нормальной форме (CNF, это то, что SAT-решатель принимает в качестве входных данных) у вас есть предложения:

 xa / xb / xc
-xa / -xb
-xa / -xc
-xb / -xa
-xb / -xc
-xc / -xa
-xc / -xb
 

Возможно, есть методы для оптимизации этого, но вы можете видеть, что one для кодирования требуется больше предложений, чем some .