title: TLA+: How to delete structure key/value pairings?
body: <p>I have a specification where I am attempting to define an LRU Cache system and one of the problems I am running into is how I can go about deleting values from a structure key/value pairing (which is basically a dictionary or a hash-map in other languages). </p>
  
  <p>Here is the specification itself so far (incomplete):</p>
  
  <pre><code>EXTENDS Integers, Sequences
  VARIABLES capacity, currentSize, queue, dictionary
  
  Init == /\ (capacity = 3 ) /\ (currentSize = 0)
          /\ (queue = &lt;&lt;&gt;&gt;) /\ (dictionary = [])
  
  
  AddItem(Item, Value) == IF currentSize &lt; 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
  </code></pre>
  
  <p>I was referencing <a href="https://learntla.com/reference/types/" rel="nofollow noreferrer">this documentation on the Learn TLA Plus</a> website but there seems to be nothing on removing a key value pair from the list. So far the only thing I could think to do would be to filter out the value that matches the key and create a new dictionary object, but I would prefer a method with a little more direct access. </p>