연결된 목록, 같은 요소가 없습니다.

Question

sig List { 
    header: set Node 
} 
sig Node { 
    link: set Node, 
    elem: set Int 
} 

같은 요소를 가리 키도록 두 개의 노드를 원하지 않습니다. 어떻게이 일을 성취 할 수 있습니까?

는 정말 * 연산자를 이해하지 않지만, 나는 그 N 가정

all n: Node | n.elem != n.*link.elem 

했습니다. * link.elem는

n.link.elem 
n.link.link.elem 
n.link.link.link.elem 

과 세트의 모든 요소를 ​​가리키는 것 그러나 이것은 효과가 없습니다. 당신 ELEM 필드

sig List { 
    header: set Node 
} 
sig Node { 
    link: set Node, 
    disj elem: set Int 
} 

를 선언 할 때

Answer 1

당신은 단순히이 두 개의 노드 N1과 N2 등 N1 것을이 없다는 것을 표현하는 속기입니다 disj 키워드를 사용할 수 있습니다! = N2 및 n1.elem & N2를. ELEM! = 없음 당신이 뭘하려에 관한

,

all n: Node | n.elem != n.*link.elem 

모든 노드 N에 대해, n으로 관련된 요소가 요소 asso 다르다는 것을 말한다 n에 연결된 노드로 전달됩니다. 두 가지 흐름이 있습니다.

먼저 n에 ​​연결되지 않은 노드는 고려하지 않습니다.

두 번째로, elem은 정수 세트임을 고려해야합니다. n1.elem = {1,2,3,4} 및 n2.elem = {1,2,3}이라고 가정합니다. writting n1.elem은 {1,2,3,4}! = {1,2,3}만큼 충분하지 않습니다.이 경우 n1과 n2는 모두 1,2,3을 가리 킵니다. 따라서 분리는 당신이 필요로하는 것입니다.

Answer 2

정수 구조의 연결된 목록을 더 잘 이해하기 위해 다음 모델을 제안합니다.

sig List { 
    header: lone Node // empty list or one header node 
} 

sig Node { 
    link: lone Node, // 0 or 1 next node 
    elem: one Int  // prohibit empty nodes 
} 

fact { 
    no n: Node | n in n.^link     // prohibit cycles 
    all disj n, n': Node | n.elem != n'.elem // different nodes have different elements 
    all n: Node | one l: List | n = l.header or n in l.header.^link 
               // every node belongs to a list 
} 

Answer 3

노드가 필요합니까?

이렇게 더 추상적 인 것은 어떻습니까?

abstract sig List {} 
sig EmptyList extends List {} 
sig NonEmptyList extends List {rest: List, contents: T}