sig Queue {
	root: Node
}

sig Node {
	next: lone Node
}

========================

sig Queue {
	root: Node
}

sig Node {
	next: lone Node
}

pred show() {}

run show for 2

========================

sig Queue {
	root: Node
}

sig Node {
	next: lone Node
}

fact nextNotReflexive {
	no n:Node | n = n.next
}

pred show() {}

run show for 2

========================

sig Queue {
	root: Node
}

sig Node {
	next: lone Node
}

fact nextNotReflexive {
	no n:Node | n = n.next
}

fact allNodesBelongToSomeQueue {
	all n:Node | some q:Queue | n in q.root.*next
}

pred show() {}

run show for 2

========================

sig Queue {
	root: Node
}

sig Node {
	next: lone Node
}

fact nextNotReflexive {
	no n:Node | n = n.next
}

fact allNodesBelongToOneQueue {
	all n:Node | one q:Queue | n in q.root.*next
}

pred show() {}

run show for 2

=======================

sig Queue {
	root: Node
}

sig Node {
	next: lone Node
}

fact nextNotReflexive {
	no n:Node | n = n.next
}

fact allNodesBelongToOneQueue {
	all n:Node | one q:Queue | n in q.root.*next
}

fact nextNotCyclic {
	no n:Node | n in n.^next
}

pred show() {}

run show for 2

=========================================

sig Queue {
        root: lone Node
}

sig Node {
        next: lone Node
}

pred show() {
	#Queue = 1
	#Node = 3
}

run show

fact nextNotReflexive {
	no n:Node | n = n.next
}

fact allNodesBelongToOneQueue {
	all n:Node | one q:Queue | n in q.root.*next
}

fact nextNotCyclic {
	no n:Node | n in n.^next
}

pred getFirst(q, q':Queue, n:Node) {
	n = q.root
	q'.root = q.root.next
}

// extends, ternary relationon