如何表达Alloy中树木之间的结构平等？答案

【问题标题】：How to express structural equality between trees in Alloy?如何表达Alloy中树木之间的结构平等？
【发布时间】：2014-01-30 23:04:44
【问题描述】：

我定义了以下合金模型使用单个 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 的限制（我认为）。

因此，如果可能的话，我倾向于使用非递归解决方案。

【问题讨论】：

标签： tree equality alloy structural-equality

【解决方案1】：

关于递归的递归深度，你说的都是对的。我刚刚尝试了以下递归谓词，它确实适用于小树

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

实现此目的的另一种不需要递归的方法是将noniso 关系建模为合金关系，然后为所有节点断言该关系包含所有非同构对。你可以这样做

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.

【讨论】：