sig LinkedList{
	head: ListNode
	}

sig ListNode {
	next: ListNode,
	prev: ListNode
	}

fact {
	all n: ListNode | n.next.prev = n
	}

pred show{}

run show for 5 but 2 LinkedList

// 1. start with the simple example, show examples --> identify that there are single nodes
// also note that there are implicit constraints already in the model above, such as that
// each node has exactly one next and prev node

// 2. in order to get rid of single nodes:
/*
fact{
    all n: ListNode | some l: LinkedList | n in l.head.*next
}
*/

// 3. check that two lists do not share the same head (which obviously fails)
/*
assert notShared {
	all disj l1, l2 : LinkedList | l1.head != l2.head
   }
check notShared for 2
*/

// 4. make this a fact
// now the assertion holds (trivially)
/*
fact notSharedHead {
	all disj l1, l2: LinkedList | l1.head != l2.head
}
*/

// check for other pathologic cases with show above --> heads share lists!

// 5. add the following predicate and retry with notSharedNode
/*
// a predicate that constraints node n to be reachable from l.head
pred inList [ l: LinkedList, n: ListNode ] {
	n in l.head.*next
}
*/

// 6. two disjoint lists should not contain shared nodes (will fail)
/*
assert notSharedNodes {
	all n: ListNode | no disjoint l1, l2: LinkedList | inList[l1,n] and inList[l2,n]
}
check notSharedNodes for 2
*/ 

// 7. ask yourself: what would be a good constraint to avoid two lists sharing nodes?