How to express structural equality between trees in Alloy?

Question

I have defined the following Alloy model that uses a single State object to point to the roots of two trees State.a and 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

Among the solutions I get:

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

So I get two trees N2 -> N0 and N3 -> N1 that are structurally equal.

How can I further constraint this model so that State.a and State.b are not equal in this sense?

I am afraid that this can only be done with a recursive predicate and recursion is only possible to a limit of depth 3 (I think).

Therefore, I would favour a non-recursive solution if this is possible.

Answer 1

You said everything right about the recursion the recursion depth. I just tried the following recursive predicate, which did work fine for small trees

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

Another way to achieve this, which doesn't require recursion, is to model the noniso relationship as an Alloy relation, and then assert for all nodes that this relation contains all non-isomorphic pairs. You could do that like this

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)
  }
}

To put this to test, I created show_noniso and show_iso predicates that create trees with 4 levels of nesting.

// 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
}

and then ran various combinations

// 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

The results of these analyses were as expected

   #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.