實現入隊和出隊的隊列採用合金

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 
} 

但離隊是不是幾乎一樣容易。問題是你需要修改一個節點，而不是一個隊列，以便對最後一個節點進行更改以便使隊列出隊。實際上，您需要使用其「下一個」字段爲空的不同節點替換隊列中倒數第二個節點 - 但由於您使用原子標識來表示節點唯一性，因此該節點實際上將是不同的節點。