Как выразить структурное равенство между деревьями в Alloy?

Я определил следующую модель Alloy, которая использует один объект State для указания на корни двух деревьев State.a и State.b.

sig N {
  children: set N
}

fact {
  let p = ~children |
    ~p.p in iden
    and no iden & ^p
}

one sig State {
  a: one N,
  b: one N
}

fun parent[n:N] : N {
  n.~children
}

fact {
  no State.a.parent
  no State.b.parent
  State.a != State.b
  State.a.^children != State.b.^children
}

pred show {}

run show for 4

Среди решений я получаю:

                 +-----+
              +--+State|+-+
             a|  +-----+  |b
              |           |
              v           v
             +--+       +--+
             |N2|       |N3|
             ++-+       +-++
              |           |
             +v-+       +-v+
             |N0|       |N1|
             +--+       +--+

Таким образом, я получаю два дерева N2 -> N0 и N3 -> N1, которые структурно равны.

Как я могу дополнительно ограничить эту модель, чтобы State.a и State.b не были равны в этом смысле?

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

Поэтому я бы предпочел нерекурсивное решение, если это возможно.


equality tree alloy structural-equality
person Peter Slotko    schedule 27.01.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

pred noniso[n1, n2: N] {
  #n1.children != #n2.children or 
  some nn1: n1.children, nn2: n2.children | noniso[nn1, nn2]
}

Другой способ добиться этого, который не требует рекурсии, — смоделировать отношение noniso как отношение Alloy, а затем утверждать для всех узлов, что это отношение содержит все неизоморфные пары. Вы могли бы сделать это вот так

one sig G {
  noniso: N -> N
} {
  all n1, n2: N {
    (n1 -> n2 in noniso) iff 
      (#n1.children != #n2.children or 
       some nn1: n1.children, nn2: n2.children | nn1 -> nn2 in noniso)
  }
}

Чтобы проверить это, я создал предикаты show_noniso и show_iso, которые создают деревья с 4 уровнями вложенности.

// differ at level 4 only
pred show_noniso[n1, n2, n3, n4, n5, n6, n7: N] {
  children = n1 -> n2 + n2 -> n3 + n3 -> n4 + n5 -> n6 + n6 -> n7
  State.a = n1
  State.b = n5
}

pred show_iso[n1, n2, n3, n4, n5, n6, n7, n8: N] {
  children = n1 -> n2 + n2 -> n3 + n3 -> n4 + n5 -> n6 + n6 -> n7 + n7 -> n8
  State.a = n1
  State.b = n5
}

а потом запускал разные комбинации

// USING RECURSION_DEPTH SET TO 2
run noniso_recursion_fails {
  some disj n1, n2, n3, n4, n5, n6, n7: N | show_noniso[n1, n2, n3, n4, n5, n6, n7]
  noniso[State.a, State.b]
} for 8 expect 0

run noniso_relation_works {
  some disj n1, n2, n3, n4, n5, n6, n7: N | show_noniso[n1, n2, n3, n4, n5, n6, n7]
  State.a -> State.b in G.noniso
} for 8 expect 1

run iso_relation_works {
  some disj n1, n2, n3, n4, n5, n6, n7, n8: N | show_iso[n1, n2, n3, n4, n5, n6, n7, n8]
  State.a -> State.b in G.noniso
} for 8 expect 0

Результаты этих анализов соответствовали ожиданиям.

   #1: no instance found. noniso_recursion_fails may be inconsistent, as expected.
   #2: instance found. noniso_relation_works is consistent, as expected.
   #3: no instance found. iso_relation_works may be inconsistent, as expected.
person Aleksandar Milicevic    schedule 30.01.2014