使用 Alloy 实现队列的入队和出队

Question

具备以下条件：

sig Queue { root: Node }
sig Node { next: lone Node }
fact nextNotReflexive { no n:Node | n = n.next }
fact nextNotCyclic { no n:Node | n in n.^next }

谁能帮忙实现 Enq 和 Deq？

pred Enq[q,q':Queue, n:Node]{}
pred Deq [q,q':Queue]{}

感谢任何帮助。

Answer 1

您可以轻松定义入队：

pred Enq[q, q': Queue, n: Node] {
  q'.root = n and n.next = q.root
}

但出队并不那么容易。问题是您需要修改节点，而不是队列，以便对元素出列所需的最后一个节点进行更改。您实际上需要用“next”字段为空的不同节点替换队列中的倒数第二个节点 - 但由于您使用原子标识来表示节点唯一性，因此该节点实际上将是一个不同的节点。