Имея следующее:
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]{}
Любая помощь приветствуется.
Вы можете легко определить очередь:
pred Enq[q, q': Queue, n: Node] {
q'.root = n and n.next = q.root
}
Но удаление из очереди не так просто. Проблема в том, что вам нужно изменить узел, а не очередь, чтобы внести изменения в последний узел, необходимый для удаления элемента из очереди. На самом деле вам нужно заменить предпоследний узел в очереди другим узлом, чье поле «следующий» пусто, но, поскольку вы используете идентификатор атома для представления уникальности узла, этот узел на самом деле будет другим узлом.
