As a homework, I have to define a heap data structure in Alloy.
I have come up with these rules
- A node can have up to 1 father, left-son, right-son, left-brother and right-brother. It also has exactly 1 value and 1 level (as in how deep in the heap it is).
- A node can have right-son if it has left-son.
- A node cannot be in transitive closure over any of its relations (father, left-son, right-son, left-brother, right-brother).
- The relations have to point to distinct nodes.
- A node has a value and values must belong to a node.
- A node's value must be less than the node's sons' values.
- If a node has left-son and not left-brother, then the rightmost brother of its father has a right-son.
- Node is its left-brother's right-brother and so on for all its relations.
- Node's father's level is one less than node's level.
- If there is a node with level two less, then all the nodes with that level must have both sons.
- For any 2 nodes m, n that have the same level, m must be in transitive closure over left-brother of n, or in transitive closure over right-brother.
The question is twofold
A) I am not sure whether these rules are sufficient, or whether there is a better way to solve this altogether. (I think I could just resolve this all by having node consist of index and a value and transcribe heap-in-array algorithm into Alloy, but that seems rather inelegant.)
B) I have trouble implementing some of these rules.
I have implemented rules 1, 2, 3, 4, 5, 6, 7, 8 and 9. At least I think I did, and the generated graph does not contradict my expectations.
I do not know how to implement the last 2.
Also, the code I have so far:
open util/ordering [Key] as KO
open util/ordering [Level] as LO
sig Key{}
sig Level{}
sig Node {
key: one Key,
level: one Level,
father: lone Node,
left_brother: lone Node,
right_brother: lone Node,
left_son: lone Node,
right_son: lone Node
}
// There's exactly one root
fact {
one n : Node | n.father = none
}
// Every key has to belong to some node
fact {
all k : Key | some n:Node | n.key = k
}
fact {
all n : Node | (n.left_son != none && n.right_son != none) => #(KO/nexts[n.key] & (n.left_son.key + n.right_son.key)) = 2
}
// Son's father's son shall be Son etc
fact {
all n : Node | all m : Node | (n.left_son = m) => m.father = n
}
fact {
all n : Node | all m : Node | (n.right_son = m) => m.father = n
}
fact {
all n : Node | all m : Node | (m.father = n) => (n.left_son = m || n.right_son = m)
}
// Is this redundant?
fact {
all n : Node | all m : Node | (n.left_brother = m) => (m.right_brother = n)
}
fact {
all n : Node | all m : Node | (n.right_brother = m) => (m.left_brother = n)
}
// If a node has right-son, it must have a left-son.
fact {
all n : Node | (n.right_son != none) => (n.left_son != none)
}
// node having left son and left brother means that his left brother has a right son
fact {
all n: Node | (n.left_son != none && n.left_brother != none) => (n.left_brother.right_son != none)
}
// nodes father must be a level higher.
fact {
all n : Node | (n.father != none) => (LO/prev[n.level] = n.father.level)
}
// FIXME: this is wrong: There needs to be difference of 2 levels, not just a single level.
fact {
all n : Node | all m : Node | (LO/prevs[m.level] & n.level = n.level) => (n.left_son != none && n.right_son != none)
}
// TODO: If 2 nodes are in the same level, then they must be in left-brother* or right-brother* relation
// ????
// No node can be its own father
fact {
all n : Node | n.father != n
}
// No node can be in transitive closure over its ancestors
fact {
no n : Node | n in n.^father
}
// No node cannot be its own brother, son, etc...
fact {
all n: Node | n.left_brother != n
}
// Nor in its transitive closure
fact {
no n: Node | n in n.^left_brother
}
fact {
all n: Node | n.right_brother != n
}
fact {
no n: Node | n in n.^right_brother
}
fact {
all n: Node | n.left_brother != n
}
fact {
no n: Node | n in n.^left_brother
}
fact {
all n: Node | n.right_son != n
}
fact {
no n: Node | n in n.^right_son
}
fact {
all n: Node | n.left_son != n
}
fact {
no n: Node | n in n.^left_son
}
// All node relatives have to be distinct
fact {
all n: Node | n.left_son & n.right_son = none && n.left_brother & n.right_brother = none && (n.left_brother + n.right_brother) & (n.left_son + n.right_son) = none
&& (n.right_son + n.left_son + n.left_brother + n.right_brother) & n.father = none
}
run{}
