합금에서 나무 사이에 구조적 평등을 표현하는 방법은 무엇입니까?

Question

이 단일 상태 개체를 사용하여 두 개의 나무 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까지만 가능합니다 (제 생각 엔).

따라서 가능한 경우 비회원 솔루션을 선호합니다.

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

테스트이 말하면처럼, 내가 중첩의 4 단계 나무를 만들 show_noniso 및 show_iso 조건을 만들 것을 할 수 있습니다.

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

예상대로였다