(Hard!) Which of the following is a counterexample to the following assertion?

	sig Node {
		next: lone Node, 
		prev: lone Node
	}
	sig Head extends Node {}
	
	fact exactlyOneHead { one Head }
	fact headHasNoPrev { no Head.prev }
	fact prevIsInverseOfNext { all n:Node | n.next.prev = n }
	
	assert acyclic { no n:Node | n in n.^next }
	check acyclic for 5

	1 [Question_3_1.png]
	2 [Question_3_2.png]
	3 None. The assertion is valid. 

Feedback for incorrect answers(1, 2):
	1 Wrong. This is not an instance of the above model as it violates prevIsInverseOfNext: Head is defined but Head.next.prev is undefined. 
	2 Wrong. This is not an instance of the above model as it violates headHasNoPrev. 

Feedback for correct answer(3):
	3 This is the correct aswer! Here is an informal explanation: Assume there is a cycle. Then when we traverse the nodes, we will eventually get back to a node that we have already visited. This node cannot be the Head by headHasNoPrev. Also, it cannot be a non-Head node as this would mean that it that has two prevs. As a node can have at most one (lone) prev, this shows that there cannot be a cycle. 

Footnote: This is an abridged version of an example taken from http://alloy.mit.edu/tutorial3/currentmodel-FS-I.html