sig List {
header: set Node
}
sig Node {
link: set Node,
elem: set Int
}
Я не хочу, чтобы два узла указывали на один и тот же элемент. Как этого добиться?
Я не очень понимаю оператор *, но я пытался
all n: Node | n.elem != n.*link.elem
предполагая, что n.*link.elem будет указывать на все элементы в наборе, например
n.link.elem
n.link.link.elem
n.link.link.link.elem
Но это не работает.
вы можете просто использовать ключевое слово disj при объявлении вашего поля elem
sig List {
header: set Node
}
sig Node {
link: set Node,
disj elem: set Int
}
Это сокращение для выражения того, что не существует двух узлов n1 и n2 таких, что n1 != n2 и n1.elem & n2.elem != none
Что касается того, что вы пытались,
all n: Node | n.elem != n.*link.elem
говорит, что для всех узлов n элементы, связанные с n, отличаются от элементов, связанных с узлами, связанными с n. Это имеет два потока.
Во-первых, вы не принимаете во внимание узлы, не связанные с n.
Во-вторых, вы должны принять во внимание, что elem представляет собой набор целых чисел. Предположим, что n1.elem= {1,2,3,4} и n2.elem={1,2,3}. записи n1.elem недостаточно, поскольку {1,2,3,4} != {1,2,3}. В этом случае n1 и n2 указывают как на 1,2, так и на 3 . Таким образом, дизъюнкция - это то, что вам нужно.
Для лучшего приближения структуры связанного списка целых чисел я бы предложил следующую модель.
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
}
Вам нужны узлы?
Как насчет чего-то более абстрактного?
abstract sig List {}
sig EmptyList extends List {}
sig NonEmptyList extends List {rest: List, contents: T}
