2.9 KiB
2.9 KiB
https://alloy.readthedocs.io/en/latest/language/signatures.html#relations
Note
Node.prox' = Node.prox != all n:Node | n.prox' = n.prox = prox' = prox
Note
some b: Bucket | ...
// Recall the hash table Alloy model,
// now with mutable lists inside the buckets.
sig Bucket {
var head : lone Node
}
sig Node {
key : one Key,
var prox : lone Node
}
sig Key {
hash : one Hash
}
sig Hash {}
// Specify the operation of inserting a node
// in the hash table. The node should be
// inserted at the head of a bucket.
// If the operation only works well when the
// hash of the new node does not exist in the
// table you get Two points. If it always
// works well you get Five points. Use the
// respective commands to check how many
// points you have.
pred insert[n : Node] {
always n in ( Bucket.head + Bucket.head.prox)
always n in Bucket.head or n in Node.prox
//if hash empty -> node to head of bucket
n.key.hash not in Hash implies
(
lone b:Bucket | b.head = none implies b.head' = n
)
//if hash empty -> bucket of desired hash, add to next
n.key.hash in Hash implies
(
lone b: Bucket | b.head.key.hash = n.key.hash | b.head.*prox = n
)
}
pred insert[n : Node] {
//nodes always in the head or linked to prox
//always n in ( Bucket.head + Bucket.head.prox)
always n.key.hash not in Hash {
always lone b: Bucket| b.head = none {
b.head = n
}
}
}
//Solved
// Recall the hash table Alloy model,
// now with mutable lists inside the buckets.
sig Bucket {
var head : lone Node
}
sig Node {
key : one Key,
var prox : lone Node
}
sig Key {
hash : one Hash
}
sig Hash {}
// Specify the operation of inserting a node
// in the hash table. The node should be
// inserted at the head of a bucket.
// If the operation only works well when the
// hash of the new node does not exist in the
// table you get Two points. If it always
// works well you get Five points. Use the
// respective commands to check how many
// points you have.
pred nodeToHead[n : Node]{
//node not in hash
n.key.hash not in Bucket.head.key.hash
some b : Bucket | {
b.head= none and b.head' = n //put node in the head
all x : Bucket - b | x.head' = x.head //everything remains the same
all y : Node | y.prox' = y.prox //all nodes remain the same
}
}
pred nodeToTail[n: Node]{
//node not in linked lists of buckets
n not in Bucket.head.*prox
//node in hash
n.key.hash in Bucket.head.key.hash
some b : Bucket | {
b.head.key.hash = n.key.hash and { //same hash
(b.head' = n and n.prox' = b.head) //new head
all x : Bucket - b | x.head' = x.head //all other buckets remain the same
all y : Node - n | y.prox' = y.prox //all other nodes remain the same
}
}
}
pred insert[n : Node] {
nodeToHead[n] or nodeToTail [n]
}