module Lists

sig List {
	head : Node
}

sig Node {
	nextN : lone Node
}

fun reachable[l : List] : set Node {
	(l.head).*nextN
}

fact AllNodesReachable {
//	"every node is contained in at least one list"
all n : Node | some l : List | n in reachable[l]
}

fact NoSharing {
// "lists don't share nodes"
// all l : List | l does not share nodes with another list"
// all l1, l2 : List | l1 does not share nodes with l2
// all l1, l2 : List | the set of nodes contained in l1 does not overlap with the set of nodes contained in l2
// all l1, l2: List | (l1 = l2)      or      (no n : Node | (n in (l1.head).*nextN)  && (n in (l2.head).*nextN))
// all l1, l2: List | (l1 != l2)   =>   (no n : Node | (n in reachable[l1])  && (n in reachable[l2]))
// all n : Node | "n contained in at most one list"
// all n : Node | all l1,l2 : List | n in reachable[l1] && n in reachable[l2] => l1=l2
all n : Node | lone l : List | n in reachable[l] 
}

fact NoCycles {
// ...
//	all n : Node | "n is not in a cycle"
//	all n: Node | "n is not reachable from itself in 1 or more steps"
//	all n: Node | "n is not in the set of nodes that can be reached from n in 1 or more steps"
//	all n: Node | n is not in n.^nextN
	all n: Node | !(n in n.^nextN)
//	all n: Node | !(n in n.*nextN)
}

assert Silly {
	all n: Node | !(n in n.^nextN)
}

assert OneTail {
// every list ends in exactly one node
// every list has exactly one node that does not have a successor
// all l : List | "l has exactly one node that does not have a successor"
// all l : List | one "all nodes in l that do not have a successor"
all l : List | one {n : reachable[l] | no n.nextN}
}

pred P {#List=2}

scenario1: run P for  3 
check Silly for 3
check OneTail for 3