CODEWITHSUNDEEP
alloy
Michael Spagon
Michael Spagon

Reputation: 151

linked list, no two elements the same

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

I want no two nodes to point to the same element. How can this be achieved?

I don't really understand the * operator, but I tried 

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

assuming that n.*link.elem would point to all elements in the set, such as

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

But this is not working.

Upvotes: 0

Views: 267

Answers (3)

Daniel Jackson
Daniel Jackson

Reputation: 2768

Do you need nodes?

How about something more abstract like this?

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

Upvotes: 1

Attila Karoly
Attila Karoly

Reputation: 1021

For a better approximation of the linked list of integers structure, I'd suggest the following model.

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
}

Upvotes: 1

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

you can simply use the disj keyword when declaring your elem field

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

This is a shorthand to express that there's no two nodes n1 and n2 such that n1 != n2 and n1.elem & n2.elem != none

Concerning what you tried, 

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

says that for all node n, the elements associated to n is different from the elements associated to the nodes linked to n. This has two flows.

First, you do not take into considerations nodes that are not linked to n.

Second, you should take into account that elem is a set of Integers. Suppose n1.elem= {1,2,3,4} and n2.elem={1,2,3}. writting n1.elem is not enough as {1,2,3,4} != {1,2,3}.In this case, n1 and n2 points both to 1,2 and 3 . A disjunction is thus what you need.

Upvotes: 3

Related Questions