queue - 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]{}

どんな助けでも大歓迎です。