实现入队和出队的队列采用合金

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 } 

任何人都可以在的查询和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 
} 

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