lru - TLA+:如何删除结构键/值对？

Question

我有一个规范，我试图定义一个 LRU 缓存系统，我遇到的一个问题是如何从结构键/值对(基本上是字典或哈希映射)中删除值其他语言)。

到目前为止，这是规范本身(不完整):

EXTENDS Integers, Sequences
VARIABLES capacity, currentSize, queue, dictionary

Init == /\ (capacity = 3 ) /\ (currentSize = 0)
        /\ (queue = <<>>) /\ (dictionary = [])


AddItem(Item, Value) == IF currentSize < capacity
            THEN /\ currentSize' = currentSize + 1
                 /\ queue' = Append(queue, Item)
                 /\ dictionary[item] = value
            ELSE /\ queue' = Append(Tail(queue), Item) 
                 /\ dictionary' = [x \in dictionary: x /= queue[3]]

GetItem(Item) == dictionary[item]

Next == \/ AddItem 
        \/ GetItem

我在引用 this documentation on the Learn TLA Plus网站，但似乎没有从列表中删除键值对。到目前为止，我唯一能想到的就是过滤掉与键匹配的值并创建一个新的字典对象，但我更喜欢一种更直接访问的方法。

Answer 1

在我回答之前，我必须问另一个问题:“删除值”是什么意思？请记住，TLA+ 不是一种编程语言:它是一种规范语言。这意味着它建立在对您正在做的事情的非常清楚的了解之上。所以我们来谈谈删除。

TLA+ 中仅有的两个复杂集合是集合和函数。函数将一组元素(其域)映射到值。结构和序列只是函数的语法糖:结构的域是它的固定键，而序列的域是1..n , n \in Nat .函数需要有一个域。如果你想从结构中“删除”一个键，你需要从结构的域中“删除”它。

相应的 Action 是取序列的尾部。 Lamport 在 Specifying Systems 的第 341 页上定义了这一点。 ，包含在 TLA+ 工具箱中。这是定义(来自标准模块 Sequences.tla ——在链接版本中略有修改):

Tail(seq) == [i \in 1 .. (Len(seq) - 1) |-> seq[i + 1]]

换句话说，序列的尾部是通过将序列偏移量加一来定义的，并删除最后一个元素。从函数的域中删除某些东西是通过构造一个相同的函数来“完成”的，而没有其域中的一个元素。仔细想想这是有道理的:我们不能改变一个数学函数，就像我们不能改变数字 7 一样。

再说一遍，我们需要在现有函数的基础上构建足够多的新函数，以便 TLA+ 添加一些方便的语法。为了更改函数中的单个映射，我们有 EXCEPT .为了添加新映射，TLC 模块添加了 @@运算符(operator)。删除映射通常不是人们做的事情，所以我们必须自己定义它。你必须做类似的事情

dictionary' = [x \in DOMAIN dictionary \ {item} |-> dictionary[x]]

请注意，您添加到字典的方式是错误的: dictionary[item] = value是相等检查，而不是赋值。 dictionary'[item] = value也不起作用，因为它没有完全指定 dictionary .你必须做类似的事情

dictionary' = [x \in {item} |-> value] @@ dictionary

(或使用 :> ，也在 TLC 模块中)

在这一点上，它可能尝起来好像我们走错了路，可能有一种更简单的方法来指定一个不断变化的 dict。我猜你的规范不依赖于你的键的一些实现细节:如果你使用字符串而不是整数作为键，你不希望你的缓存改变行为。在这种情况下，我会指定一组任意的键和值，这样我们就可以像这样定义突变:

CONSTANTS Keys, Values, NULL
VARIABLE dict \* [key \in Keys |-> NULL]

Add(dict, key, val) == [dict EXCEPT ![key] = val]
Del(dict, key, val) == [dict EXCEPT ![key] = NULL]

在哪里 dict[key] = NULL表示该键不在字典中。

这通常是我向初学者推荐 PlusCal 的原因之一，因为这样您就不必担心如何在学习规范的基础知识时改变函数。如果你正在编写一个 pluscal 算法，你可以用 dict[key] := val 改变字典。 .